mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.CompHaus.Projective

Goal state before:
pp: case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.nil.refl
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := none, stk := update S k [] }

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option.refine_5.none
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
⊢ none ∈ univ → ∀ ⦃y : Option I⦄, y ∈ univ → none ≠ y → (Disjoint on C) none y

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
refine ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩,
    fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩

Goal state after:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
⊢ X '' ⋂ c, ↑c = univ
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
x : X
hx : ∃ i, x ∈ D i
hx0 : x ∉ C0
hxD : x ∈ D none
⊢ x ∈ ⋃ i, C' i

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case neg.none
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
x : X
hx0 : x ∉ C0
hxD : x ∉ D none
hi : x ∈ D none
⊢ ∃ i, x ∈ C i

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
x : X
hx0 : x ∉ C0
hxD : x ∉ D none
j : I
hi : x ∈ D (some j)
⊢ x ∈ D' j

Tactic:
grind

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d } =
    { l := some q, var := none, stk := elim (Γ'.bit1 :: Γ'.cons :: (trNum Num.zero ++ [Γ'.cons]).tail) [] c d }

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := ?m.498, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ some Γ'.bit1 = ?m.498

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ (bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.bit1) then
      { l := some q.succ, var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
        stk := elim (trPosNum m.bit0 ++ [Γ'.cons]).tail (Γ'.bit0 :: l₁) c d }
    else
      bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.cons) then
        { l := some (unrev q), var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
          stk := elim (Γ'.bit1 :: Γ'.cons :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d }
      else
        { l := some (unrev q), var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
          stk := elim (Γ'.bit1 :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d }) =
    { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d }

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.pos.bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ (bif decide ((trPosNum m.bit1.succ).head?.getD Γ'.cons = Γ'.bit0) then
      { l := some (q₁.pred q₂), var := some ((trPosNum m.bit1.succ).head?.getD Γ'.cons),
        stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit1 :: l₁) c d }
    else
      bif
          match (trPosNum m.bit1.succ).head?.getD Γ'.cons with
          | Γ'.consₗ => true
          | Γ'.cons => true
          | x => false then
        { l := some q₁, var := some ((trPosNum m.bit1.succ).head?.getD Γ'.cons),
          stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d }
      else
        bif
            match (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?.getD Γ'.consₗ with
            | Γ'.consₗ => true
            | Γ'.cons => true
            | x => false then
          { l := some (unrev q₂), var := (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?,
            stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d }
        else
          { l := some (unrev q₂), var := (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?,
            stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit0 :: l₁) c d }) =
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.pos.bit0
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ (bif natEnd Γ'.bit1 then { l := some q₁, var := some Γ'.bit1, stk := elim (a :: (l ++ Γ'.cons :: trList v)) l₁ c d }
    else { l := some (unrev q₂), var := some a, stk := elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d }) =
    { l := some (unrev q₂), var := some a, stk := elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d }

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid) a✝)) = ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_4.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim ?tail.convert_7 [] [] (trContStack k)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (g.comp f) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = (map g h1 ∘ map f h2) (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk (⇑A.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk (⇑A'.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A'.toSetoid) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ x✝¹.proj ⁻¹' {Qs x✝¹} ⊆ x✝.proj ⁻¹' {Qs x✝}

Tactic:
rw [← compat _ _ h]
    exact fiber_subset_ofLE _ _

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.cons fs) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]

Goal state after:
Module: Mathlib.Condensed.AB

Goal state before:
pp: A : Type u_1
J : Type u_2
inst✝⁸ : Category.{v_1, u_1} A
inst✝⁷ : Category.{v_2, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
exact HasExactColimitsOfShape.domain_of_functor _ e.functor

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁.refine_1
fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) rev = []

Tactic:
rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁.refine_2.refine_5.refine_1
fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ update
      (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
        ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
      main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) rev =
    []

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
j : J
⊢ ConcreteCategory.ofHom (TopCat.Hom.hom x✝.hom) ≫ (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j =
    ConcreteCategory.ofHom (TopCat.Hom.hom (x✝ ≫ (limitCone F).π.app j).hom)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
x✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x ↦ op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ x✝¹ ((ConcreteCategory.hom (opCoproductIsoProduct X).inv.unop) ((ConcreteCategory.hom (Sigma.ι X x✝)) a✝)) =
    x✝¹
      ((ConcreteCategory.hom (opCoproductIsoProduct X).inv.unop)
        ((ConcreteCategory.hom (TopCat.sigmaIsoSigma X).inv) ⟨x✝, a✝⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ TopCat
Y : Type w'
inst✝ : TopologicalSpace Y
x✝ : ℕ
K : Discrete (Fin x✝) ⥤ TopCatᵒᵖ
α✝ : Type
X : α✝ → TopCat
⊢ IsIso (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x))

Tactic:
rw [piComparison_fac]; infer_instance

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y✝ : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y✝
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y✝), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
y : ↑(pullback (G.map π) (G.map π))
⊢ (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
    (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.fst π π))) y

Tactic:
rfl

Goal state after: