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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ StrictAnti (∑ c, fun p ↦ a c * b c ^ p)

Tactic:
refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms

Goal state after:
case terms
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ x ∈ univ, StrictAnti fun p ↦ a x * b x ^ p
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i, a i * b i ^ p

Tactic:
refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
⊢ 0 ≤ a i * b i ^ p
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ∈ Set.Icc (b * x) (1 * x)

Tactic:
simp only [one_mul, Set.mem_Icc]

Goal state after:
b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u ∧ u ≤ x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ C * T n = C * (∑ i, a i * T (r i n) + g ↑n)

Tactic:
by grind [AkraBazziRecurrence]

Goal state after:
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: m n : ℕ
⊢ n < 2 ^ m ↔ n.size ≤ m

Tactic:
size_le

Goal state after:
m n : ℕ
⊢ n < 2 ^ m ↔ n < 2 ^ m
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
(f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit b n = 0

Tactic:
rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
conv_lhs => rw [← bit_bodd_div2 n]

Goal state after:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case zero
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ 0 < m

Tactic:
rw [Nat.pos_iff_ne_zero]

Goal state after:
case zero
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ m ≠ 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0

Tactic:
simp only [Nat.add_zero, ofNat'_zero, add_zero]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.evalFrom start = List.foldl M.stepSet start

Tactic:
εNFA.evalFrom,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet (M.toεNFA.εClosure start) = List.foldl M.stepSet start
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
⊢ (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))

Goal state after:
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 Γ
this : ∀ (i : ℕ) (L : Tape (?m.37 i)), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail

Tactic:
refine (Eq.symm ?_).trans (this n _)
    simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
      ListBlank.tail_cons]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
    clear star_rmatch_iff
    constructor
    · rcases x with - | ⟨a, x⟩
      · intro _h
        use []; dsimp; tauto
      · rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
        rw [IH _ hwf] at hu
        rcases hu with ⟨S', hsum, helem⟩
        use (a :: t) :: S'
        constructor
        · simp [hs, hsum]
        · intro t' ht'
          cases ht' with
          | head ht' =>
            simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht
          | tail _ ht' => exact helem t' ht'
    · rintro ⟨S, hsum, helem⟩
      rcases x with - | ⟨a, x⟩
      · rfl
      · rw [rmatch, deriv, mul_rmatch_iff]
        rcases S with - | ⟨t', U⟩
        · exact ⟨[], [], by tauto⟩
        · obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

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

Goal state before:
pp: case succ
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
obtain ⟨cg, hg₁⟩ := hg 0
    obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
    exact
      ⟨cons cg cl, fun v => by
        simp [Vector.mOfFn, hg₁, hl]
        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
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
      TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
            update (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
              none)
          (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
by
          erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
            Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
            addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
            stk_nth_val _ (hL k), e,
            show (List.cons hd tl).reverse[tl.length]? = some hd by
              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
            List.head?, List.tail]

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
a : α
⊢ Function.Injective ⇑(ConcreteCategory.hom (ι X a))

Tactic:
intro x y hxy

Goal state after:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
hxy : (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y
⊢ x = y
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
simp only [Cont.then, stepRet, *]

Goal state after:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝² (Cont.cons₂ v (a✝.then k')) a✝¹ = (stepNormal a✝² (Cont.cons₂ v a✝) a✝¹).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepRet ((Cont.comp a✝¹ a✝).then k') v = (stepRet (Cont.comp a✝¹ a✝) v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Goal state after:
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepNormal a✝¹ (a✝.then k') v = (stepNormal a✝¹ a✝ v).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepRet ((Cont.fix a✝¹ a✝).then k') v = (stepRet (Cont.fix a✝¹ a✝) v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Goal state after:
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ (if v.headI = 0 then (stepRet a✝ v.tail).then k' else stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail) =
    (if v.headI = 0 then stepRet a✝ v.tail else stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case halt
k' : Cont
v : List ℕ
⊢ stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Goal state after:
case halt
k' : Cont
v : List ℕ
⊢ stepRet k' v = (Cfg.halt v).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₂
k' : Cont
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
⊢ stepRet ((Cont.cons₂ a✝¹ a✝).then k') v = (stepRet (Cont.cons₂ a✝¹ a✝) v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

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

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h) y).down = ((ConcreteCategory.hom g) y).down
⊢ False

Tactic:
change 1 = ite _ _ _ at H

Goal state after:
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : 1 = if y ∈ V then 0 else 1
⊢ False
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
← CompHaus.epi_iff_surjective

Goal state after:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
⊢ Epi f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (↑n).succ ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (↑n).succ ++ Γ'.cons :: trList tail✝).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trNum (↑n).succ ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (↑n).succ ++ Γ'.cons :: trList tail✝).tail =
        (trNum (↑n).succ).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Tactic:
Num.succ,

Goal state after:
case cons.succ
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos (↑n).succ') ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos (↑n).succ')).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X✝ Y✝ : LightDiagram'
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : LightDiagram'.toLightFunctor.map a₁✝ = LightDiagram'.toLightFunctor.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    apply InducedCategory.homEquiv.injective
    apply InducedCategory.homEquiv.symm.injective 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 π π)))
⊢ Function.FactorsThrough ⇑a ⇑(ConcreteCategory.hom (G.map π))

Tactic:
intro x y hxy

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
⊢ a x = a y
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
x : ↑(G.obj (unop (op B)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a x = b x

Tactic:
← hy

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
x : ↑(G.obj (unop (op B)))
y : ↑(G.obj Z)
hy : (ConcreteCategory.hom (G.map π)) y = x
⊢ a ((ConcreteCategory.hom (G.map π)) y) = b ((ConcreteCategory.hom (G.map π)) y)
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
y : ↑(Set.range ⇑l)
hy : (fun x ↦ ⇑l ⁻¹' {↑x}) y = ↑x
⊢ IsCompact ↑x

Tactic:
← hy

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
y : ↑(Set.range ⇑l)
hy : (fun x ↦ ⇑l ⁻¹' {↑x}) y = ↑x
⊢ IsCompact ((fun x ↦ ⇑l ⁻¹' {↑x}) y)
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ functorToPresheaves.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).hom =
    𝟙 (functorToPresheaves.obj X)

Tactic:
ext ⟨S⟩ (f : LocallyConstant _ X)
  simp only [Functor.id_obj, functor_obj_obj_obj, functorToPresheaves_obj_obj, Functor.comp_obj,
    Functor.flip_obj_obj, ObjectProperty.ι_obj, unit_app, NatTrans.comp_app,
    functorToPresheaves_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.toFun_apply,
    CategoryTheory.comp_apply, TypeCat.Fun.coe_mk, NatTrans.id_app, id_apply]
  simp only [counit]
  have := CompHausLike.preregular hs
  apply presheaf_ext
    (X := ((functor P hs).obj X).obj) (Y := ((functor.{u, w} P hs).obj X).obj)
      (f.map ((unit P hs).app X))
  intro a
  erw [incl_of_counitAppApp]
  simp only [functor_obj_obj_obj, Functor.id_obj, Functor.comp_obj, Functor.flip_obj_obj,
    ObjectProperty.ι_obj, unit_app, counitAppAppImage, functor_obj_obj_map,
    Quiver.Hom.unop_op, ConcreteCategory.hom_ofHom]
  ext x
  erw [← map_eq_image _ a x]
  rfl

Goal state after: