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

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

Tactic:
rw [rmatch] at h₂

Goal state after:
case nil.mpr
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.rmatch [] = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
rw [rmatch] at h₂

Goal state after:
case nil.mpr
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
rw [rmatch] at h₂

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

Goal state before:
pp: case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ ∃ a ∈ S, M default ∈ TM1.stmts₁ (M a)

Tactic:
exact ⟨_, ss.1, TM1.stmts₁_self⟩

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

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (true ::ᵥ v)))

Tactic:
apply IH

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (false ::ᵥ v)))

Tactic:
apply IH

Goal state after:
case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case char
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
x : List α
⊢ (char a✝).rmatch x = true ↔ x ∈ (char a✝).matches'

Tactic:
| char =>

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

Goal state before:
pp: case some.move.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L.tail (ListBlank.cons L.head R)))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L.tail (ListBlank.cons L.head R))))

Tactic:
apply IH

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

Goal state before:
pp: case some.move.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 (ListBlank.cons R.head L) R.tail))
    (trCfg enc enc0 (stepAux q v (Tape.move Dir.right (Tape.mk' L R))))

Tactic:
apply IH

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

Goal state before:
pp: case some.load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (Stmt.load (fun x s ↦ a R.head s) (trNormal dec q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))

Tactic:
apply IH

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.126

Tactic:
apply IH

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.171

Tactic:
apply IH

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

Tactic:
rcases e : M q T.1 with - | val

Goal state after:
case none
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
val : Λ × TM0.Stmt Γ
e : M q T.head = some val
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((cons₁ a✝² a✝¹ a✝).then k').eval v = (cons₁ a✝² a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, *]

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

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k' : K'
q' : Λ'
⊢ Decidable (clear p k q = clear p' k' q')

Tactic:
exact decidable_of_iff' (p = p' ∧ k = k' ∧ q = q') (by simp)

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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst✝¹] U
hx : x ∈ U ∧ y ∉ U
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝¹] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst✝¹] U
hy : y ∈ U ∧ x ∉ U
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝¹] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
· choose V hV using h.isOpen_iff.mp hU₀ x hx.1
    exact ⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2,
      (union_compl_self V).superset, disjoint_compl_right⟩

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst✝¹] U
hy : y ∈ U ∧ x ∉ U
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝¹] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
⊢ Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Tactic:
intro c₁ c₂ h
  obtain @⟨- | l, v, S, L, hT⟩ := h; · constructor
  rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _
  · exact ⟨b, c, TransGen.head' rfl r⟩
  simp only [tr]
  generalize M l = N
  induction N using stmtStRec generalizing v S L hT with
  | run k s q IH => exact tr_respects_aux M hT s @IH
  | load a _ IH => exact IH _ hT
  | branch p q₁ q₂ IH₁ IH₂ =>
    unfold TM2.stepAux trNormal TM1.stepAux
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
  | goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
  | halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

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

Goal state before:
pp: case refine_1.inl.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ s q✝))

Tactic:
cases s
        · exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
        · exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
        · exact ⟨⟨fun _ _ ↦ hret, fun _ _ ↦ hret⟩, fun _ _ ↦ hgo⟩

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ HasExplicitPullbacksOfInclusions fun Y ↦ ExtremallyDisconnected ↑Y

Tactic:
by
  apply CompHausLike.hasPullbacksOfInclusions
  intro _ _ _ _ _ hi
  exact ⟨extremallyDisconnected_pullback _ hi⟩

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

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

Tactic:
refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩

Goal state after:
case zero'
k : Cont
v : List ℕ
s : Option Γ'
⊢ { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList (0 :: v)) [] [] (trContStack k) } ∈
    TM2.step tr { l := some (trNormal Code.zero' (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
f : Code
IH :
  ∀ (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₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal f.fix k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal f.fix (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
apply IH

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ⋃₀ (Subtype.val '' ↑⋯.choose) = t.carrier

Tactic:
(this t).choose_spec,

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s ↦ ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ⋃₀ (Subtype.val '' ↑⋯.choose) = ⋃₀ (Subtype.val '' ↑⋯.choose)
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)
y : ↑Y.toTop
x : ↑X.toTop
hx : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.snd f g)) a = y

Tactic:
exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

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

Goal state before:
pp: case ret
q' : Λ'
k✝ : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k✝) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k✝)

Tactic:
| ret =>

Goal state after:
case ret
q' : Λ'
k✝ : Cont'
⊢ q' ∈ trStmts₁ (Λ'.ret k✝) → trStmts₁ q' ⊆ trStmts₁ (Λ'.ret k✝)
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
⊢ a x = a y

Tactic:
have h₂ : ∀ y, G.map (pullback.snd _ _) ((PreservesPullback.iso G π π).inv y) =
      pullback.snd (G.map π) (G.map π) y := by
    simp only [← PreservesPullback.iso_inv_snd]; intro y; rfl

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
h₂ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y
⊢ a x = a y
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : trStmts₁ (Λ'.ret k✝) ⊆ S
⊢ Supports (trStmts₁ (Λ'.ret k✝)) S

Tactic:
| ret =>

Goal state after:
case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : trStmts₁ (Λ'.ret k✝) ⊆ S
⊢ Supports (trStmts₁ (Λ'.ret k✝)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S

Tactic:
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_

Goal state after:
case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
H' : trStmts₁ (trNormal (f.case g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
x✝ : codeSupp' f k ∪ codeSupp' g k ⊆ S
⊢ Supports (codeSupp' f k ∪ codeSupp' g k) S
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
x : ↑X✝.toTop
hx : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g.down.hom) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y

Tactic:
exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

Goal state after:
Module: Mathlib.Condensed.Light.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : LightProfinite
g : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
x : ↑X✝.toTop
hx : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g.hom) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g)) a = y

Tactic:
exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
rw [coherentTopology.isLocallySurjective_iff,
    regularTopology.isLocallySurjective_iff]

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (Y.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op S))) x)

Tactic:
exact continuous_coinducingCoprod Y _

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f (g <$> x) = traverse (f ∘ g) x

Tactic:
rw [@map_eq_traverse_id t _ _ _ _ g]

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ op (↾flip (List.foldl f) (FreeMonoid.toList (x✝ * y✝))) =
    op (↾flip (List.foldl f) (FreeMonoid.toList x✝)) * op (↾flip (List.foldl f) (FreeMonoid.toList y✝))

Tactic:
simp only [FreeMonoid.toList_mul, List.foldl_append, Function.flip_def]

Goal state after:
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ op (↾fun a ↦ List.foldl f (List.foldl f a (FreeMonoid.toList x✝)) (FreeMonoid.toList y✝)) =
    op (↾fun a ↦ List.foldl f a (FreeMonoid.toList x✝)) * op (↾fun a ↦ List.foldl f a (FreeMonoid.toList y✝))
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ ∀ (x : Fin2 (n + 1)), x ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

Tactic:
rintro (_ | i) <;> simp [compl]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ f P n α ⊚ g P n α = TypeVec.id

Tactic:
ext i ⟨x, _⟩

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) i ⟨x, property✝⟩) = ↑(TypeVec.id i ⟨x, property✝⟩)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)

Tactic:
ext i ⟨x, _⟩

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (α.PredLast' P i x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α i ⟨x, property✝⟩)