mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ (true ^^ v.testBit i) = false

Tactic:
hi

Goal state after:
case inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ (true ^^ true) = false
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 1 / 2 * log x ≤ log u

Tactic:
calc
    1 / 2 * Real.log x = Real.log x + (-1 / 2) * Real.log x := by ring
      _ ≤ Real.log x + Real.log b := by grind
      _ = Real.log (b * x) := by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]
      _ ≤ Real.log u := by gcongr; exact hu.1

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

Goal state before:
pp: case inr.inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ (true ^^ v.testBit i) = false

Tactic:
hi

Goal state after:
case inr.inl.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ (true ^^ true) = false
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
0 < b * x := by positivity
         _ ≤ u := by exact hu.1

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

Goal state before:
pp: case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ v.testBit i) = false

Tactic:
hi

Goal state after:
case inr.inr.refine_1
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ true) = false
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)

Tactic:
rw [add_comm]

Goal state after:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption

Tactic:
induction l with

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

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]

Tactic:
· intro h
    rw [reduceOption_eq_append_iff] at h
    obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h
    rw [reduceOption_eq_singleton_iff] at hl₂
    obtain ⟨m, n, hl₂⟩ := hl₂
    use l₁ ++ replicate m none, replicate n none
    simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = (filter Option.isSome l).length

Tactic:
induction l with

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
stepSet,

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ ⋃ s ∈ S, M.εClosure (M.step s (some a)) ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
stepSet,

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ ⋃ s ∈ ∅, M.εClosure (M.step s (some a)) = ∅
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
(choice (PosNum.transfer "transfer") (Num.transfer "transfer"))

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
⊢ L ∈ Set.range L.leftQuotient

Tactic:
exists []

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

Goal state before:
pp: f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
⊢ ∀ (m n : Num), ↑(f m n) = Nat.bitwise g ↑m ↑n

Tactic:
intro m n

Goal state after:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : Num
⊢ ↑(f m n) = Nat.bitwise g ↑m ↑n
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
L R : ListBlank Γ
⊢ map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)

Tactic:
simp only [Tape.mk', Tape.map, ListBlank.head_map,
    ListBlank.tail_map]

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

Goal state before:
pp: case left.right
Γ : 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
⊢ default.2 ∈ Finset.univ

Tactic:
apply Finset.mem_univ

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v ((Tape.move d)^[i + 1] T)

Tactic:
iterate_succ

Goal state after:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
x : List α
⊢ (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
induction x generalizing P Q with
  | nil =>
    rw [rmatch]; simp only [matchEpsilon]
    constructor
    · intro h
      refine ⟨[], [], rfl, ?_⟩
      rw [rmatch, rmatch]
      rwa [Bool.and_eq_true_iff] at h
    · rintro ⟨t, u, h₁, h₂⟩
      obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
      repeat rw [rmatch] at h₂
      simp [h₂]
  | cons a x ih =>
    rw [rmatch]; simp only [deriv]
    split_ifs with hepsilon
    · rw [add_rmatch_iff, ih]
      constructor
      · rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩
      · rintro ⟨t, u, h, hP, hQ⟩
        rcases t with - | ⟨b, t⟩
        · right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ
        · left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
    · rw [ih]
      constructor <;> rintro ⟨t, u, h, hP, hQ⟩
      · exact ⟨a :: t, u, by tauto⟩
      · rcases t with - | ⟨b, t⟩
        · contradiction
        · rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

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
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q

Tactic:
cases s <;> simp only [trStmts₁, stRun]

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

Goal state before:
pp: Γ : 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 Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := T })
    (step M { l := l₁, var := v, Tape := T })

Tactic:
by
    obtain ⟨L, R, rfl⟩ := T.exists_mk'
    rcases l₁ with - | l₁
    · exact rfl
    suffices ∀ q R, 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))) by
      refine TransGen.head' rfl ?_
      rw [trTape_mk']
      exact this _ R
    clear R l₁
    intro q R
    induction q generalizing v L R with
    | move d q IH =>
      cases d <;>
          simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0] <;>
        apply IH
    | write f q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
      refine ReflTransGen.head rfl ?_
      obtain ⟨a, R, rfl⟩ := R.exists_cons
      rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]
      simpa using! IH ..
    | load a q IH =>
      simp only [trNormal, stepAux_read dec enc0 encdec]
      apply IH
    | branch p q₁ q₂ IH₁ IH₂ =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]
      grind
    | goto l =>
      simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']
      apply ReflTransGen.refl
    | halt =>
      simp only [trNormal, stepAux, trCfg,
        trTape_mk']
      apply ReflTransGen.refl

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

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

Tactic:
trans

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

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.126 = ↑(pos m.bit1) >>> (n + 1)

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
trans

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

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.171 = ↑(pos m.bit0) >>> (n + 1)

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b

Tactic:
ext z

Goal state after:
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : ↑Z.toTop
⊢ (ConcreteCategory.hom a) z = (ConcreteCategory.hom b) z
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case none
α : Type u_1
p : α → Bool
a : α
L l₁ l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) none
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, none, l₂)

Tactic:
rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨⟨⟩, rfl⟩

Goal state after:
case none.cons
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ a :: L, p x = false
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: L, none, [])
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun z ↦ Classical.choose ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
⊢ ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
have ht : Continuous t := continuous_of_discreteTopology

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun z ↦ Classical.choose ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
⊢ ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
⊢ Injective ρ

Tactic:
intro x₁ x₂ hρx

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
⊢ x₁ = x₂
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
by_cases! Un : U = ∅

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U = ∅
⊢ IsOpen (closure U)

case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)
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)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
g✝ : Y✝ ⟶ B✝
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom f✝) → HasExplicitPullback f✝ g✝

Tactic:
hi

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi✝ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
g✝ : Y✝ ⟶ B✝
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f✝)
⊢ HasExplicitPullback f✝ g✝
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert! clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH

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

Goal state before:
pp: case refine_1
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
v' : List ℕ
hv : v' ∈ c.eval v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a ∈ c.eval v, halt a = x

Tactic:
exact ⟨_, hv, hc₁.symm⟩

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_2
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 π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : (yonedaPresheaf G X).obj (op Z)
ha :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
⊢ ∃ a_1,
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a_1 = ⟨a, ha⟩

Tactic:
simp only [yonedaPresheaf, comp, Quiver.Hom.unop_op, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, mk.injEq, Set.mem_ofPred_eq] at ha

Goal state after:
case refine_2
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 π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : (yonedaPresheaf G X).obj (op Z)
ha✝ :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
ha : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(TopCat.Hom.hom (G.map (pullback.snd π π)))
⊢ ∃ a_1,
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a_1 =
      ⟨a, ha✝⟩
Module: Mathlib.Condensed.Light.TopCatAdjunction

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

Tactic:
rw [← continuous_sigma_iff]

Goal state after:
X : LightCondSet
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous X.coinducingCoprod
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj.obj S
⊢ ∀ (i : (T : LightProfinite) × X.obj.obj (Opposite.op T)), Continuous fun a ↦ LightCondSet.coinducingCoprod✝ X ⟨i, a⟩

Tactic:
rw [← continuous_sigma_iff]

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj.obj S
⊢ Continuous (LightCondSet.coinducingCoprod✝ X)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X : CondensedSet
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ ∀ (i : (T : CompHaus) × X.obj.obj (Opposite.op T)), Continuous fun a ↦ X.coinducingCoprod ⟨i, a⟩

Tactic:
rw [← continuous_sigma_iff]

Goal state after:
X : CondensedSet
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous X.coinducingCoprod