mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
π'_quot : IsOpenQuotientMap ⇑π'
u_restr_eq : u.domRestrict A = v.domRestrict B ∘SL π'
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔ IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range

Tactic:
by
        rw [← range_eq, u_eq, coe_comp, π_quot.isQuotientMap.isStrictMap_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u v : E →L[𝕜] F
A : Submodule 𝕜 E
inst✝ : A.CoFG
h_eqOn : EqOn ⇑u ⇑v ↑A.topologicalClosure
⊢ IsStrictMap ⇑(u.domRestrict A.topologicalClosure) ∧ IsClosed[inst✝⁴] (range ⇑(u.domRestrict A.topologicalClosure)) ↔
    IsStrictMap ⇑(v.domRestrict A.topologicalClosure) ∧ IsClosed[inst✝⁴] (range ⇑(v.domRestrict A.topologicalClosure))

Tactic:
ContinuousLinearMap.coe_domRestrict,

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u v : E →L[𝕜] F
A : Submodule 𝕜 E
inst✝ : A.CoFG
h_eqOn : EqOn ⇑u ⇑v ↑A.topologicalClosure
⊢ IsStrictMap ((↑A.topologicalClosure).domRestrict ⇑u) ∧
      IsClosed[inst✝⁴] (range ((↑A.topologicalClosure).domRestrict ⇑u)) ↔
    IsStrictMap ((↑A.topologicalClosure).domRestrict ⇑v) ∧
      IsClosed[inst✝⁴] (range ((↑A.topologicalClosure).domRestrict ⇑v))
Module: Mathlib.Dynamics.FixedPoints.Topology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n ↦ f^[n + 1] x) atTop (𝓝 (f y))

Tactic:
simp only [iterate_succ' f]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n ↦ (f ∘ f^[n]) x) atTop (𝓝 (f y))
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
⊢ u (k + 1) ≤ u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ k_1 ∈ Ico n₀ (k + 1), b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i

Tactic:
have hck : 0 ≤ c k := hc k hk

Goal state after:
case succ
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
⊢ u (k + 1) ≤ u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ k_1 ∈ Ico n₀ (k + 1), b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
simp only [gronwallBound_of_K_ne_0 hK]

Goal state after:
case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x

Tactic:
simp only [gronwallBound_K0, hK]

Goal state after:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε ↦ δ + ε * x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x

Tactic:
simp only [gronwallBound_of_K_ne_0 hK]

Goal state after:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K ^ (n + 1) * |↑t - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
pow_succ',

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K * ↑K ^ n * |↑t - ↑t₀| ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.degree ≤ 0

Tactic:
by simp [leadingCoeff_eq_zero.1 hP]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
· simp [hP, IsEquivalent.refl]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
· simp [hP, IsEquivalent.refl]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
n : ℕ
r : R
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n

Tactic:
by_cases hr : r = 0 <;> simp [gaussNorm, support_monomial, hr]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i ∧ ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p

Tactic:
have h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty := by
    obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
    exact ⟨i, Set.mem_ofPred.mpr hi⟩

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i ∧ ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h✝ : i < x
⊢ gaussNorm v c p * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) =
    v (p.coeff i) * c ^ i * (v (q.coeff (i + j - x)) * c ^ (i + j - x))

Tactic:
hi_p

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h✝ : i < x
⊢ v (p.coeff i) * c ^ i * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) =
    v (p.coeff i) * c ^ i * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.logMahlerMeasure = log p.mahlerMeasure

Tactic:
by
  rw [mahlerMeasure]
  split_ifs <;> simp_all [logMahlerMeasure_def, circleAverage_def]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : (X - C z).logMahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
logMahlerMeasure_eq_log_MahlerMeasure

Goal state after:
z : ℂ
this : log (X - C z).mahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
logMahlerMeasure_eq_log_MahlerMeasure

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ (volume.restrict (Icc 0 (2 * π))) {x | eval (circleMap 0 1 x) p ≠ 0}ᶜ = 0

Tactic:
compl_def,

Goal state after:
case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ (volume.restrict (Icc 0 (2 * π))) {x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} = 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ (volume.restrict (Icc 0 (2 * π))) {x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} = 0

Tactic:
Measure.restrict_apply' (by simp)

Goal state after:
case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ volume ({x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) = 0
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹

Tactic:
pow_succ',

Goal state after:
case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * (↑b * ↑b ^ x)⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b ^ (n + 1))⁻¹

Tactic:
pow_succ',

Goal state after:
case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b * ↑b ^ n)⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹

Tactic:
pow_succ',

Goal state after:
case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b * ↑b ^ x)⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b ^ (n + 1) * ∑ x_1 ∈ Finset.range n, ofDigitsTerm (x.digits b) x_1 + ↑b ^ (n + 1) * ofDigitsTerm (x.digits b) n =
    ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
pow_succ',

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑b ^ n * ∑ x_1 ∈ Finset.range n, ofDigitsTerm (x.digits b) x_1 + ↑b * ↑b ^ n * ofDigitsTerm (x.digits b) n =
    ↑⌊↑b * ↑b ^ n * x⌋₊
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊↑b ^ (n + 1) * x⌋₊) = ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
pow_succ',

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊↑b * ↑b ^ n * x⌋₊) = ↑⌊↑b * ↑b ^ n * x⌋₊
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case ha
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ 1 ≤ max 1 ‖a‖

pp: case a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ x ≤ p.roots

Tactic:
· exact le_max_left 1 ‖a‖

Goal state after:
case a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ x ≤ p.roots
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
z : A
⊢ (C z).mapMahlerMeasure v = ‖z‖

Tactic:
simp [mapMahlerMeasure, hv.norm_map_of_map_zero (map_zero _)]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x

Tactic:
rw [pow_succ] at h

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
| dist x y / 2 ^ (n + 1)

Tactic:
pow_succ',

Goal state after:
x y : ℝ≥0
n : ℕ
| dist x y / (2 * 2 ^ n)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
have : -p * log p ≤ 0 := by
      wlog h : -1 < p
      · simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]
      · nlinarith [log_neg_of_lt_zero hp h]

Goal state after:
case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
· exact (binEntropy_neg_of_neg hp).le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

Tactic:
deriv.log differentiableAt_fun_id xne0

Goal state after:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x)) p - deriv (fun x ↦ x) p / p = -1 / (p * (1 - p))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * ↑(a ^ i) * ↑(b ^ (k - i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑b ^ (k - i)

pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
← Int.cast_pow

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * ↑(a ^ i) * ↑(b ^ (k - i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑(b ^ (k - i))

case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
by
  have : ∀ x ∈ Ici (0 : A), IsStrictlyPositive (algebraMap ℝ A t + x) := by grind
  let addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm (algebraMap ℝ A t, .id)
  have haddl : Function.Injective addl := by intro _ _; simp [addl]
  have hici : Ici (0 : A) = addl ⁻¹' addl '' Ici 0 := by
    rw [Set.preimage_image_eq _ haddl]
  simp_rw [add_comm]
  change ConvexOn ℝ (Ici 0) (Ring.inverse ∘ addl)
  rw [hici]
  apply ConvexOn.comp_affineMap
  refine ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))
  simp only [AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add,
    LinearMap.coe_toAffineMap, LinearMap.id_coe, AffineMap.coe_const, Pi.add_apply, id_eq,
    Function.const_apply, image_add_right, preimage_add_const_Ici, sub_neg_eq_add, zero_add, addl]
  exact fun x hx  => IsStrictlyPositive.of_le (by grind) hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 1)

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : t ∈ Ioo 0 1
⊢ ‖p.rpowIntegrand₀₁ t x‖ ≤ t ^ (p - 1)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m

Tactic:
· intro m
    rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]
    exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

Tactic:
have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
    rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]
    exact Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ clog b r = 0

Tactic:
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_ge, neg_eq_zero, Int.natCast_eq_zero,
    Nat.log_eq_zero_iff]

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ 0 ≤ logb b x

Tactic:
logb_nonneg_iff_of_base_lt_one b_pos b_lt_one hx

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ LipschitzWith 1 ε.mulExpNegMulSq

Tactic:
by
  apply lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq
  exact nnnorm_deriv_mulExpNegMulSq_le_one hε

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
⊢ (fun x ↦ logb b (c * x)) =O[atTop] log

Tactic:
simpa [logb, div_eq_mul_inv, mul_comm]
    using (isBigO_log_const_mul_log_atTop c).const_mul_left (log b)⁻¹

Goal state after: