mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 ↦ μ x ^ (↑(x_1 % m1) / ↑x_1)) atTop (𝓝 1)

Tactic:
← rpow_zero (μ x)

Goal state after:
case hg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun x_1 ↦ μ x ^ (↑(x_1 % m1) / ↑x_1)) atTop (𝓝 (μ x ^ 0))
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f (x * y) / f y) y ≤ f x

Tactic:
rw [← mul_one (f x), ← div_self hy0, ← mul_div_assoc,
          div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy0), mul_div_assoc, div_self hy0, mul_one]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ f (x * y) ≤ f x * f y
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
⊢ dist (smoothingSeminormSeq μ x n) (smoothingFun μ x) < ε

Tactic:
rw [Real.dist_eq, abs_lt]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
⊢ -ε < smoothingSeminormSeq μ x n - smoothingFun μ x ∧ smoothingSeminormSeq μ x n - smoothingFun μ x < ε
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun (k • y) =
    (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k * y)

Tactic:
Algebra.smul_def

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)
⊢ ((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toFun ((algebraMap K L) k * y) =
    (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k * y)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬n - m = 0

Tactic:
Nat.sub_eq_zero_iff_le

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬n ≤ m
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n

Goal state after:
case refine_1.inl
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : P.natDegree < n
⊢ ‖P.coeff n‖ ≤ 1

case refine_1.inr.inl
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : P.natDegree = n
⊢ ‖P.coeff n‖ ≤ 1

case refine_1.inr.inr
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : n < P.natDegree
⊢ ‖P.coeff n‖ ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n
    · simp [coeff_eq_zero_of_natDegree_lt hPn]
    · rw [← hPn, hP.coeff_natDegree, norm_one]
    · have : spectralValueTerms P n ≤ 1 := le_ciSup (spectralValueTerms_bddAbove P) n |>.trans h
      contrapose! this
      simp only [spectralValueTerms_of_lt_natDegree _ hPn]
      exact Real.one_lt_rpow this (by simp [hPn])

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ Tendsto (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop (𝓝 1)

Tactic:
← rpow_zero (μ x)

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ Tendsto (fun n ↦ μ x ^ (↑(s (ψ n)) * (μ x ^ 0 / ↑(ψ n)))) atTop (𝓝 1)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R

Tactic:
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul,
      sub_mul, mul_assoc]
    intro h₁ h₂
    rw [← h₂, ← h₁]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ ‖a • x‖ ≤ ‖a‖ * ‖x‖

Tactic:
simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ ⨅ p, projectiveSeminormAux ↑p ≤ ⨅ i, ‖a‖ * projectiveSeminormAux ↑i
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case smul_tprod
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
r✝ : 𝕜
f✝ : (i : ι) → E i
⊢ ↑(e ((lift f'.toMultilinearMap) (r✝ • (tprod 𝕜) f✝))) = (lift f.toMultilinearMap) (r✝ • (tprod 𝕜) f✝)

Tactic:
| smul_tprod =>

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
⊢ IsStrictMap ⇑(u.domRestrict E₁) ∧ IsClosed[inst✝⁵] ↑(↑(u.domRestrict E₁)).range

Tactic:
eqL

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
⊢ IsStrictMap ⇑(F₁.subtypeL ∘SL ↑e) ∧ IsClosed[inst✝⁵] ↑(↑(F₁.subtypeL ∘SL ↑e)).range
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : V →L[𝕜] V) (x : V), T (A x) = (f A) (T x)
d : StrongDual 𝕜 W
hd : d ((f (smulRight v u)) z) = 1
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
h_smul : smulRight v x = smulRight v y
⊢ x = y

Tactic:
simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝¹ : Subsingleton V
h✝ : Subsingleton W
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
use { toLinearEquiv := 0,
            norm_map' _ := by simp [Subsingleton.eq_zero (α := V), Subsingleton.eq_zero (α := W)] }
      exact ext fun _ ↦ Subsingleton.allEq _ _

Goal state after:
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:
rw [pow_succ', mul_assoc, mul_div_assoc, mul_assoc]

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.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ a < -t ∧ -t ≤ b

Tactic:
constructor <;> linarith

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree

Tactic:
← div_tendsto_atTop_zero_iff_degree_lt _ _ hQ

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
⊢ Tendsto (fun x ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) atTop (𝓝 0)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < ↑a' - ↑r'
ε' : ℝ := min ε ((↑a' - ↑r') / (↑L + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ ↑L / (↑L + 1) * (↑a' - ↑r') ≤ 1 * (↑a' - ↑r')

Tactic:
gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith

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

Goal state before:
pp: p q : ℂ[X]
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
by_cases hpq : p * q = 0
  · simpa [hpq, mahlerMeasure_zero] using mul_eq_zero.mp hpq
  rw [mul_eq_zero, not_or] at hpq
  simp only [mahlerMeasure, ne_eq, mul_eq_zero, hpq, or_self, not_false_eq_true, ↓reduceIte,
    logMahlerMeasure, eval_mul, Complex.norm_mul, circleAverage_def, mul_inv_rev, smul_eq_mul]
  rw [← exp_add, ← left_distrib]
  congr
  rw [← integral_add p.intervalIntegrable_mahlerMeasure q.intervalIntegrable_mahlerMeasure]
  apply integral_congr_ae
  rw [MeasureTheory.ae_iff]
  apply Set.Finite.measure_zero _ MeasureTheory.volume
  simp only [Classical.not_imp]
  apply Set.Finite.of_finite_image (f := circleMap 0 1) _ <|
    (injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [le_of_eq, pi_nonneg])).mono (fun _ h ↦ h.1)
  apply (p * q).roots.finite_toSet.subset
  rintro _ ⟨_, ⟨_, h⟩, _⟩
  contrapose h
  simp_all [log_mul]

Goal state after:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ x * prec ^ 2 < ((x * prec ^ 2).sqrt + 1) ^ 2

Tactic:
exact lt_succ_sqrt' (x * prec ^ 2)

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

Goal state before:
pp: a : ℂ
ha : a ≠ 0
b : ℂ
⊢ (C a * X + C b).mahlerMeasure = max ‖a‖ ‖b‖

Tactic:
simp only [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha],
    mahlerMeasure_mul, mahlerMeasure_const, ← coe_nnnorm, mahlerMeasure_X_add_C]

Goal state after:
a : ℂ
ha : a ≠ 0
b : ℂ
⊢ ↑‖a‖₊ * max 1 ↑‖a⁻¹ * b‖₊ = max ↑‖a‖₊ ↑‖b‖₊
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < ↑(x.ratSqrt prec + 1 / ↑prec)
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

Tactic:
push_cast at this

Goal state after:
x prec : ℕ
h : 0 < prec
this✝¹ : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
this✝ : ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)
this : √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
rw [sqrtTwoAddSeries_succ]

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries_succ]

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (√(2 + ↑c / ↑d)).sqrtTwoAddSeries n
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
by rw [← hn, sqrt_eq, abs_mul_abs_self]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.st = stdPart x

Tactic:
by
  rw [st]
  split_ifs with h
  · exact (isSt_iff.1 (Classical.choose_spec h)).2.symm
  · simp_rw [isSt_iff] at h
    push Not at h
    rw [eq_comm, stdPart_eq_zero]
    apply ne_of_lt
    by_contra! hx
    exact h _ hx rfl

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

Goal state before:
pp: x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
⊢ 1 < p.natDegree

Tactic:
by
  by_contra rid
  rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
  clear rid
  have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
  rcases em (a = 0) with (rfl | ha)
  · obtain rfl : b = 0 := by simpa
    simp at p_nonzero
  · rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
    · refine hx ⟨-b / a, ?_⟩
      assumption_mod_cast
    · assumption_mod_cast

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1

Tactic:
constructor <;> linarith

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
⊢ (cosPoly (n + 2)).natDegree ≤ n + 2

Tactic:
by
      rw [cosPoly]
      refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
      · exact (cosPoly_natDegree_le (n + 1)).trans (by simp)
      exact natDegree_mul_le.trans (by simp [add_comm 2, cosPoly_natDegree_le n])

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

Goal state before:
pp: case h₁
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ⋯
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ ‖log x‖ ≤ sSup ((fun y ↦ ‖log y‖) '' s)

Tactic:
refine le_csSup ?_ (by grind)

Goal state after:
case h₁
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ BddAbove ((fun y ↦ ‖log y‖) '' s)
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: case hbc
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ⋯
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖log x‖ ^ 2 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)

Tactic:
refine le_csSup ?_ (by grind)

Goal state after:
case hbc
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ BddAbove ((fun x ↦ ‖log x‖ ^ 2) '' s)