Reducing Ite in a type of an object

Stream: new members

[Michał Pacholski]

I have have reached a point where I need to prove a goal which is essentially trivial, but it's blocked by a cast statement

⊢ ⇑(CategoryTheory.ConcreteCategory.hom
      (cast ⋯ (CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj ⊤)))) =
  id

where the cast is from

((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj ⊤ ⟶ (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj ⊤)

to

((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (if i = i then ⊤ else (TopologicalSpace.Closeds.singleton 0).compl) ⟶ (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (if i = i then ⊤ else (TopologicalSpace.Closeds.singleton 0).compl))

(the type of last id in the goal). I would hope that there is some method to reduce the if-then-else statement in the type of id given that i=i is true, but none of the theorems if_pos, reduceDIte do anything. I couldn't find any way to proceed.

This is the code that lead me to that goal:

import Mathlib

noncomputable
def circleGlueDataCore : TopCat.GlueData.MkCore := by
  constructor
  case J := Fin 2
  case U => intro j; exact TopCat.of ℝ
  case V =>
    intro i j
    exact if i = j then ⊤ else
      TopologicalSpace.Closeds.compl (TopologicalSpace.Closeds.singleton 0)
  case t =>
    intro i j
    simp_rw [eq_comm]
    if h : i = j then
      simp only [h, ↓reduceIte]
      exact CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj ⊤)
    else
      rw [if_neg]
      · constructor; constructor
        case hom'.toFun => exact fun x => ⟨x.val⁻¹, inv_ne_zero x.property⟩
        case hom'.continuous_toFun =>
          apply Continuous.subtype_mk
          apply Continuous.inv₀
          · exact continuous_subtype_val
          · intro x
            exact x.property
      · assumption
  case V_id =>
    intro i
    simp only [reduceIte]
  case t_id =>
    intro i
    simp only [↓reduceDIte, eq_mpr_eq_cast, cast_eq]
    -- ⊢ ⇑(CategoryTheory.ConcreteCategory.hom
    --       (cast ⋯ (CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj ⊤)))) =
    --   id
    sorry
  case cocycle =>
    sorry
  case t_inter =>
    sorry

Does anyone know how to solve it?

[Kenny Lau]

you'll be advised to

1. not use tactics for data, which would lead to:
2. perhaps you can use Bool for J and then define V using matching

[Aaron Liu]

I will advertise file#Tactic/DepRewrite

[Michał Pacholski]

@Kenny Lau thanks! I took your advice, and I managed to complete the construction. I'll just post it here for completeness

import Mathlib
open CategoryTheory

noncomputable
def circleGlueDataCore : TopCat.GlueData.MkCore := by

  let puncturedLine := TopologicalSpace.Closeds.compl (TopologicalSpace.Closeds.singleton (0 : ℝ))

  let inversionHomeo : puncturedLine ≃ₜ puncturedLine := {
    toFun := fun x ↦ ⟨x.val⁻¹, inv_ne_zero x.property⟩,
    invFun := fun x ↦ ⟨x.val⁻¹, inv_ne_zero x.property⟩,
    left_inv := by intro x; simp [inv_inv, Subtype.coe_eta],
    right_inv := by intro x; simp [inv_inv, Subtype.coe_eta],
    continuous_toFun := by
      apply Continuous.subtype_mk
      apply Continuous.inv₀
      exact continuous_subtype_val
      intro x
      exact x.property,
    continuous_invFun := by
      apply Continuous.subtype_mk
      apply Continuous.inv₀
      exact continuous_subtype_val
      intro x
      exact x.property,
  }

  have inversionHomeo_involutive {x} : inversionHomeo (inversionHomeo x) = x := by
    dsimp [inversionHomeo]; simp only [inv_inv]

  let V : Bool → Bool → TopologicalSpace.Opens ℝ :=
    fun | true, true   => ⊤
        | true, false  => puncturedLine
        | false, true  => puncturedLine
        | false, false => ⊤

  let t : ∀ i j, (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (V i j) ⟶
    (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (V j i) :=
    fun | true, true => 𝟙 _
        | true, false => (TopCat.isoOfHomeo inversionHomeo).hom
        | false, true => (TopCat.isoOfHomeo inversionHomeo).hom
        | false, false => 𝟙 _

  constructor
  case J => exact Bool
  case U => exact fun _ => TopCat.of ℝ
  case V => exact V
  case t => exact t

  case V_id =>
    intro i
    cases i <;> rfl

  case t_id =>
    intro i
    cases i <;> rfl

  case t_inter =>
    intros i j k x hx_in_Vik
    cases i <;> cases j <;> cases k <;>
    dsimp [t, V, puncturedLine] at * <;>
    first | trivial | apply SetLike.coe_mem

  case cocycle =>
    intros i j k x hx_in_Vik
    cases i <;> cases j <;> cases k <;>
    dsimp [t, V] <;>
    rw [SetLike.coe_eq_coe] <;>
    exact inversionHomeo_involutive

@Aaron Liu Thank you for that reference, it got me through proving t_id in my original approach, but I got stuck at cocycle again. I'll need to spend some time learning this tool, it looks very powerful.