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

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
hfg : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a
hgf : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a
⊢ f = g

Tactic:
obtain ⟨r, hr0, hr⟩ := hfg
  obtain ⟨s, hs0, hs⟩ := hgf
  have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩
  have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩
  rw [← Function.Injective.eq_iff DFunLike.coe_injective]
  ext x
  exact le_antisymm (contraction_of_isPowMul_of_boundedWrt g hfpm hge x)
    (contraction_of_isPowMul_of_boundedWrt f hgpm hle x)

Goal state after:
Module: Mathlib.Analysis.Normed.Field.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ 0 < ?m.159

Tactic:
by simpa only [norm_pow] using norm_pos_iff.mpr this

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ mu μ hn n ≤ n
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ (fun n ↦ 1 / ↑(s (ψ n)) * ↑(s (ψ n))) =ᶠ[atTop] 1

Tactic:
apply Filter.EventuallyEq.div_mul_cancel_atTop

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ Tendsto (fun x ↦ ↑(s (ψ x))) atTop atTop
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = X ^ (minpoly K y).natDegree
⊢ (X ^ (minpoly K y).natDegree).coeff 0 = 0

Tactic:
coeff_X_pow,

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = X ^ (minpoly K y).natDegree
⊢ (if 0 = (minpoly K y).natDegree then 1 else 0) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = X ^ (minpoly K y).natDegree
⊢ (if 0 = (minpoly K y).natDegree then 1 else 0) = 0

Tactic:
if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = X ^ (minpoly K y).natDegree
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
⊢ ∀ (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h

Tactic:
g

Goal state after:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g : explicitCokernel f ⟶ Z
⊢ ∀ (h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f (x - y) = 0

Tactic:
rw [Metric.inseparable_iff, dist_eq_norm] at h

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : ‖x - y‖ = 0
⊢ f (x - y) = 0
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
this : (↑f.rangeRestrict).ker = ⊥
p : F →L[R] ↥(↑f).range
hp : ∀ (x : ↥(↑f).range), p ↑x = x
x : E
⊢ (f.leftInverse_of_injective_of_isClosed_range hf hf' ∘SL p) (f x) = x

Tactic:
simpa [hp ⟨f x, by simp⟩] using! f.rangeRestrict.leftInverse_apply_of_inj this x

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

Goal state before:
pp: ι : 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
x : ⨂[𝕜] (i : ι), E i
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‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ∈
    {p |
      ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

Tactic:
rw [Set.mem_ofPred]

Goal state after:
ι : 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
x : ⨂[𝕜] (i : ι), E i
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‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ ∃ G_1 x x_1,
    (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) =
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G_1 →L[𝕜] G_1)).comp (toDualContinuousMultilinearMap G_1)
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 ∧ IsClosed[inst✝⁵] ↑(↑u).range

Tactic:
rw [u.isStrictMap_isClosed_range_iff_restrict E₁ E₁_closed, 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: case h
𝕜 : 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
⊢ f =
    (let __LinearEquiv := 0;
      { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }).conjStarAlgEquiv

Tactic:
exact ext fun _ ↦ Subsingleton.allEq _ _

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K x : ℝ
⊢ Continuous fun ε ↦ gronwallBound δ K ε x

Tactic:
by
  by_cases hK : K = 0
  · simp only [gronwallBound_K0, hK]
    fun_prop
  · simp only [gronwallBound_of_K_ne_0 hK]
    fun_prop

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ gronwallBound δ K ε (x - a)

Tactic:
change f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε

Goal state after:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun ε' ↦ gronwallBound δ K ε' (x - a)) ε
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
L : ℝ≥0
α : FunSpace t₀ x₀ 0 L
⊢ α.toFun t₀ = x₀

Tactic:
by
  simpa using α.mem_closedBall₀

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

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

Tactic:
· rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
      exact this.symm

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 : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : 0 < c
⊢ gaussNorm v c p = 0 ↔ p = 0

Tactic:
by
  rw [← gaussNorm_coe_powerSeries _ _ (le_of_lt hc)]
  convert PowerSeries.gaussNorm_eq_zero_iff v c p (by grind) (by simp) h_eq_zero hc
    (by simpa [PowerSeries.HasGaussNorm] using! aux_bdd v p)
  exact Iff.symm coe_eq_zero_iff

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
h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty
j : ℕ
⊢ j < Nat.find h_nonempty → v (p.coeff j) * c ^ j < gaussNorm v c p

Tactic:
hj_lt

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
j : ℕ
hj_lt : j < Nat.find h_nonempty
⊢ v (p.coeff j) * c ^ j < gaussNorm v c p
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i :=
    Finset.prod_nonneg (fun i hi ↦ pow_nonneg (hc i) (t i))
  have Final (t : σ →₀ ℕ) : v ((coeff t) (f + g)) * ∏ i ∈ t.support, c ↑i ^ t ↑i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
      (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
    specialize hv (coeff t f) (coeff t g)
    rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h
    · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_left]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
    · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_right]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
  refine Real.iSup_le ?_ ?_
  · refine fun t ↦ calc
    _ ≤ _ := Final t
    _ ≤ max (gaussNorm v c f) (gaussNorm v c g) := by
      simp only [le_sup_iff]
      rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i)
        (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h
      · left
        simpa [h] using! le_gaussNorm v c f hbfd t
      · right
        simpa [h] using! le_gaussNorm v c g hbgd t
  · simp only [le_sup_iff]
    left
    exact gaussNorm_nonneg v c f vNonneg

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

Goal state before:
pp: s : Multiset ℂ[X]
⊢ s.prod.mahlerMeasure = (Multiset.map (fun p ↦ p.mahlerMeasure) s).prod

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [mahlerMeasure_mul, ih]

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

Goal state before:
pp: case refine_1
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ circleMap 0 1 '' {a | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x | x ∈ p.roots}

Tactic:
rintro z ⟨θ, ⟨_, heval⟩, rfl⟩
      exact (mem_roots hp).mpr heval

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case mk.mk
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : (↑φ).Germ β
f : α → β
x✝ : (↑φ).Germ β
g : α → β
⊢ Quot.mk (⇑((↑φ).germSetoid β)) f < Quot.mk (⇑((↑φ).germSetoid β)) g ↔
    LiftRel (fun x1 x2 ↦ x1 < x2) (Quot.mk (⇑((↑φ).germSetoid β)) f) (Quot.mk (⇑((↑φ).germSetoid β)) g)

Tactic:
exact coe_lt

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ max ↑a ↑b = map₂ max ↑a ↑b

Tactic:
rcases le_total (a : β*) b with h | h
    · rw [max_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_right hi).symm
    · rw [max_eq_left h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_left hi).symm

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

Goal state before:
pp: b : ℕ
⊢ Continuous ofDigits

Tactic:
| =>

Goal state after:
b : ℕ
⊢ Continuous ofDigits
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b n : ℕ
⊢ Continuous ofDigits

Tactic:
| =>

Goal state after:
b n : ℕ
⊢ Continuous ofDigits
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑m * ↑(↑D ^ n) = ↑(N ^ n)
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False

Tactic:
← Int.cast_mul,

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑(m * ↑D ^ n) = ↑(N ^ n)
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑(D ^ n) ∣ ↑(N ^ n).natAbs
⊢ False

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ^ n ∣ (N ^ n).natAbs
⊢ False
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
by_cases hp : p.leadingCoeff = 0

Goal state after:
case pos
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
hp : p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

case neg
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
hp : ¬p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st

Tactic:
h.st_eq,

Goal state after:
case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -0
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
let u₂ (x : ℝ) : ℝ := x * (f x) ^ n

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y k : ℝ≥0
⊢ ⨅ n, ((k * x).agmSequences (k * y) n).2 = ⨅ i, k * (x.agmSequences y i).2

Tactic:
congr! with n

Goal state after:
x y k : ℝ≥0
n : ℕ
⊢ ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 0 = 0

Tactic:
by simp [binEntropy]

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

Goal state before:
pp: ⊢ binEntropy 1 = 0

Tactic:
by simp [binEntropy]

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

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ Real.log ‖z‖ ≤ Real.log (√2 * max z.re |z.im|)

pp: case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ √2 ≠ 0

pp: case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0

Tactic:
Real.log_le_log_iff,

Goal state after:
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ ‖z‖ ≤ √2 * max z.re |z.im|

case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ 0 < ‖z‖

case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ 0 < √2 * max z.re |z.im|

case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ √2 ≠ 0

case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < √2
hz' : 1 ≤ ‖z‖
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot

Tactic:
simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]

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

Goal state before:
pp: case refine_1
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

pp: case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
· exact (sinPoly_natDegree_le (n + 1)).trans (by simp)

Goal state after:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1)) =
    ↑(n + 2)! *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]

Goal state after:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) *
        ((↑n + 1) * ↑n ! *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 *
        (↑n ! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑n !) *
      ((2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)