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

Goal state before:
pp: n : ℕ
⊢ decodeNat (encodeNat n) = n

Tactic:
by
  conv_rhs => rw [← Num.to_of_nat n]
  exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)

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

Goal state before:
pp: a b : PosNum
⊢ ↑(a + b).succ + ↑(a + b).succ = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
rw [succ_to_nat, add_to_nat a b]; simp [add_left_comm]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none

Tactic:
use l₁.length, l₂.length

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

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑n + ↑n).pred

Tactic:
rw [← to_nat_inj.1 h]

Goal state after:
n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
this : 0 < ↑n
⊢ Nat.bit false ↑n ≠ 0

Tactic:
dsimp [Nat.bit]

Goal state after:
n : PosNum
this : 0 < ↑n
⊢ ¬2 * ↑n = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ Nat.bit true ↑n ≠ 0

Tactic:
dsimp [Nat.bit]

Goal state after:
n : PosNum
⊢ ¬2 * ↑n + 1 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
apply to_nat_pos

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a

Tactic:
h₁,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ q (f a)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a

Tactic:
h₁,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ q (f a)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
let G : Fin n ↪ Fin n → Bool :=
    ⟨fun a b ↦ a = b, fun a b h ↦
      Bool.of_decide_true <| (congr_fun h b).trans <| Bool.decide_true rfl⟩

Goal state after:
Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b ↦ decide (a = b), inj' := ⋯ }
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (f ⟨a :: l₂, ⋯⟩) v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
    · dsimp [readAux, stepAux]
      simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
      cases a <;> rfl
    · rw [← ListBlank.append, IH]
      rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (map f (char a)).matches' = (Language.map f) (char a).matches'

Tactic:
rw [eq_comm]
    exact image_singleton

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

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
IH :
  SupportsStmt S q →
    (∀ q' ∈ writes q, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes (Stmt.move d q), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, supportsStmt_move, IH]

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

Goal state before:
pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

Tactic:
simp [Nat.testBit_add_one]

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

Goal state before:
pp: P✝ : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P✝
inst✝¹ : HasExplicitFiniteCoproduct X
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
this : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P')
⊢ PreservesFiniteCoproducts (toCompHausLike h)

Tactic:
exact preservesFiniteCoproducts_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }

Tactic:
refine Reaches₀.head ?_ IH
    simp only [Option.mem_def, TM1.step]
    rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]
    rfl

Goal state after:
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 Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
⊢ ∀ ⦃a₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ⦄,
    TrCfg c₁ a₂ →
      match TM2.step M c₁ with
      | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) a₂ b₂
      | none => TM1.step (tr M) a₂ = none

Tactic:
c₂

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
⊢ TrCfg c₁ c₂ →
    match TM2.step M c₁ with
    | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
    | none => TM1.step (tr M) c₂ = none
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: a b : Λ'
⊢ Decidable (a = b)

Tactic:
induction a generalizing b <;> cases b
  case move.move p k₁ k₂ q _ p' k₁' k₂' q' =>
    exact decidable_of_iff' (p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q') (by simp)
  case clear.clear p k q _ p' k' q' => exact decidable_of_iff' (p = p' ∧ k = k' ∧ q = q') (by simp)
  case copy.copy q _ q' => exact decidable_of_iff' (q = q') (by simp)
  case push.push k s q _ k' s' q' => exact decidable_of_iff' (k = k' ∧ s = s' ∧ q = q') (by simp)
  case read.read f _ f' => exact decidable_of_iff' (∀ a, f a = f' a) (by simp [funext_iff])
  case succ.succ q _ q' => exact decidable_of_iff' (q = q') (by simp)
  case pred.pred q₁ q₂ _ _ q₁' q₂' => exact decidable_of_iff' (q₁ = q₁' ∧ q₂ = q₂') (by simp)
  case ret.ret k k' => exact decidable_of_iff' (k = k') (by simp)
  all_goals exact .isFalse (by rintro ⟨⟨⟩⟩)

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

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v ↦ do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc, pure_bind]

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₂
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun v ↦ k.eval (ns.headI :: v)) v

Tactic:
exact IH

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

Goal state before:
pp: case pos
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : v.headI = 0
⊢ eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail

Tactic:
exact IH

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop

Tactic:
by
        change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
        exact Subtype.totallyDisconnectedSpace

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

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

Tactic:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s
    exact ⟨_, h₁, TransGen.head rfl h₂⟩

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)
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

Tactic:
h₁,

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 (pullback.fst (G.map π) (G.map π)))
        ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)) =
    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.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ f ↑↑x = Fiber.image f (Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))

Tactic:
Fiber.mk_image,

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ f ↑↑x = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
by
  rw [← S.proj_comp_transitionMap n]
  rfl

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
by
  have := functor_initial c hc
  have : ((StructuredArrow.toCostructuredArrow toProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
  exact Functor.final_comp (functor c).op _

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h :
  ∀ (a : Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
⊢ x = y

Tactic:
apply injective_of_mono (X.mapIso (sigmaIso f).op).hom
  apply injective_of_mono (sigmaComparison X (fun a ↦ (fiber f a).1))
  ext a
  specialize h a
  rw [← sigmaComparison_comp_sigmaIso] at h
  exact h

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ Fiber.image (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a =
    Fiber.image (⇑f)
      (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a)))

Tactic:
exact image_eq_image_mk (g := g.unop) (a := a)

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
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 _ _

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f✝ : X ⟶ Y
X✝ Y✝ : LightCondMod R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((LightCondensed.forget R).map f)

Tactic:
by
    rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢
    exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mp hf

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) ((ihomPoints R P A S').symm g') =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g

Tactic:
rw [ihom_map_val_app]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ (ihomPoints R P B S').symm ((ihomPoints R P A S') ((ihomPoints R P A S').symm g') ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ Continuous f

Tactic:
rw [continuous_coinduced_dom, continuous_sigma_iff]

Goal state after:
X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ ∀ (i : (S : CompHaus) × X.obj.obj (Opposite.op S)), Continuous fun a ↦ (f ∘ X.coinducingCoprod) ⟨i, a⟩
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k
⊢ Part.fix f x = Fix.approx f k.succ x

Tactic:
replace hk : Nat.find h' = k + (@Upto.zero p).val := hk

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f k.succ x
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = (fun x1 x2 ↦ x1 ++ x2) <$> traverse f [] <*> traverse f bs

Tactic:
simp [functor_norm]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a

Tactic:
exact ⟨_, hh⟩

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ ∃ i, b ∈ approx (⇑f) i a

Tactic:
exact ⟨_, hh⟩

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a

Tactic:
induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ F = Equiv.functor eqv

Tactic:
cases F

Goal state after:
case mk
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := map✝, mapConst := mapConst✝ } = Equiv.functor eqv
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
n m : OnePoint X
⊢ Continuous fun x ↦ (π ↑(x n)).1

pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace ↑(Prod.snd ∘ π ⁻¹' {x})
n m : OnePoint X
⊢ Continuous fun x ↦ (π ↑(x m)).1

Tactic:
all_goals fun_prop

Goal state after: