mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_1
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₂ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₂ ⋯) = t
⊢ p₁ = p₂

Tactic:
rw [← heq] at hy₂'

Goal state after:
case refine_1
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₁ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₁ ⋯) = t
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: x✝¹ : YoungDiagram
x✝ : ℕ × ℕ
⊢ x✝ ∈ { cells := ∅, isLowerSet := instOrderBot._proof_2 } → x✝ ∈ x✝¹

Tactic:
by
    intro y
    simp only [mem_mk, Finset.notMem_empty] at y

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ μ.rowLen i1 < μ.rowLen i1

Tactic:
rw [← mem_iff_lt_rowLen] at h_lt ⊢

Goal state after:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.colLen j

Tactic:
← rowLen_transpose,

Goal state after:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.transpose.rowLen j
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n k : ℕ
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k

Tactic:
by
    induction k with
    | zero => simp
    | succ n ih => simp only [ih, add_succ, psub_succ, bind_assoc]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
this : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
by exact fun a => this _ _ (Nat.le_add_left _ _)

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x ↦ (x, f x)) bs)).toList ++
      List.flatMap (fun x ↦ (List.lookup x (List.map (fun x ↦ (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'

Tactic:
have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
          rcases this with ⟨ha, has'⟩
          simpa [List.lookup_graph f ha] using ih has'

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ 0 < ack m 1

Tactic:
apply ack_pos

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)

Tactic:
apply ack_pos

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ m + n + 2 = (m + 1 + n).succ

Tactic:
rw [succ_eq_add_one]

Goal state after:
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
rw [max_eq_right h₁]

Goal state after:
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
⊢ ack (b + 4) (pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + (n + 1))
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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ↑n
⊢ ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2

Tactic:
by exact hn' i

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
eventually_atTop

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
h : ∃ a, ∀ (b : ℝ), a ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, f x = c
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ᶠ (x : ℝ) in atTop, f x = f (max n₀ 2)

Tactic:
eventually_atTop

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → f b = f (max n₀ 2)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case e_a.e_f.e_a.e_a.e_a
α : 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 : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
⊢ ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1) =
    ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1) - ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
refine eq_sub_of_add_eq ?_

Goal state after:
case e_a.e_f.e_a.e_a.e_a
α : 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 : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) 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
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, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
⊢ ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1) + ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1) =
    ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ (1 + ε ↑n) * asympBound g a b n

Tactic:
filter_upwards [R.eventually_asympBound_pos, eventually_one_add_smoothingFn_pos] with n hn hn₂

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < asympBound g a b n
hn₂ : 0 < 1 + ε ↑n
⊢ 0 ≤ (1 + ε ↑n) * asympBound g a b n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case e_a.e_f.e_a.e_a.e_a
α : 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
i : α
⊢ ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1) =
    ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1) - ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
refine eq_sub_of_add_eq ?_

Goal state after:
case e_a.e_f.e_a.e_a.e_a
α : 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
i : α
⊢ ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1) + ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1) =
    ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ (⨆ i, l ^ i) * m ≤ m

Tactic:
iSup_mul

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : l * m ≤ m
⊢ ⨆ i, l ^ i * m ≤ m
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
⊢ (fun n ↦ (1 - ε ↑n) * asympBound g a b n) =O[atTop] fun n ↦ 1 * asympBound g a b n

Tactic:
refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero) (isBigO_refl _ _)
      rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop

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
⊢ c ^^^ a = b ^^^ v

Tactic:
rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]

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

Goal state before:
pp: case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1) ++ [n + 1]) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
List.foldl_append,

Goal state after:
case succ
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
⊢ List.foldl (fun x1 x2 ↦ x1 ^^^ x2) (List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1))) [n + 1] =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (decodePosNum (encodePosNum m)).bit0 = m.bit0

Tactic:
| bit0 m hm =>

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

Goal state before:
pp: m p : PosNum
⊢ ↑(m * p) + ↑(m * p) = ↑m * (↑p + ↑p)

Tactic:
rw [mul_to_nat m p, left_distrib]

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

Goal state before:
pp: m p : PosNum
⊢ ↑(m * p) + ↑(m * p) + ↑m = ↑m * (↑p + ↑p) + ↑m

Tactic:
rw [mul_to_nat m p, left_distrib]

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

Goal state before:
pp: case nil
α : Type u_1
⊢ [].length = [].length

Tactic:
length

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a

Tactic:
List.foldl_append,

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
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]

Goal state after:
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₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
intro a b
    transfer_rw
    apply le_antisymm

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (b ∈ (Nat.rfind fun n_1 ↦ Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun a ↦ ↑pred (f (a ::ᵥ v))) ↔
    b ∈ Nat.rfindOpt fun a ↦ ofNat (Option ℕ) (f (a ::ᵥ v))

Tactic:
simp only [Nat.rfindOpt, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]

Goal state after:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun n_1 ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome), ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]

Goal state after:
case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a a ∧ f a = none
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
⊢ (char a).rmatch x = true ↔ x = [a]

Tactic:
by
  rcases x with - | ⟨_, x⟩
  · exact of_decide_eq_true rfl
  · rcases x with - | ⟨head, tail⟩
    · rw [rmatch, deriv, List.singleton_inj]
      split <;> tauto
    · rw [rmatch, rmatch, deriv, cons.injEq]
      split
      · simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]
      · simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (move n d q) = SupportsStmt S q

Tactic:
by
  suffices ∀ {i}, SupportsStmt S ((Stmt.move d)^[i] q) = _ from this
  intro i; induction i generalizing q <;> simp only [*, iterate]; rfl

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 → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
rintro _ f L' R' l₁ l₂ rfl

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

Goal state before:
pp: case some.goto
Γ : 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 : Γ → σ → Λ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) { l := some (Λ'.normal (l R.head v)), var := v, Tape := trTape' enc0 L R }
    { l := Option.map Λ'.normal (some (l (Tape.mk' L R).head v)), var := v, Tape := trTape' enc0 L R }

Tactic:
apply ReflTransGen.refl

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

Goal state before:
pp: case some.halt
Γ : 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 Γ
⊢ Reaches (step (tr enc dec M)) { l := none, var := v, Tape := trTape' enc0 L R }
    { l := Option.map Λ'.normal none, var := v, Tape := trTape' enc0 L R }

Tactic:
apply ReflTransGen.refl

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
inst✝ : HasExplicitFiniteCoproducts P
n : ℕ
⊢ HasColimitsOfShape (Discrete (Fin n)) (CompHausLike P)

Tactic:
let α := ULift.{w} (Fin n)

Goal state after:
P : TopCat → Prop
α✝ : Type w
inst✝² : Finite α✝
X : α✝ → CompHausLike P
inst✝¹ : HasExplicitFiniteCoproduct X
inst✝ : HasExplicitFiniteCoproducts P
n : ℕ
α : Type w := ULift.{w, 0} (Fin n)
⊢ HasColimitsOfShape (Discrete (Fin n)) (CompHausLike P)
Module: Mathlib.Topology.Separation.Profinite

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

Tactic:
constructor
  · intro h
    exact totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim
  apply TotallySeparatedSpace.totallyDisconnectedSpace

Goal state after: