mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ (↑1 ^ (u - 1 + 1) - ↑0 ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u

pp: u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re

Tactic:
· rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
    rw [sub_add_cancel]
    contrapose! hu; rw [hu, zero_re]

Goal state after:
u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))
⊢ ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) =
    (↑π * z * ((∏ x ∈ Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * (n + 1))) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1)))

Tactic:
set A := ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)

Goal state after:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
hn :
  Complex.sin (↑π * z) =
    (↑π * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))
⊢ (↑π * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * (n + 1))) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

pp: case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

pp: x : ℝ
n : ℕ
⊢ (x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
    x * log ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

Tactic:
· rw [Nat.cast_ne_zero]; exact Nat.succ_ne_zero n

Goal state after:
case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

x : ℝ
n : ℕ
⊢ (x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
    x * log ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ √π * Γ 1 * 2 ^ (1 - 1) / √π = 1

Tactic:
sub_self,

Goal state after:
⊢ √π * Γ 1 * 2 ^ 0 / √π = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
n : ℕ
⊢ u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)

Tactic:
by
  induction n generalizing u with
  | zero =>
    rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]
    simp
  | succ n IH =>
    have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
    swap; · rw [← ofReal_natCast, ofReal_re]; positivity
    rw [mul_comm u _, ← eq_div_iff] at this
    swap; · contrapose! hu; rw [hu, zero_re]
    rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
    swap; · rw [add_re, one_re]; positivity
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ←
      mul_div_assoc, ← div_div]
    congr 3 with j : 1
    push_cast; abel

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1

Tactic:
norm_inv,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ ‖‖x -ᵥ p‖‖⁻¹ * ‖x -ᵥ p‖ = 1
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
⊢ cobounded P = ⨆ v ∈ Metric.sphere 0 1, asymptoticNhds ℝ P v

Tactic:
refine le_antisymm ?_ <| iSup₂_le fun _ h => asymptoticNhds_le_cobounded <|
    Metric.ne_of_mem_sphere h one_ne_zero
  intro s hs
  have ⟨p⟩ : Nonempty P := inferInstance
  simp_rw [mem_iSup, asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at hs
  choose! t ht u hu smul_subset_s using hs
  have ⟨cover, h₁, h₂⟩ := (isCompact_sphere 0 1).elim_nhds_subcover u hu
  rw [← Metric.comap_dist_left_atTop p]
  refine ⟨Set.Ioi 0 ∩ ⋂ x ∈ cover, t x, inter_mem (Ioi_mem_atTop 0)
    (cover.iInter_mem_sets.mpr fun x hx => ht x (h₁ x hx)), fun x hx => ?_⟩
  rw [Set.mem_preimage, dist_eq_norm_vsub'] at hx
  let x' := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
  have x'_mem : x' ∈ Metric.sphere 0 1 := by
    rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
  have ⟨y, y_mem, hy⟩ := Set.mem_iUnion₂.mp (h₂ x'_mem)
  rw [← vsub_vadd x p, ← show ‖x -ᵥ p‖ • x' = x -ᵥ p from smul_inv_smul₀ hx.1.ne' (x -ᵥ p)]
  exact smul_subset_s y (h₁ y y_mem) <| Set.smul_mem_smul (Set.biInter_subset_of_mem y_mem hx.2) hy

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in map Prod.snd (atTop ×ˢ 𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P x, p y

Tactic:
rw [eventually_map]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P a.2, p y
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
⊢ ∑ j ∈ fsx i, wx i j = 1

Tactic:
← hw i,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
⊢ ∑ j ∈ fsx i, wx i j = ∑ j ∈ fs i, w i j
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (x (s.points 0)) (x (s.points 1))

Tactic:
← Function.comp_apply (f := x),

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist ((⇑x ∘ s.points) 0) ((⇑x ∘ s.points) 1)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ dist (s.points i) (s.points j) = dist (x (s.points 0)) (x (s.points 1))

Tactic:
← Function.comp_apply (f := x),

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ dist (s.points i) (s.points j) = dist ((⇑x ∘ s.points) 0) ((⇑x ∘ s.points) 1)
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x y : ℍ
⊢ (starRingEnd ℝ) ⟪y, x⟫ = ⟪x, y⟫

Tactic:
simp [inner_def, mul_comm]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel :
  ‖x - (algebraMap ℂ F) w‖ * ‖(aeval (x - (algebraMap ℂ F) y)) p‖ =
    ‖(x - (algebraMap ℂ F) y) ^ n - ((algebraMap ℂ F) w - (algebraMap ℂ F) y) ^ n‖
⊢ ‖(x - (algebraMap ℂ F) y) ^ n - ((algebraMap ℂ F) w - (algebraMap ℂ F) y) ^ n‖ ≤ M ^ n + ‖w - y‖ ^ n

Tactic:
exact (norm_sub_le ..).trans <| by simp [hy, ← map_sub]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖(algebraMap ℂ F) (↑‖x‖ + ↑M + 1)‖ - ‖x‖ ≤ M
⊢ False

Tactic:
rw [norm_algebraMap, norm_one, mul_one] at key

Goal state after:
case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖↑‖x‖ + ↑M + 1‖ - ‖x‖ ≤ M
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    ((z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! - (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)!) * I / 2 +
      ((z ^ 2) ^ k * (I ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)! - (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I /
        2

Tactic:
sub_self,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    0 * I / 2 +
      ((z ^ 2) ^ k * (I ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)! - (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I /
        2
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx

Goal state after:
case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : f ↑x = 0
⊢ x = 0

Tactic:
← ZeroMemClass.coe_eq_zero

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : f ↑x = 0
⊢ ↑x = 0
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
r : K
x : L
⊢ (NormedField.toMulRingNorm L).toFun (r • x) = ‖r‖ * (NormedField.toMulRingNorm L).toFun x

Tactic:
simp only [Algebra.smul_def, AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe,
      map_mul, mul_eq_mul_right_iff, map_eq_zero]
    exact Or.inl <| norm_algebraMap' L r

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : ¬seminormFromBounded' f y = 0
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
· intro z
    rw [← div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy)]
    apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z
    rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy),
      div_mul_eq_mul_div]
    by_cases hz : f z = 0
    · have hxyz : f (z * (x * y)) = 0 := map_mul_zero_of_map_zero f_nonneg f_mul hz _
      simp_rw [mul_comm, hxyz, zero_div]
      exact div_nonneg (mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _))
        (f_nonneg _)
    · rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), mul_comm (f (x * z))]
      by_cases hxz : f (x * z) = 0
      · rw [mul_comm x y, mul_assoc, mul_comm y, map_mul_zero_of_map_zero f_nonneg f_mul hxz y]
        exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)
      · rw [← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hxz)]
        apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) (x * z)
        rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hxz), mul_comm x y, mul_assoc]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z

Tactic:
· rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz),
      div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul, ← le_max_iff]
    exact hna _ _

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)

Tactic:
rcases le_max_iff.mp hxy with (hx | hy)

Goal state after:
case inl
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hx : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr x) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)

case inr
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hy : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr y) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: 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
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
⊢ f x = f (x * 1) / f 1

Tactic:
by_cases h0 : f x = 0

Goal state after:
case pos
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
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : f x = 0
⊢ f x = f (x * 1) / f 1

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
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ f x = f (x * 1) / f 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case a
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
⊢ f x ≤ ⨆ y, f (x * y) / f y

Tactic:
· have h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y) := by
      use f x
      rintro r ⟨y, rfl⟩
      by_cases hy0 : f y = 0
      · simp only [hy0, div_zero]
        exact f_nonneg _
      · 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]
        exact hx y
    convert! le_ciSup h_bdd (1 : R)
    by_cases h0 : f x = 0
    · rw [mul_one, h0, zero_div]
    · have heq : f 1 = 1 := by
        apply h_one.antisymm
        specialize hx 1
        rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx
        exact hx
      rw [heq, mul_one, div_one]

Goal state after:
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
h1 : f₁ ↑y = g₁ y
⊢ f₁ x = f₂ x

Tactic:
have h2 : 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
h2 : f₂ ↑y = g₂ y
⊢ f₁ x = f₂ x
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
⊢ f₁ = f₂

Tactic:
ext x
  set g₁ : AlgebraNorm R R[(x : S)] := AlgebraNorm.restriction _ f₁
  set g₂ : AlgebraNorm R R[(x : S)] := AlgebraNorm.restriction _ f₂
  have hg₁_pm : IsPowMul g₁ := IsPowMul.restriction _ hf₁_pm
  have hg₂_pm : IsPowMul g₂ := IsPowMul.restriction _ hf₂_pm
  let y : R[(x : S)] := ⟨x, self_mem_adjoin_singleton R x⟩
  have hy : x = y.val := rfl
  have h1 : f₁ y.val = g₁ y := rfl
  have h2 : f₂ y.val = g₂ y := rfl
  obtain ⟨C₁, C₂, hC₁_pos, hC₂_pos, hC⟩ := h_eq x
  obtain ⟨hC₁, hC₂⟩ := forall_and.mp hC
  rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ seminormFromConst_seq c f 1 =ᶠ[atTop] fun x ↦ 1

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst_seq c f (-x) =ᶠ[atTop] seminormFromConst_seq c f x

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
n : ℕ
⊢ seminormFromConst_seq c f (x ^ m) (m * n) = seminormFromConst_seq c f x n ^ m

Tactic:
simp only [seminormFromConst_seq, div_pow, ← hpm _ hm, ← pow_mul, mul_pow, mul_comm m n]

Goal state after: