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

Goal state before:
pp: case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
intro h

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inr.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)}.card = {u, v}.card

Tactic:
congr
      ext x
      simp [hn, imp_iff_not_or]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inr
ε : ℝ
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
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_mem : w' ∈ s
hw'_eq : ↑w' = w
hp' : ∃ a, ∃ (h : a ∈ K.parts), y a ⋯ = p'
⊢ G.Adj v w

Tactic:
obtain ⟨p, hp, hp'_eq⟩ : ∃ p, ∃ (h : p ∈ K.parts), y p h = p' := hp'

Goal state after:
case inr
ε : ℝ
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
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
p' : Finset (Fin n)
v : Fin n
hv : v ∈ ↑p'
w : Fin n
hw : w ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s)
w' : ↥(ErdosStone.filter K t)
hw'_mem : w' ∈ s
hw'_eq : ↑w' = w
p : Finset (Fin n)
hp : p ∈ K.parts
hp'_eq : y p hp = p'
⊢ G.Adj v w
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
hj : (i, j) ∉ μ.cells
⊢ ∃ j, (i, j) ∉ μ

Tactic:
exact ⟨j, hj⟩

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
⊢ pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h, g, hg₁, hg₂⟩ ↦ ?_⟩
  · subst h
    simp only [and_self, true_and]
    refine ⟨pt₁.groupElts.out, ?_⟩
    rw [Quotient.out_eq]
  · rcases pt₁ with ⟨i₁, g₁⟩
    rcases pt₂ with ⟨i₂, g₂⟩
    dsimp only at h
    subst h
    ext
    · rfl
    · exact heq_of_eq (hg₁.symm.trans hg₂)

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

Goal state before:
pp: case mp
m : ℕ
⊢ ppred 0 = some m → m.succ = 0

Tactic:
intro h

Goal state after:
case mp
m : ℕ
h : ppred 0 = some m
⊢ m.succ = 0
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mpr
m : ℕ
⊢ m.succ = 0 → ppred 0 = some m

Tactic:
intro h

Goal state after:
case mpr
m : ℕ
h : m.succ = 0
⊢ ppred 0 = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m n : ℕ
⊢ (n + 1).ppred = some m → m.succ = n + 1

Tactic:
intro h

Goal state after:
case mp
m n : ℕ
h : (n + 1).ppred = some m
⊢ m.succ = n + 1
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mpr
m n : ℕ
⊢ m.succ = n + 1 → (n + 1).ppred = some m

Tactic:
intro h

Goal state after:
case mpr
m n : ℕ
h : m.succ = n + 1
⊢ (n + 1).ppred = some m
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ (encode (Option.map f x)).pred = encode (Option.map (fun a ↦ (f a).get ⋯) x)

Tactic:
cases x

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
hx : decode n = none
⊢ (encode (Option.map f none)).pred = encode (Option.map (fun a ↦ (f a).get ⋯) none)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
val✝ : α
hx : decode n = some val✝
⊢ (encode (Option.map f (some val✝))).pred = encode (Option.map (fun a ↦ (f a).get ⋯) (some val✝))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f

Tactic:
simp [this, get_mem]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

Tactic:
rcases decode (α := α) n with - | a <;> simp

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f a)
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
G' : SimpleGraph V
| ¬G'.Adj x x'

Tactic:
1

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
G' : SimpleGraph V
| G'.Adj x x'
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ 1 ≤ 2 * 2

Tactic:
by decide

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ 0 < 4

Tactic:
by decide

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

Goal state before:
pp: f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
⊢ GrowsPolynomially f

Tactic:
by
  intro b hb
  have hg' := hg b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hg'⟩ := hg'
  refine ⟨c₁, hc₁_mem, c₂, hc₂_mem, ?_⟩
  filter_upwards [hg', (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg, hfg]
    with x hx₁ hx₂ hx₃
  intro u hu
  rw [hx₂ u hu.1, hx₃]
  exact hx₁ u hu

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → ∃ u, G.IsTutteViolator u

Tactic:
intro h

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
⊢ ∃ u, G.IsTutteViolator u
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ f =ᶠ[atTop] fun x ↦ |f x|

Tactic:
filter_upwards [hf'] with x hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : 0 ≤ f x
⊢ f x = |f x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ -f =ᶠ[atTop] fun x ↦ |f x|

Tactic:
filter_upwards [hf'] with x hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
x : ℝ
hx : f x ≤ 0
⊢ (-f) x = |f x|
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun x ↦ |f x| * |g x|) u ∈ Set.Icc (c₁ * c₃ * (fun x ↦ |f x| * |g x|) x) (c₂ * c₄ * (fun x ↦ |f x| * |g x|) x)

Tactic:
filter_upwards [hf, hg] with x hf hg

Goal state after:
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
⊢ ∀ u ∈ Set.Icc (b * x) x, |f u| * |g u| ∈ Set.Icc (c₁ * c₃ * (|f x| * |g x|)) (c₂ * c₄ * (|f x| * |g x|))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case ub
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u| * |g u| ≤ c₂ * c₄ * (|f x| * |g x|)

Tactic:
case ub => calc
    |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
           gcongr
           · exact (hf u hu).2
           · exact (hg u hu).2
    _ = c₂ * c₄ * (|f x| * |g x|) := by ring

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
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, a i * T (r i n) + g ↑n ≤ ∑ i, a i * (C * ((1 - ε ↑(r i n)) * asympBound g a b (r i n))) + g ↑n

Tactic:
by
      -- Apply the induction hypothesis
      gcongr (∑ i, a i * ?_) + g n with i _
      · exact le_of_lt <| R.a_pos _
      · exact h_ind (r i n) (by grind)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
⊢ f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))

Tactic:
have hfg₃ : ‖g u‖ ≤ 1 / 2 * f u := by
      calc ‖g u‖ ≤ 1 / 2 * ‖f u‖ := hfg' _ hu_lb
           _ = 1 / 2 * f u := by congr; simp only [norm_eq_abs, abs_eq_self, hfu_nonneg]

Goal state after:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0

Tactic:
· rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
          exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec.zero
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₁ n x : ℕ
⊢ x ∈ cf.eval n₁ → ∃ k, n ≤ k ∧ evaln (k + 1) cf n₁ = some x

Tactic:
intro h

Goal state after:
case prec.zero
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₁ n x : ℕ
h : x ∈ cf.eval n₁
⊢ ∃ k, n ≤ k ∧ evaln (k + 1) cf n₁ = some x
Module: Mathlib.Computability.DFA

Goal state before:
pp: case refine_3
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ List.drop (↑n) (List.take (↑m) x) ≠ []

Tactic:
intro h

Goal state after:
case refine_3
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
h : List.drop (↑n) (List.take (↑m) x) = []
⊢ False
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
x✝ : (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
cases hf.eventually_atTop_zero_or_pos_or_neg with

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

Goal state before:
pp: m n : ℕ
h : m.size ≤ n
⊢ 2 > 0

Tactic:
by decide

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

Goal state before:
pp: n : ℕ
⊢ 1 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
nk : n ∈ List.range 0
⊢ Nat.rec Option.none
      (fun n_1 n_ih ↦
        rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
          (fun cf cg x x_1 ↦ do
            let x ←
              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 0 (encode c))))
                  (0, cf) n
            let y ←
              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 0 (encode c))))
                  (0, cg) n
            some (Nat.pair x y))
          (fun cf cg x x_1 ↦ do
            let x ←
              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 0 (encode c))))
                  (0, cg) n
            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 0 (encode c))))
                (0, cf) x)
          (fun cf cg x x_1 ↦
            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 0 (encode c))))
                (0, cf) (unpair n).1)
              (fun n_2 n_ih ↦ do
                let 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 0 (encode c))))
                      (n_1, c) (Nat.pair (unpair n).1 n_2)
                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 0 (encode c))))
                    (0, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
              (unpair n).2)
          (fun cf x ↦ do
            let x ←
              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 0 (encode c))))
                  (0, cf) n
            Nat.rec (some (unpair n).2)
                (fun n_2 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 0 (encode c))))
                    (n_1, c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                x)
          c)
      0 =
    evaln 0 c n

Tactic:
simp [evaln]

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

Goal state before:
pp: case pos
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 : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : i = 0
⊢ bit b n < bit b' m

Tactic:
subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _

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

Goal state before:
pp: n i j : ℕ
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j <;> cases h : n.testBit i

Goal state after:
case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j