mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
z : ℝ
hz : z ∈ Set.Ioi 1
⊢ z ≠ 0

Tactic:
rw [Set.mem_Ioi] at hz

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
z : ℝ
hz : 1 < z
⊢ z ≠ 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_1.left
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑fun n ↦ (unpair n).1

Tactic:
| left =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2.left
⊢ Nat.Partrec left.eval

Tactic:
| left =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2.rfind'
cf : Code
pf : Nat.Partrec cf.eval
⊢ Nat.Partrec cf.rfind'.eval

Tactic:
| rfind' cf pf =>

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x : ℕ
h : ∃ a ∈ cg.eval n, x ∈ cf.eval a
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
rcases h with ⟨y, hy, hx⟩
    rcases hg hy with ⟨k₁, hk₁⟩; rcases hf hx with ⟨k₂, hk₂⟩
    refine ⟨max k₁ k₂, ?_⟩
    exact
      ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩

Goal state after:
case rfind'.succ
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ (⨆ i, m ^ i) * n ≤ l

Tactic:
iSup_mul,

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ ⨆ i, m ^ i * n ≤ l
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse

Tactic:
rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : Code → ℕ →. ℕ
hf : Partrec₂ f
cf : Code
ef : cf.eval = fun n ↦ (↑(decode n)).bind fun a ↦ Part.map encode ((fun p ↦ f p.1 p.2) a)
c : Code
e : (cf.curry (encode c)).eval = c.eval
n : ℕ
⊢ c.eval n = f c n

Tactic:
simp [e.symm, ef, Part.map_id']

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

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ w✝¹.reduceOption ++ (some a :: w✝).reduceOption = l' ++ [a]

Tactic:
reduceOption_cons_of_some,

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ w✝¹.reduceOption ++ a :: w✝.reduceOption = l' ++ [a]
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1

Tactic:
apply Nat.lt_succ_self

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case prim
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
hf : Primrec' f✝
⊢ Partrec ↑f✝

Tactic:
| prim hf =>

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : ComputablePred p
⊢ Computable fun a ↦ decide (p a)

Tactic:
convert! hp.choose_spec

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c

Tactic:
rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
O O' : Set (ℕ →. ℕ)
f : ℕ →. ℕ
hO : ∀ g ∈ O, Nat.RecursiveIn O' g
⊢ Nat.RecursiveIn O' fun n ↦ ↑(Option.some (unpair n).1)

Tactic:
| left =>

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
⊢ Nat.Partrec fun n ↦ ↑(Option.some (unpair n).1)

Tactic:
| left =>

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case left
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
⊢ Nat.RecursiveIn O ↑fun n ↦ (unpair n).1

Tactic:
| left =>

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
rw [rmatch, rmatch]

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

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append (b :: l₂) R'✝)

Tactic:
simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

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 Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
this :
  ∀ (q : Stmt Γ Λ σ) (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)))
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := some l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R })

Tactic:
by
      refine TransGen.head' rfl ?_
      rw [trTape_mk']
      exact this _ R

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

Goal state before:
pp: case pos
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 : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : i = (S k).length
⊢ some (f v) = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]

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

Goal state before:
pp: case prim
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
hf : Nat.Primrec' f✝
⊢ ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> ↑f✝ v

Tactic:
| prim hf =>

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

Goal state before:
pp: case pop.nil
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) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k [] k_1)).reverse) ∧
      (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (∅.head.2 k))
            (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))

Tactic:
rw [← e, Function.update_eq_self]

Goal state after:
case pop.nil
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) → σ
e : S k = []
⊢ ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
      (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
        else
          TM1.stepAux q (f v (∅.head.2 k))
            (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
        TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L'))
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

Goal state after:
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) }
⊢ { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) } ∈
    TM1.step (tr M) { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace X

Tactic:
constructor
  rintro x - y - hxy
  choose U hU using exists_isOpen_xor_mem hxy
  obtain ⟨hU₀, hU₁⟩ := hU
  rcases hU₁ with hx | hy
  · 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⟩
  · choose V hV using h.isOpen_iff.mp hU₀ y hy.1
    exact ⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
      (union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩

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

Goal state before:
pp: case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by
      rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]
      exact PairwiseDisjoint.subset Z_disj (by simp)

Goal state after:
case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_3
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
p✝ : σ → Bool
q₁✝ 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')
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 (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝, x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)

Tactic:
rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]

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

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

pp: case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
· dsimp [Function.Surjective]
    contrapose!
    rintro ⟨y, hy⟩ hf
    let C := Set.range f
    have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
    let U := Cᶜ
    have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'
    have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
    classical
      let Z := of (ULift.{u} <| Fin 2)
      let g : Y ⟶ Z := ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
      let h : Y ⟶ Z := ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
      have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, ConcreteCategory.hom_ofHom,
          ContinuousMap.coe_mk, Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]
      apply_fun fun e => (e y).down at H
      dsimp [g, LocallyConstant.ofIsClopen] at H
      rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
      exact top_ne_bot H

Goal state after:
case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.Category.Profinite.AsLimit

Goal state before:
pp: case refine_2
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a_1 = a

Tactic:
obtain ⟨b, hb⟩ :=
          DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)

Goal state after:
case refine_2
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
b : ↑X.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toTop), Q.proj b = ↑a Q
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a_1 = a
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
⊢ s = t

Tactic:
ext1

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) := ⋯
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ↑s = ↑t
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

pp: case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
· -- Note: in mathlib3 `contrapose` saw through `Function.Surjective`.
    dsimp [Function.Surjective]
    contrapose!
    rintro ⟨y, hy⟩ hf
    let C := Set.range f
    have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
    let U := Cᶜ
    have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'
    have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
    classical
      let Z := of (ULift.{u} <| Fin 2)
      let g : Y ⟶ Z := CompHausLike.ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
      let h : Y ⟶ Z := CompHausLike.ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
      have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, hom_ofHom, ContinuousMap.coe_mk,
          Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]
      apply_fun fun e => (e y).down at H
      dsimp [g, LocallyConstant.ofIsClopen] at H
      rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
      exact top_ne_bot H

Goal state after:
case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightDiagram
⊢ SecondCountableTopology ↑S.cone.pt.toTop

Tactic:
← TopologicalSpace.Clopens.countable_iff_secondCountable

Goal state after:
S : LightDiagram
⊢ Countable (Clopens ↑S.cone.pt.toTop)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ (q' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))

Tactic:
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, forall_exists_index]
    intro s h x h'
    simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]
    exact Or.inr ⟨_, q_ih s h h'⟩

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
use j, LocallyConstant.ofIsClopen hV

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⋯
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen hV)