mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ + d₂ ≤ d₃ ↔ of p✝ ≤ d₃ ∧ d₂ ≤ d₃

Tactic:
induction d₂ using ManyOneDegree.ind_on

Goal state after:
case h.h
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ + of p✝ ≤ d₃ ↔ of p✝¹ ≤ d₃ ∧ of p✝ ≤ d₃
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

Tactic:
rmatch,

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ ((char a).deriv head✝).rmatch [] = true ↔ [head✝] = [a]
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ (char a).rmatch (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]

Tactic:
rmatch,

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ ((char a).deriv head✝).rmatch (head :: tail) = true ↔ head✝ :: head :: tail = [a]
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ ((char a).deriv head✝).rmatch (head :: tail) = true ↔ head✝ :: head :: tail = [a]

Tactic:
rmatch,

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ (((char a).deriv head✝).deriv head).rmatch tail = true ↔ head✝ :: head :: tail = [a]
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ (P + Q).rmatch (head✝ :: tail✝) = true ↔ P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true

Tactic:
rmatch,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail✝ = true ↔ P.rmatch tail✝ = true ∨ Q.rmatch tail✝ = true
P Q : RegularExpression α
⊢ ((P + Q).deriv head✝).rmatch tail✝ = true ↔ P.rmatch (head✝ :: tail✝) = true ∨ Q.rmatch (head✝ :: tail✝) = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.rmatch [] = true ∧ Q.rmatch [] = true

Tactic:
rmatch,

Goal state after:
case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.matchEpsilon = true ∧ Q.rmatch [] = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)

Tactic:
obtain ⟨a, L, rfl⟩ := L.exists_cons
  simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]
  suffices ∀ {L' R' l₁ l₂} (_ : List.Vector.toList (enc a) = List.reverseAux l₁ l₂),
      (Tape.move Dir.left)^[l₁.length]
      (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (List.Vector.toList (enc a)) R') by
    simpa only [List.length_reverse, Vector.toList_length] using! this (List.reverse_reverse _).symm
  intro _ _ l₁ l₂ e
  induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ P.star.rmatch (a :: x) = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
rmatch,

Goal state after:
case mp.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (P.star.deriv a).rmatch x = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝

Tactic:
rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ P.star.rmatch (a :: x) = true

Tactic:
rmatch,

Goal state after:
case mpr.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
hsum : a :: x = S.flatten
⊢ (P.star.deriv a).rmatch x = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (addBottom L) = L

Tactic:
simp only [addBottom, ListBlank.map_cons]

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons L.head
      (ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    L
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'

Tactic:
rw [← ih, Cont.then]

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

Goal state before:
pp: case fix
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'

Tactic:
rw [← ih, Cont.then]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullback.fst f π))

Tactic:
intro y

Goal state after:
P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : ↑X.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.fst f π)) a = y
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
rw [h, ← bind_pure_comp]; congr; funext v
  exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Precoherent (CompHausLike P)

Tactic:
have : Preregular (CompHausLike P) := preregular hs
  infer_instance

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
⊢ IsOpen[inst✝³] (Subtype.val '' V)

Tactic:
have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
⊢ IsOpen[inst✝³] (Subtype.val '' V)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
⊢ ∃ C,
    (∀ (i : β✝), IsClopen (C i)) ∧
      (∀ (i : β✝), Z i ⊆ C i) ∧ (∀ (i : β✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i),
      fun i ↦ by simpa using h3 (e.symm i), ?_,
      by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩

Goal state after:
case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
C : α✝ → Set X
h1 : ∀ (i : α✝), IsClopen (C i)
h2 : ∀ (i : α✝), (Z ∘ ⇑e) i ⊆ C i
h3 : ∀ (i : α✝), C i ⊆ (D ∘ ⇑e) i
h4 : ⋃ i, (D ∘ ⇑e) i ⊆ ⋃ i, C i
h5 : univ.PairwiseDisjoint C
⊢ ⋃ i, D i ⊆ ⋃ i, (C ∘ ⇑e.symm) i
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: X : CompHaus
Y : Profinite
f : X.toProfiniteObj ⟶ Y
y : ↑X.toProfiniteObj.toTop
⊢ (ConcreteCategory.hom
        ((fun g ↦ ConcreteCategory.ofHom { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ })
            ((fun f ↦
                ofHom (fun x ↦ True) ((TopCat.Hom.hom f.hom).comp { toFun := Quotient.mk'', continuous_toFun := ⋯ }))
              f)).hom)
      y =
    (ConcreteCategory.hom f.hom) y

Tactic:
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Goal state after:
X : CompHaus
Y : Profinite
f : X.toProfiniteObj ⟶ Y
y : ↑X.toTop
⊢ (ConcreteCategory.hom
        ((fun g ↦ ConcreteCategory.ofHom { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ })
            ((fun f ↦
                ofHom (fun x ↦ True) ((TopCat.Hom.hom f.hom).comp { toFun := Quotient.mk'', continuous_toFun := ⋯ }))
              f)).hom)
      (ConnectedComponents.mk y) =
    (ConcreteCategory.hom f.hom) (ConnectedComponents.mk y)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p [] = ([], o, L₂)
⊢ 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 := o, stk := update S k L₂ }

Tactic:
cases e
      rfl

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

Goal state before:
pp: case inl
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a
⊢ x ≠ Γ'.consₗ

pp: case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

pp: case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ

Tactic:
· rintro rfl
      cases trNat_natEnd _ _ h

Goal state after:
case inr.inl
a : ℕ
l : List ℕ
⊢ Γ'.cons ≠ Γ'.consₗ

case inr.inr
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList l
⊢ x ≠ Γ'.consₗ
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (CompHausLike.pullback.snd f g))

Tactic:
intro y

Goal state after:
X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom f)
y : ↑Y.toTop
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.snd f g)) a = y
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
f : Code
k : Cont
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) = elim ?neg.convert_6✝ [] [] (trContStack (Cont.fix f k))

Tactic:
convert! rfl

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:
intro y

Goal state after:
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
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)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.snd π π))) y

Tactic:
intro y

Goal state after:
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)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
y : ↑(pullback (G.map π) (G.map π))
⊢ (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
    (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.snd π π))) y
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X : LightCondSet
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦ X.coinducingCoprod ⟨⟨S, x⟩, a⟩

Tactic:
suffices ∀ (i : (T : LightProfinite.{u}) × X.obj.obj ⟨T⟩),
      Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
  rw [← continuous_sigma_iff]
  apply continuous_coinduced_rng

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
⊢ univ ⊆ ⋃ i, D i

Tactic:
intro y

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
y : Y
⊢ y ∈ univ → y ∈ ⋃ i, D i
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj P ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g =
    ((μIso (free R) P S'.toCondensed).hom ≫ (free R).map (P ◁ lightProfiniteToLightCondSet.map π)) ≫
      (μIso (free R) P S.toCondensed).inv ≫ g

Tactic:
← assoc

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj P ⊗ (free R).obj S.toCondensed ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g =
    (((μIso (free R) P S'.toCondensed).hom ≫ (free R).map (P ◁ lightProfiniteToLightCondSet.map π)) ≫
        (μIso (free R) P S.toCondensed).inv) ≫
      g