mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
⊢ μH[d] s ≤ 1

Tactic:
by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
  · simp only [measure_empty, zero_le]
  · rw [(subsingleton_iff_singleton hx).1 hs]
    rcases eq_or_lt_of_le hd with (rfl | dpos)
    · simp only [le_refl, hausdorffMeasure_zero_singleton]
    · have := nullSingletonClass_hausdorff X dpos
      simp only [zero_le, measure_singleton]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x : X
v : V
⊢ ‖(kerFunAux x) v‖ ≤ √‖K x x‖ * ‖v‖

Tactic:
refine (sq_le_sq₀ (by simp) (by simp [mul_nonneg])).mp ?_
  simp only [LinearMap.coe_mk, AddHom.coe_mk, UniformSpace.Completion.norm_coe,
    ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_self_re_eq_norm]
  simp only [inner_H₀_def, RCLike.star_def, mul_zero, zero_mul,
    Finsupp.sum_single_index, mul_one, map_zero, map_one, one_mul]
  calc
    _ ≤ ‖K x x v‖ * ‖v‖ := by simp [norm_inner_le_norm]
    _ ≤ ‖K x x‖ * ‖v‖ * ‖v‖ := by simp [mul_le_mul_of_nonneg_right, le_opNorm]
    _ ≤ _ := by simp [mul_pow, mul_assoc, ← sq]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑K ^ d * ediam (i_1 i) ^ d

Tactic:
refine le_iSup₂_of_le (ε / K) (by simp [ε0.ne']) ?_

Goal state after:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨅ i,
      ⨅ (_ : s ⊆ ⋃ n, i n),
        ⨅ (_ : ∀ (n : ℕ), ediam (i n) ≤ ε / ↑K), ∑' (i_1 : ℕ), ⨆ (_ : (i i_1).Nonempty), ↑K ^ d * ediam (i i_1) ^ d
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ = ‖x‖

Tactic:
LinearMap.id_apply

Goal state after:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖x‖ = ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x y : E →SWOT[σ] F
⊢ (fun x_1 ↦
      match x_1 with
      | (x_2, y_1) => y_1 ((x + y) x_2)) =
    (fun x_1 ↦
        match x_1 with
        | (x_2, y) => y (x x_2)) +
      fun x ↦
      match x with
      | (x, y_1) => y_1 (y x)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
⊢ (fun x_1 ↦
      match x_1 with
      | (x_2, y_1) => y_1 ((x • y) x_2)) =
    (RingHom.id 𝕜₂) x • fun x ↦
      match x with
      | (x, y_1) => y_1 (y x)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.normSq ((o.kahler x) y) = (‖x‖ * ‖y‖) ^ 2

Tactic:
linear_combination o.normSq_kahler x y

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u)) =
    ∫ (u : ℝ), cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
by
      congr
      ext u
      trans Complex.exp (-s.im * u * I) • (Real.exp (-s.re * u) • f (Real.exp (-u)))
      · conv => lhs; rw [← re_add_im s]
        rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]
        norm_cast
        push_cast
        ring_nf
      congr
      simp [field]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1) ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖

Tactic:
rw [mul_div_assoc, mul_comm, norm_pow]

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ (1 - ‖z‖)⁻¹ / (↑n + 1) * ‖z‖ ^ (n + 1) ≤ 2 / (↑n + 1) * ‖z‖ ^ (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(n - 1) = ↑n - 1

Tactic:
Nat.cast_sub (one_le_two.trans hn),

Goal state after:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑n - ↑1 = ↑n - 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ (-1) ^ (n + 1) * z ^ n / ↑n) (log (1 + z))

Tactic:
refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_
  · 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
  · rw [← tendsto_sub_nhds_zero_iff]
    conv => enter [1, x]; rw [← div_one (_ - _), ← logTaylor]
    rw [← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim]
    refine IsLittleO.trans_isBigO ?_ <| isBigO_const_one ℂ (1 : ℝ) atTop
    have H : (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] (fun n : ℕ ↦ ‖z‖ ^ n) := by
      have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
      exact (isBigOWith_of_le' atTop this).isBigO
    refine IsBigO.trans_isLittleO H ?_
    convert! isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz
    exact (one_pow _).symm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine this ⌈x - 1⌉₊ ?_ ?_
    · rcases lt_or_ge x 1 with ⟨⟩
      · rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
      · convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
        abel
    · rw [← sub_le_iff_le_add]; exact Nat.le_ceil _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
⊢ EqOn f Γ (Ioi 0)

Tactic:
suffices EqOn (log ∘ f) (log ∘ Gamma) (Ioi (0 : ℝ)) from
    fun x hx ↦ log_injOn_pos (hf_pos hx) (Gamma_pos_of_pos hx) (this hx)

Goal state after:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
⊢ EqOn (log ∘ f) (log ∘ Γ) (Ioi 0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
rw [Function.comp_apply (f := log) (g := f) (x := 1), hf_one, log_one, sub_zero] at e1

Goal state after:
case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
⊢ (log ∘ f) x = (log ∘ Γ) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2))

pp: case refine_2
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2 + 1 / 2))

pp: case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2

Tactic:
· convert!
      convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap
      using 1
    · simpa only [zero_div] using! (preimage_const_mul_Ioi₀ (0 : ℝ) one_half_pos).symm
    · ext1 x
      simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribSMul.toLinearMap_apply]
      rw [smul_eq_mul, mul_comm, mul_one_div]

Goal state after:
case refine_2
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2 + 1 / 2))

case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ (↑↑k * ↑π).im

Tactic:
← ofReal_mul,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ (↑(↑k * π)).im
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) ≤ toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
x : R
⊢ toAddGroupSeminorm✝¹ x = toAddGroupSeminorm✝ x

Tactic:
exact congr_fun h x

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
h1 : f 1 = 0
⊢ False

Tactic:
h1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f (1 * y) ≤ c * 0 * f y
⊢ False
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ toRingSeminorm✝¹ x = toRingSeminorm✝ x

Tactic:
exact congr_fun h x

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
x : R
⊢ toAddGroupSeminorm✝¹ x = toAddGroupSeminorm✝ x

Tactic:
exact congr_fun h x

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ toMulRingSeminorm✝¹ x = toMulRingSeminorm✝ x

Tactic:
exact congr_fun h x

Goal state after:
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
x : R
f_mul : f x ≤ c * f x * f 1
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
h1,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : f x ≤ c * f x * 0
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
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
x : R
f_mul : f x ≤ 0
h1 : f 1 = 0
hx0 : f x = 0
⊢ 0 ≤ f 1 * seminormFromBounded' f x

Tactic:
h1,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : f x ≤ 0
h1 : f 1 = 0
hx0 : f x = 0
⊢ 0 ≤ 0 * seminormFromBounded' f x
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ (g - f).natDegree < g.natDegree + 1

Tactic:
· simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f

Goal state after:
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
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
seminormFromBounded_eq_zero_iff f_nonneg f_mul

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
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
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
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)
h1 : 1 = (algebraMap K L) 1
⊢ 0 < B.norm 1

Tactic:
h1,

Goal state after:
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)
h1 : 1 = (algebraMap K L) 1
⊢ 0 < B.norm ((algebraMap K L) 1)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

Tactic:
exact hx y

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✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f

Tactic:
have hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖ := Basis.norm_extends hB1

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f
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
h2 : f₂ ↑y = g₂ y
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1 ∧ f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
hC₁ : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥R[x]), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ f₁ ↑y = f₂ ↑y

Tactic:
h1,

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
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1 ∧ f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
hC₁ : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥R[x]), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ g₁ y = f₂ ↑y
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ ‖x⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
x✝¹ : F × F
x y : F
x✝ : (x, y).1 ≠ 0 ∧ (x, y).2 ≠ 0
hx : (x, y).1 ≠ 0
hy : (x, y).2 ≠ 0
⊢ (x, y).1⁻¹ - (x, y).2⁻¹ = (x, y).1⁻¹ * ((x, y).2 - (x, y).1) * (x, y).2⁻¹

Tactic:
simp [mul_sub, sub_mul, hx, hy]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : Tendsto (⇑f) (cocompact E) (cocompact F)
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖

Tactic:
rw [tendsto_def] at h

Goal state after:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : ∀ s ∈ cocompact F, ⇑f ⁻¹' s ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
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) ≤ ε / 2

Tactic:
nth_rw 3 [← mul_one (L + ε / 2)]

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