mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.hg
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ HasFiniteIntegral (fun t ↦ d * t ^ (s - b - 1)) (volume.restrict (Ioo 0 ε))

Tactic:
refine (Integrable.hasFiniteIntegral ?_).const_mul _

Goal state after:
case refine_2.hg
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ Integrable (fun t ↦ t ^ (s - b - 1)) (volume.restrict (Ioo 0 ε))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
⊢ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi 0) volume

Tactic:
obtain ⟨c1, hc1, hc1'⟩ := mellin_convergent_top_of_isBigO hfc.aestronglyMeasurable hf_top hs_top

Goal state after:
a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
⊢ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_1
z : ℂ
hz : ‖z‖ < 1
⊢ Summable fun i ↦ ‖(-1) ^ (i + 1) * z ^ i / ↑i‖

Tactic:
refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_
    intro n
    simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]
    rcases n.eq_zero_or_pos with rfl | hn
    · simp
    conv => enter [2]; rw [← div_one (‖z‖ ^ n)]
    gcongr
    norm_cast

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
⊢ ‖↑t ^ (z - 1)‖ * ‖log t‖ * ‖f t‖ ≤ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖

Tactic:
mul_assoc,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
⊢ ‖↑t ^ (z - 1)‖ * (‖log t‖ * ‖f t‖) ≤ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * (|log t| * ‖f t‖)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1)) * ∫ (x : ℝ) in 0..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)

Tactic:
mul_assoc,

Goal state after:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1) * ∫ (x : ℝ) in 0..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ↑(rexp (-x)) * ↑x ^ (s + t - 1) * s.betaIntegral t

Tactic:
mul_assoc,

Goal state after:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ↑(rexp (-x)) * (↑x ^ (s + t - 1) * s.betaIntegral t)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
⊢ ↑(Gamma s) * ↑(Gamma (1 - s)) = ↑π / Complex.sin (↑π * ↑s)

Tactic:
←
    Complex.Gamma_ofReal,

Goal state after:
s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma ↑(1 - s) = ↑π / Complex.sin (↑π * ↑s)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π

Tactic:
suffices (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z =>
      (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π) by
    convert! congr_arg Inv.inv (congr_fun this s) using 1
    · rw [mul_inv, inv_inv, inv_inv]
    · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
  have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by
    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
    refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
    exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
  have h2 : AnalyticOnNhd ℂ
      (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ := by
    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
    refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
    apply Differentiable.mul
    · exact differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)
    · refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)
      exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
  have h3 : Tendsto ((↑) : ℝ → ℂ) (𝓝[≠] 1) (𝓝[≠] 1) := by
    rw [tendsto_nhdsWithin_iff]; constructor
    · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
    · exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)
  refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)
  refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently
  refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)
  rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]

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

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) =
    inl (∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) + inr ((∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) • x.snd)

pp: case neg
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) =
    inl (∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) + inr ((∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) • x.snd)

Tactic:
· refine (hasSum_expSeries_of_smul_comm ℚ x hx ?_).tsum_eq
    exact h.hasSum

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h : ¬Summable fun n ↦ (expSeries ℚ R n) fun x_1 ↦ x.fst
⊢ (∑' (n : ℕ), (expSeries ℚ (tsze R M) n) fun x_1 ↦ x) =
    inl (∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) + inr ((∑' (n : ℕ), (expSeries ℚ R n) fun x_1 ↦ x.fst) • x.snd)
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)

Tactic:
gcongr
      · apply norm_mul_le
      · refine norm_add_le_of_le ?_ ?_ <;>
        apply norm_smul_le

Goal state after:
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 =
    -(2 * ((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I / 2)

Tactic:
mul_assoc,

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 =
    -(2 * ((z ^ 2) ^ k * ((I ^ 2) ^ k * (z * I)) / ↑(2 * k + 1)! * I) / 2)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
⊢ exp q = exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

Tactic:
let +nondep : NormedAlgebra ℚ ℍ := .restrictScalars ℚ ℝ ℍ

Goal state after:
q : ℍ
this : NormedAlgebra ℚ ℍ
⊢ exp q = exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq ↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) ^ 2 * normSq q.im +
      2 * (↑(Real.cos ‖q.im‖) * (Real.sin ‖q.im‖ / ‖q.im‖) • star q.im).re =
    Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
coe_mul_eq_smul,

Goal state after:
case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq ↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) ^ 2 * normSq q.im +
      2 * (Real.cos ‖q.im‖ • (Real.sin ‖q.im‖ / ‖q.im‖) • star q.im).re =
    Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
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
hf1 : f 1 = 1
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

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
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
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 : f y = 0
z : R
⊢ f (y * x * z) / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
mul_assoc,

Goal state after:
case pos
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 : f y = 0
z : R
⊢ f (y * (x * z)) / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
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
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ f (y * x * z) ≤ seminormFromBounded' f y * f (x * z)

Tactic:
mul_assoc,

Goal state after:
case pos
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
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ f (y * (x * z)) ≤ seminormFromBounded' f y * f (x * z)
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case h.h
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
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖
k' : ι
hk' : ‖∑ j, (B.repr y) j • (B.repr (B k * B j)) ixy‖ ≤ ‖(B.repr y) k' • (B.repr (B k * B k')) ixy‖
⊢ ‖(B.repr x) k‖ * (‖(B.repr y) k'‖ * ‖(B.repr (B k * B k')) ixy‖) ≤ B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
mul_assoc,

Goal state after:
case h.h
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
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖
k' : ι
hk' : ‖∑ j, (B.repr y) j • (B.repr (B k * B j)) ixy‖ ≤ ‖(B.repr y) k' • (B.repr (B k * B k')) ixy‖
⊢ ‖(B.repr x) k‖ * (‖(B.repr y) k'‖ * ‖(B.repr (B k * B k')) ixy‖) ≤ B.norm (B c.1 * B c.2) * (B.norm x * B.norm y)
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
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ f x = f (x * 1) / f 1

Tactic:
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.SeminormFromConst

Goal state before:
pp: case inr
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 n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * (f c ^ n * (f c ^ m)⁻¹ * (f c ^ n)⁻¹) ≤ f (x * c ^ m) / f c ^ m

Tactic:
mul_assoc,

Goal state after:
case inr
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 n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * (f c ^ n * ((f c ^ m)⁻¹ * (f c ^ n)⁻¹)) ≤ f (x * c ^ m) / f c ^ m
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 y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (c ^ n * x * y * c ^ n) ≤ f (x * c ^ n) * f (y * c ^ n)

Tactic:
mul_assoc,

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 y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (c ^ n * x * (y * c ^ n)) ≤ f (x * c ^ n) * f (y * c ^ n)
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
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n ∨ f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n

Tactic:
apply hmax.imp <;> intro <;> gcongr

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

Goal state before:
pp: 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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - (L + ε / 2) * 1 ≤ ε / 2

Tactic:
mul_assoc,

Goal state after:
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
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) * ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) - (L + ε / 2) * 1 ≤ ε / 2
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ ↑(Hom.hom (f ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯)) x = ↑(Hom.hom (0 ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯)) x

Tactic:
rw [Limits.zero_comp, comp_apply, SemiNormedGrp₁.mkHom_apply,
        SemiNormedGrp₁.zero_apply, ← NormedAddGroupHom.mem_ker, f.hom.1.range.ker_normedMk,
        f.hom.1.mem_range]

Goal state after:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ ∃ w, ↑(Hom.hom f) w = ↑(Hom.hom f) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g : V ⟶ W
c : Fork f g
⊢ (NormedAddGroupHom.compHom (Hom.hom f)) (Hom.hom c.ι) = (NormedAddGroupHom.compHom (Hom.hom g)) (Hom.hom c.ι)

Tactic:
exact congr_arg Hom.hom c.condition

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

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂

Tactic:
let g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
  have w : f ≫ g = 0 := by simp [g]
  have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
  rw [this]
  apply explicitCokernelDesc_unique
  exact h

Goal state after: