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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥R[x] := ⟨x, ⋯⟩
hy : x = ↑y
⊢ f₁ x = f₂ x

Tactic:
have h1 : f₁ y.val = g₁ y := rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥R[x] := ⟨x, ⋯⟩
hy : x = ↑y
h1 : f₁ ↑y = g₁ y
⊢ f₁ x = f₂ x
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝² : FiniteDimensional K ↥K⟮y⟯
this✝¹ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this✝ : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
this : ‖z - z'‖ < ‖z - z'‖
⊢ False

Tactic:
simp [lt_self_iff_false] at this

Goal state after:
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case neg.refine_1
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ f g = h

Tactic:
have : f ∘ s = fun n => ∑ k ∈ range (n + 1), v k := by
      ext n
      simp [s, map_sum, hu]

Goal state after:
case neg.refine_1
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : ⇑f ∘ s = fun n ↦ ∑ k ∈ range (n + 1), v k
⊢ f g = h
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
⊢ f = default

Tactic:
ext; apply Subsingleton.elim

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

Goal state before:
pp: case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
⊢ f = default

Tactic:
ext; apply Subsingleton.elim

Goal state after:
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
this : ‖f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑g‖ + ‖↑g'‖ = ‖hatg - ↑g‖ + ‖g'‖

Tactic:
rw [Completion.norm_coe]

Goal state after:
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
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0

Tactic:
simp [cond2]

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

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst✝³ : NormedField L
inst✝² : NormedAlgebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : CompleteSpace K
x : L
⊢ ‖x‖ = spectralNorm K L x

Tactic:
← toMulAlgebraNorm_apply K L x,

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst✝³ : NormedField L
inst✝² : NormedAlgebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : CompleteSpace K
x : L
⊢ (toMulAlgebraNorm K L) x = spectralNorm K L x
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ ‖(1 + f x) * ∏ x ∈ t, (1 + f x) - 1‖ ≤ Real.exp (∑ i ∈ insert x t, ‖f i‖) - 1

Tactic:
Finset.sum_insert hx,

Goal state after:
case insert
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
⊢ ‖(1 + f x) * ∏ x ∈ t, (1 + f x) - 1‖ ≤ Real.exp (‖f x‖ + ∑ x ∈ t, ‖f x‖) - 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ∏ x ∈ b, (1 + f x) ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)

Tactic:
rw [← union_sdiff_of_subset hb, prod_union sdiff_disjoint.symm,
      Metric.mem_ball, dist_eq_norm_sub, ← mul_sub_one,
      show ε / 2 = r₁ * (ε / (2 * r₁)) by field]
    apply (norm_mul_le _ _).trans_lt
    refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
    · refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
    · refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
      simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ∀
    b ∈
      {p |
        ∃ G x x_1,
          p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)},
    b ≤ projectiveSeminorm

Tactic:
· intro p hp
    simp only [Set.mem_ofPred_eq] at hp
    obtain ⟨G, _, _, h⟩ := hp
    rw [h]; intro x; simp only [Seminorm.comp_apply, coe_normSeminorm]
    exact toDualContinuousMultilinearMap_le_projectiveSeminorm _

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
u : E →L[𝕜] F
pkg : u.FredholmPackage
⊢ (↑pkg.quasiInverse).IsQuasiInverse ↑u

Tactic:
pkg.eq_equiv

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
u : E →L[𝕜] F
pkg : u.FredholmPackage
⊢ (↑pkg.quasiInverse).IsQuasiInverse ↑(pkg.decCodom.X₁.subtypeL ∘SL ↑pkg.equiv ∘SL pkg.decDom.proj)
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_1
𝕜 : 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✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
v_mapsto : MapsTo ⇑v ↑F₁ ↑E₁
⊢ u.restrict u_mapsto ∘SL v.restrict v_mapsto = ContinuousLinearMap.id 𝕜 ↥F₁

pp: case refine_2
𝕜 : 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✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
v_mapsto : MapsTo ⇑v ↑F₁ ↑E₁
⊢ v.restrict v_mapsto ∘SL u.restrict u_mapsto = ContinuousLinearMap.id 𝕜 ↥E₁

Tactic:
· ext ⟨x, hx : x = u (v x)⟩
    simp [coe_restrict_apply u_mapsto, coe_restrict_apply v_mapsto, ← hx]

Goal state after:
case refine_2
𝕜 : 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✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
v : F →L[𝕜] E
hvu : (LinearMap.id.eqLocus (↑v ∘ₗ ↑u)).CoFG
huv : (LinearMap.id.eqLocus (↑u ∘ₗ ↑v)).CoFG
E₁ : Submodule 𝕜 E := (↑(ContinuousLinearMap.id 𝕜 E)).eqLocus ↑(v ∘SL u)
F₁ : Submodule 𝕜 F := (↑(ContinuousLinearMap.id 𝕜 F)).eqLocus ↑(u ∘SL v)
u_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
v_mapsto : MapsTo ⇑v ↑F₁ ↑E₁
⊢ v.restrict v_mapsto ∘SL u.restrict u_mapsto = ContinuousLinearMap.id 𝕜 ↥E₁
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : 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:
simp only [hP, zero_mul, tendsto_const_nhds_iff] at this

Goal state after:
case pos
𝕜 : 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.leadingCoeff = c ∧ P.degree ≤ 0
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
α : FunSpace t₀ x₀ r L
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)

Tactic:
iterate_succ_apply

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
α : FunSpace t₀ x₀ r L
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i] (next hf hx α)) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)
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
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i + 1] α) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)

Tactic:
iterate_succ_apply

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
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i] ((next hf hx)^[m] α)) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case pos
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 ℝ
h_supp : p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

pp: case neg
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 ℝ
h_supp : ¬p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
· simp only [gaussNorm, h_supp]
    obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)
    exact ⟨i, hi2⟩

Goal state after:
case neg
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 ℝ
h_supp : ¬p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i
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 ℝ
r : R
⊢ gaussNorm v c (C r) = v r

Tactic:
by_cases hr : r = 0

Goal state after:
case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : r = 0
⊢ gaussNorm v c (C r) = v r

case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : ZeroHomClass F R ℝ
r : R
hr : ¬r = 0
⊢ gaussNorm v c (C r) = v r
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

Goal state after:
case pos
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
hr : r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n

case neg
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
hr : ¬r = 0
⊢ gaussNorm v c ((monomial n) r) = v r * c ^ n
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:
by
  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⟩
  refine ⟨Nat.find h_nonempty, Nat.find_spec h_nonempty, ?_⟩
  intro j hj_lt
  simp only [Nat.lt_find_iff, Set.mem_ofPred_eq] at hj_lt
  exact lt_of_le_of_ne (le_gaussNorm v _ hc j) fun a ↦ hj_lt j (Nat.le_refl j) a.symm

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

Goal state before:
pp: case inr.inl
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝ : p ≠ 0
hq : q = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp [hq]

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 ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
j : ℕ
left✝ : j ∈ range (i + 1)
right✝ : v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) ≤ v (p.coeff j * q.coeff (i - j))
⊢ v (p.coeff j) * c ^ j * (v (q.coeff (i - j)) * c ^ (i - j)) ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i

Tactic:
have hp_le := p.le_gaussNorm v hc j

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 ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
j : ℕ
left✝ : j ∈ range (i + 1)
right✝ : v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) ≤ v (p.coeff j * q.coeff (i - j))
hp_le : v (p.coeff j) * c ^ j ≤ gaussNorm v c p
⊢ v (p.coeff j) * c ^ j * (v (q.coeff (i - j)) * c ^ (i - j)) ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
this :
  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
⊢ 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)

Tactic:
simp_rw [this]

Goal state after:
case inl
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
this :
  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
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
this :
  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
⊢ 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)

Tactic:
simp_rw [this]

Goal state after:
case inr
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
this :
  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
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
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
⊢ v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) ≤
    gaussNorm v c p * (v (q.coeff (i + j - x)) * c ^ (i + j - x))

Tactic:
by
        gcongr
        exact p.le_gaussNorm v hc0 x

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

Goal state before:
pp: p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ circleMap 0 1 ''
      {a |
        a ∈ Set.uIoc 0 (2 * π) ∧
          ¬log (‖eval (circleMap 0 1 a) p‖ * ‖eval (circleMap 0 1 a) q‖) =
              log ‖eval (circleMap 0 1 a) p‖ + log ‖eval (circleMap 0 1 a) q‖} ⊆
    {x | x ∈ (p * q).roots}

Tactic:
rintro _ ⟨_, ⟨_, h⟩, _⟩

Goal state after:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
a✝ : ℂ
w✝ : ℝ
right✝ : circleMap 0 1 w✝ = a✝
left✝ : w✝ ∈ Set.uIoc 0 (2 * π)
h :
  ¬log (‖eval (circleMap 0 1 w✝) p‖ * ‖eval (circleMap 0 1 w✝) q‖) =
      log ‖eval (circleMap 0 1 w✝) p‖ + log ‖eval (circleMap 0 1 w✝) q‖
⊢ a✝ ∈ {x | x ∈ (p * q).roots}
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom :
  ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

Tactic:
rw [← vMulEq] at hdom
  rw [coeff_mul, IsNonarchimedean.apply_sum_eq_of_lt vna (by grind) (k := (i, j))
    (s := Finset.antidiagonal (i + j)) (Finset.mem_antidiagonal.mpr rfl) hdom]

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

Goal state before:
pp: p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) p.roots).prod ≠ 0

Tactic:
by simp [hp, X_sub_C_ne_zero]

Goal state after: