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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
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 ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt

Tactic:
simp_rw [← mem_coe, coe_smul, Set.mem_smul_set_iff_inv_smul_mem]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false.inl
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n < m
⊢ false ∈ p n

pp: case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p n

Tactic:
· exact al _ h

Goal state after:
case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p n
Module: Mathlib.Computability.Ackermann

Goal state before:

Tactic:
n + 1 + 1 ≤ m + (m + 1 + n + 1) := by lia
      _ ≤ m + ack (m + 1) n := by gcongr; exact add_add_one_le_ack ..
      _ < ack m (ack (m + 1) n) := add_lt_ack ..

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inl
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.338 < m
⊢ 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_left h₁.le]
          gcongr <;> omega

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

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

Tactic:
contrapose!

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
calc
        (fun z => p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_sub_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring

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

Goal state before:

Tactic:
b (min_bi b) / 2
    _ < b (min_bi b) := by aesop (add safe apply div_two_lt_of_pos)
    _ < 1 := R.b_lt_one _

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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
let b' := b (min_bi b) / 2

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)
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)
⊢ (fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
simp_rw [mul_assoc]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ (fun n ↦ b i ^ p a b * (↑n ^ p a b * (1 / log ↑n ^ 2))) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)
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 * (b i)⁻¹ ≤ b i * ↑⌈(b i)⁻¹⌉₊

Tactic:
by gcongr; exact Nat.le_ceil _

Goal state after:
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
⊢ ∃ b_1, 1 ≤ ∑ i, a i * b i ^ b_1

Tactic:
exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

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)
⊢ (fun n ↦ b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
simp_rw [mul_assoc]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ (fun n ↦ b i ^ p a b * (↑n ^ p a b * (1 / log ↑n ^ 2))) =Θ[atTop] fun n ↦ ↑n ^ p a b * (1 / log ↑n ^ 2)
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 * (b i)⁻¹ ≤ b i * ↑⌈(b i)⁻¹⌉₊

Tactic:
by gcongr; exact Nat.le_ceil _

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

Tactic:
let b' := b (min_bi b) / 2

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

Goal state before:
pp: case ha
α : 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 ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j / ↑j ^ (p a b + 1)

Tactic:
rw [div_nonneg_iff]

Goal state after:
case ha
α : 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 ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑n ^ (p a b + 1) ≥
    ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑n ^ (p a b + 1))

Tactic:
gcongr; exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)

Goal state after:
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
⊢ ∀ᶠ (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:
let b' := b (min_bi b) / 2

Goal state after:
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
⊢ ∀ᶠ (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
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑(r i n) ^ (p a b + 1) ≥
    ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))

Tactic:
gcongr; exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)

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

Goal state before:
pp: case ha
α : 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 : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j / ↑j ^ (p a b + 1)

Tactic:
rw [div_nonneg_iff]

Goal state after:
case ha
α : 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 : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:

Tactic:
sumTransform (p a b) g (r i n) n
        = n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
      _ ≥ n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
        gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1
      _ ≥ n ^ (p a b) * (∑ _u ∈ Finset.Ico (r i n) n, c₂ * g n / (r i n) ^ ((p a b) + 1)) := by
        gcongr n ^ (p a b) * (Finset.Ico (r i n) n).sum (fun _ => c₂ * g n / ?_) with u hu
        · rw [Finset.mem_Ico] at hu
          have := calc 0 < r i n := hrpos_i
                      _ ≤ u := hu.1
          positivity
        · rw [Finset.mem_Ico] at hu
          exact rpow_le_rpow_of_nonpos (by positivity)
            (by exact_mod_cast hu.1) (le_of_lt hp)
      _ ≥ n ^ p a b * #(Ico (r i n) n) • (c₂ * g n / r i n ^ (p a b + 1)) := by
          gcongr; exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)
      _ = n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / r i n ^ (p a b + 1)) := by
          rw [nsmul_eq_mul, mul_assoc]
      _ ≥ n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / (c₁ * n) ^ (p a b + 1)) := by
          gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)
          exact rpow_le_rpow_of_nonpos (by positivity) (hn₁ i) (le_of_lt hp)
      _ = n ^ (p a b) * (n - r i n) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by
          congr; rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
      _ ≥ n ^ (p a b) * (n - c₃ * n) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by
          gcongr; exact hn₃ i
      _ = n ^ (p a b) * n * (1 - c₃) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by ring
      _ = n ^ (p a b) * n * (1 - c₃) * (c₂ * g n / (c₁ ^ ((p a b) + 1) * n ^ ((p a b) + 1))) := by
          rw [Real.mul_rpow (by positivity) (by positivity)]
      _ = (n ^ ((p a b) + 1) / n ^ ((p a b) + 1)) * (1 - c₃) * c₂ * g n / c₁ ^ ((p a b) + 1) := by
          rw [← Real.rpow_add_one (by positivity) (p a b)]; ring
      _ = (1 - c₃) * c₂ / c₁ ^ ((p a b) + 1) * g n := by
          rw [div_self (by positivity), one_mul]; ring
      _ ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)) * g n := by
          gcongr; exact min_le_right _ _

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

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

Tactic:
refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
    have hb_pos := hb.1
    filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx'
    intro u hu
    simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).1
⊢ Primrec fun a ↦
    have z := (unpair a.1.1.2).1;
    Nat.casesOn (unpair a.1.1.2).2 (lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y ↦ do
      let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y)
      lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))

Tactic:
refine
      Primrec.nat_casesOn (Primrec.snd.comp (Primrec.unpair.comp n))
        (hlup.comp <| L.pair <| (k.pair cf).pair z)
        (?_ : Primrec _)

Goal state after:
case hpc
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
z : Primrec fun a ↦ (unpair a.1.1.2).1
⊢ Primrec fun p ↦
    (fun a y ↦ do
        let i ← lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair (unpair a.1.1.2).1 y)
        lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair (unpair a.1.1.2).1 (Nat.pair y i)))
      p.1 p.2
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 : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
this : a.testBit i = true ∨ b.testBit i = true ∨ c.testBit i = true
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
obtain h | h | h := this

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

case inr.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 : b.testBit i = true
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

case inr.inr
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 : c.testBit i = true
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl
a b c : ℕ
h : a < b ^^^ c
ha : b ^^^ c < a
⊢ a ^^^ c < b ∨ a ^^^ b < c

pp: case inr.inl
a b c : ℕ
h : a < b ^^^ c
hb : c ^^^ a < b
⊢ a ^^^ c < b ∨ a ^^^ b < c

pp: case inr.inr
a b c : ℕ
h : a < b ^^^ c
hc : a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
exacts [(h.asymm ha).elim, Or.inl <| Nat.xor_comm _ _ ▸ hb, Or.inr hc]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (M.reverse.evalFrom S' x)
⊢ Disjoint S' (M.evalFrom S x.reverse)

Tactic:
simp only [evalFrom, List.foldl_reverse] at h ⊢

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' x)
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S x)
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
have := (H _).1 _ hn

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ (↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (f a)) ∨
    n ∈ (↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a