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

Goal state before:
pp: case refine_3
α : 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₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
filter_upwards [eventually_ge_atTop R.n₀] with n₀ n₀_ge_Rn₀

Goal state after:
α : 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₀
⊢ ∃ C₀,
    ∀ᶠ (n : ℕ) in atTop,
      ∀ C ≥ C₀, (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ l ≤ m∗ * n

Tactic:
intro x hx

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
⊢ x ∈ m∗ * n
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
apply rewrites_of_exists_parts

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

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x

Tactic:
simp [add_mul_div_left]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} ∪ {x | M2.evalFrom s2 x ∈ M2.accept}

Tactic:
Set.mem_union

Goal state after:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} ∨ x ∈ {x | M2.evalFrom s2 x ∈ M2.accept}
Module: Mathlib.Data.Num.Bitwise

Goal state before:
pp: b : Bool
⊢ (b::zero b) = zero b

Tactic:
cases b <;> rfl

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

Goal state before:
pp: b : Bool
⊢ (b::zero (decide ¬b = true)) = nz (msb b)

Tactic:
cases b <;> rfl

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

Goal state before:
pp: b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = m.testBit j

Tactic:
by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]

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

Goal state before:
pp: 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' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ (false ^^ false ^^ c.testBit i) = false

Tactic:
hi.2.2

Goal state after:
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' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ (false ^^ false ^^ false) = false
Module: Mathlib.Computability.Encoding

Goal state before:
pp: b : Bool
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b

Tactic:
cases b <;> rfl

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

Goal state before:
pp: m n : PosNum
⊢ ↑m < ↑n → ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
intro h; rw [Nat.add_right_comm m m 1, add_assoc]; exact Nat.add_le_add h h

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

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length

Tactic:
apply Nat.le_add_right

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

Goal state before:
pp: n : PosNum
⊢ ↑n.size + 1 = n.natSize.succ

Tactic:
size_eq_natSize n

Goal state after:
n : PosNum
⊢ n.natSize + 1 = n.natSize.succ
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} (x ++ [a]) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [evalFrom_append_singleton, mem_stepSet_iff]
    constructor
    · intro ⟨t, ht, h⟩
      obtain ⟨x', _, _⟩ := ih.mp ht
      rw [mem_εClosure_iff_exists] at h
      simp_rw [mem_εClosure_iff_exists_path] at h
      obtain ⟨u, _, n, _⟩ := h
      use x' ++ some a :: List.replicate n none
      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]
      tauto
    · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
        List.reduceOption_eq_nil_iff]
      intro ⟨_, ⟨x', _, rfl, _, n, rfl⟩, h⟩
      rw [isPath_append] at h
      obtain ⟨t, _, _ | u⟩ := h
      use t
      rw [mem_εClosure_iff_exists, ih]
      simp_rw [mem_εClosure_iff_exists_path]
      tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x✝ ∈ M.step a s

Tactic:
simp only [and_congr_right_iff]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ a ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x✝ ∈ M.step a s
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✝ : PosNum
b : Bool
n : PosNum
⊢ (bif b then ↑n else 0) = ↑(bif b then pos n else 0)

Tactic:
cases b <;> rfl

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

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l // BlankExtends l l₁ ∧ BlankExtends l l₂ }

Tactic:
refine
    if hl : l₁.length ≤ l₂.length then ⟨l₁, BlankExtends.refl _, Or.elim h id fun h' ↦ ?_⟩
    else ⟨l₂, Or.elim h (fun h' ↦ ?_) id, BlankExtends.refl _⟩

Goal state after:
case refine_1
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

case refine_2
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ ∀ (a b : List Γ), BlankExtends a b → a.getI n = b.getI n

Tactic:
rintro l _ ⟨i, rfl⟩

Goal state after:
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
⊢ l.getI n = (l ++ List.replicate i default).getI n
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.9
Γ' : Type ?u.8
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ ∀ (a b : List Γ), BlankExtends a b → mk (List.map f.f a) = mk (List.map f.f b)

Tactic:
rintro l _ ⟨i, rfl⟩

Goal state after:
Γ : Type ?u.9
Γ' : Type ?u.8
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
l : List Γ
i : ℕ
⊢ mk (List.map f.f l) = mk (List.map f.f (l ++ List.replicate i default))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
⊢ ∀ (a b : List Γ), BlankExtends a b → mk (List.flatMap f a) = mk (List.flatMap f b)

Tactic:
rintro l _ ⟨i, rfl⟩

Goal state after:
Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
i : ℕ
⊢ mk (List.flatMap f l) = mk (List.flatMap f (l ++ List.replicate i default))
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
O O' : Set (ℕ →. ℕ)
f : α →. σ
hf : RecursiveIn O f
hO : ∀ g ∈ O, RecursiveIn O' g
⊢ ∀ g ∈ O, Nat.RecursiveIn O' g

Tactic:
simpa only [RecursiveIn.iff_nat] using hO

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p

Tactic:
rw [show p = fun a => q (f a) from Set.ext hf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a ↦ q (f a)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case cons
Γ : 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)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
simp only [List.length, iterate_succ_apply]

Goal state after:
case cons
Γ : 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)^[l₁.length]
      (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝))) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some S.reverse[n]?).getD default = S.reverse[n]?

Tactic:
cases S.reverse[n]?

Goal state after:
case none
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some none).getD default = none

case some
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
val✝ : Γ k
⊢ (Option.map some (some val✝)).getD default = some val✝
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ head.eval v = pure [v.headI]

Tactic:
by simp [head]

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
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Tactic:
specialize h a

Goal state after:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
a : α
h : ι X a ≫ f = ι X a ≫ g
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩
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
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
this : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P')
⊢ PreservesLimit (cospan f g) (toCompHausLike h)

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

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
⊢ IsOpen[inst✝³] (range fun x ↦ ↑↑x)

Tactic:
have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior

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

Goal state before:
pp: case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H

Tactic:
apply TotallySeparatedSpace.totallyDisconnectedSpace

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

Goal state before:
pp: case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k₁ (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (push' k₂ (goto fun x ↦ Λ'.move p k₁ k₂ q))))
      s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
simp only [pop', Option.elim, TM2.stepAux, push']

Goal state after:
case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (S k₁).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k₁).head?, stk := update S k₁ (S k₁).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (S k₁).head?,
        stk := update (update S k₁ (S k₁).tail) k₂ ((S k₁).head?.getD default :: update S k₁ (S k₁).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case refine_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ U ⊆ φ ⁻¹' Z₂

Tactic:
intro x hx

Goal state after:
case refine_1
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
x : X
hx : x ∈ U
⊢ x ∈ φ ⁻¹' Z₂
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option.refine_5
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)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
⊢ univ.PairwiseDisjoint C

Tactic:
· rw [Set.pairwiseDisjoint_iff]
      rintro (_ | i) _ (_ | j) _
      · simp
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_right (subset_iUnion C' j) disjoint_sdiff_left
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_left (subset_iUnion C' i) disjoint_sdiff_right
      · simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) (by trivial) (by trivial)

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ ofLE ⋯ = id

Tactic:
by
  ext ⟨⟩
  rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (g.comp f) ⋯ = map g h1 ∘ map f h2

Tactic:
by
  ext ⟨⟩
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V}

Tactic:
let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ

Goal state after:
case e'_3.mpr
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V}
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
x✝ : ℕᵒᵖ
⊢ S.asLimitConeAux.π.app x✝ =
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).hom ≫
      S.asLimitCone.π.app x✝

Tactic:
rw [← @Iso.inv_comp_eq]

Goal state after:
S : LightProfinite
x✝ : ℕᵒᵖ
⊢ (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
      S.asLimitConeAux.π.app x✝ =
    S.asLimitCone.π.app x✝