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

Goal state before:
pp: case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1

Tactic:
intro w

Goal state after:
case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
⊢ w ∈ G.neighborFinset v → #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ

Tactic:
intro w

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
⊢ w ∈ Gᶜ.neighborFinset v → #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
⊢ G.Colorable (r + 2)

Tactic:
obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
⊢ G.Colorable (r + 2)
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ∞
⊢ G.vertexCoverNum ≤ n ↔ ∀ (m : ℕ∞), (∀ (s : Set V), G.IsVertexCover s → m ≤ s.encard) → m ≤ n

Tactic:
simp [vertexCoverNum, iInf_le_iff]

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

Goal state before:
pp: μ ν : YoungDiagram
h : μ.cells = ν.cells
⊢ μ = ν

Tactic:
by rwa [YoungDiagram.ext_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
⊢ ∃ M, M.IsPerfectMatching

Tactic:
suffices ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧
      G'.Adj a c ∧ G' ≤ G ⊔ edge a c by
    obtain ⟨G', hG', hG'cyc, hG'xb, hnG'ac, hle⟩ := this
    have : M2.spanningCoe ∆ G' ≤ G := by
      apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
      simp [disjoint_edge, symmDiff_def, hM2ac, hnG'ac]
    use (G.toSubgraph (symmDiff M2.spanningCoe G') this)
    apply hM2.symmDiff_of_isAlternating hG' hG'cyc

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b) (decode n.div2)) = encode (Option.map Sum.inl (decode n.div2))

Tactic:
cases @decode α _ n.div2 <;> rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ → Bool
m : ℕ
pm : p m = true
this : true ∈ ↑p m
n : ℕ
hn : n ∈ rfind ↑p
h : m < n
⊢ False

Tactic:
by injection mem_unique this (rfind_min hn h)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑(decode n)).bind fun a ↦
      map encode
        ((fun a ↦
            (do
                  let n ← (↑fun n ↦ encode (decode n)) a.2
                  ↑n.ppred).bind
              ↑fun b ↦ (fun a n ↦ (decode n).bind (f a)) (a, b).1.1 (a, b).1.2)
          a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun p ↦ f p.1 p.2) a)

Tactic:
by
        simp only [decode_prod_val, decode_nat, Option.map_some, PFun.coe_val, bind_eq_bind,
          bind_some, Part.map_bind, map_some]
        cases decode (α := α) n.unpair.1 <;> simp
        cases decode (α := β) n.unpair.2 <;> simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a ↦ List.ofFn fun i ↦ x✝¹ i a

Tactic:
simp only [List.ofFn_zero]

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a ↦ []
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a ↦ List.ofFn fun i ↦ x✝¹ i a

Tactic:
simp only [List.ofFn_zero]

Goal state after:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a ↦ []
Module: Mathlib.Computability.Ackermann

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

Tactic:
exact add_add_one_le_ack ..

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ f x

Tactic:
have hu := Set.nonempty_of_mem hu

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ 0 ≤ f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ f x ≤ 0

Tactic:
have hu := Set.nonempty_of_mem hu

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu✝ : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ f x ≤ 0
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case right
α : 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)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ p a b * deriv (fun z ↦ 1 + ε z) x) =O[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
case right =>
          calc (fun x => x ^ (p a b) * deriv (fun z => 1 + ε z) x)
            _ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
              IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_add_smoothingFn.isBigO
            _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
              filter_upwards [eventually_gt_atTop 0] with x hx
              rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ∈ Set.Ioi 1

Tactic:
calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
                _ < b i * n := by gcongr

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pair
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 : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Tactic:
rcases hf hx with ⟨k₁, hk₁⟩

Goal state after:
case pair
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 : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
k₁ : ℕ
hk₁ : x ∈ evaln (k₁ + 1) cf n
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
⊢ (∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q) → r.Rewrites u v

Tactic:
by rintro ⟨p, q, rfl, rfl⟩; apply rewrites_of_exists_parts

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

Goal state before:
pp: case inl
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
left; rw [hbc]

Goal state after:
case inl
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
⊢ a ^^^ v < a
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
⊢ Nat.rec
      (lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cf) (unpair n).1)
      (fun n_1 n_ih ↦
        (lup
              (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          lup
            (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2

Tactic:
obtain ⟨lf, lg⟩ := encode_lt_prec cf cg
        rw [hg (Nat.pair_lt_pair_right _ lf)]
        cases n.unpair.2
        · rfl
        simp only
        rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]
        cases evaln k' _ _
        · rfl
        simp [k, hg (Nat.pair_lt_pair_right _ lg)]

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 + 1)) =
    match Fin.ofNat 4 (n + ↑(Fin.ofNat 4 1)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
List.range_succ,

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) 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.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)

Tactic:
filter_upwards [(tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf',
                  (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf_lb,
                  (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf_ub,
                  (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hg,
                  eventually_ge_atTop 0]
    with x hf_pos h_lb h_ub hg_bound hx_pos

Goal state after:
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
⊢ ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
⊢ M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a

Tactic:
ext s

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
s : σ
⊢ s ∈ M.stepSet (S ∪ T) a ↔ s ∈ M.stepSet S a ∪ M.stepSet T a
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
⊢ M.stepSet {s | s ∈ S ∧ p} a = {s | s ∈ M.stepSet S a ∧ p}

Tactic:
ext s

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
s : σ
⊢ s ∈ M.stepSet {s | s ∈ S ∧ p} a ↔ s ∈ {s | s ∈ M.stepSet S a ∧ p}
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)

Tactic:
rw [← not_iff_not]
  simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_ofPred_eq]
  tauto

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

Goal state before:
pp: m n : PosNum
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n
  norm_cast at this
  -- Porting note: `cases` didn't rewrite at `this`, so `revert` is required.
  revert this; cases cmp m n <;> simp_all [LT.lt.ne, LT.lt.ne']

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

Goal state before:
pp: m n : Num
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n
  norm_cast at this
  -- Porting note: `cases` didn't rewrite at `this`, so `revert` is required.
  revert this; cases cmp m n <;> simp_all [LT.lt.ne, LT.lt.ne']

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

Goal state before:
pp: case zero.zero
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)
⊢ ↑0 = Nat.bitwise g 0 0

Tactic:
Nat.bitwise_zero

Goal state after:
case zero.zero
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)
⊢ ↑0 = 0
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ l.nth 0 = l.head

Tactic:
by
  rw [← ListBlank.cons_head_tail l]
  induction l.tail using Quotient.inductionOn'
  rfl

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ l.nth (n + 1) = l.tail.nth n

Tactic:
by
  rw [← ListBlank.cons_head_tail l]
  induction l.tail using Quotient.inductionOn'
  rfl

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
⊢ ∀ g ∈ O, RecursiveIn O g

Tactic:
intro g

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
⊢ g ∈ O → RecursiveIn O g
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs,

Goal state after:
case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => Option.map (Cfg.map f₁ g₁.f) (step M c) = none
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ Cfg.map f₁ g₁.f val✝ ∈ step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c)

Tactic:
← M.map_step f₁ f₂ g₁ g₂ f₂₁ g₂₁ _ cs,

Goal state after:
case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ Cfg.map f₁ g₁.f val✝ ∈ Option.map (Cfg.map f₁ g₁.f) (step M c)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q

Tactic:
cases q

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Dir
a✝ : Stmt Γ Λ σ
⊢ move a✝¹ a✝ ∈ stmts₁ (move a✝¹ a✝)

case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → Γ
a✝ : Stmt Γ Λ σ
⊢ write a✝¹ a✝ ∈ stmts₁ (write a✝¹ a✝)

case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝ : Γ → σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
⊢ halt ∈ stmts₁ halt