mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ ((↑(n + 1) * ↑n.factorial)⁻¹ * ↑(n + 1)) • x.fst ^ n • x.snd = (↑n.factorial)⁻¹ • x.fst ^ n • x.snd

Tactic:
mul_inv_rev,

Goal state after:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ ((↑n.factorial)⁻¹ * (↑(n + 1))⁻¹ * ↑(n + 1)) • x.fst ^ n • x.snd = (↑n.factorial)⁻¹ • x.fst ^ n • x.snd
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun n ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * (1 + 0)))
⊢ Tendsto ?m.248 ?m.251 (𝓝 M)

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z + w) = ↑z + ↑w

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: r : ℝ
z : ℂ
⊢ r • ↑z = ↑r * ↑z

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: ⊢ Continuous ⇑normSq

Tactic:
by
  simpa [← normSq_eq_norm_mul_self] using
    (continuous_norm.fun_mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f fun x ↦ u x * v x
a : ℝ
⊢ a ≥ 0 → a < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a * b' ≤ liminf (u * v) f

Tactic:
a0

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f fun x ↦ u x * v x
a : ℝ
a0 : a ≥ 0
⊢ a < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a * b' ≤ liminf (u * v) f
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: 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
⊢ seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
apply ciSup_le
  by_cases hy : seminormFromBounded' f y = 0
  · rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy
    intro z
    rw [mul_comm x y, mul_assoc, map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z), zero_div]
    exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x)
      (seminormFromBounded_nonneg f_nonneg f_mul y)
  · 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.Field.Approximation

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
⊢ ∃ g, g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < ε

Tactic:
by_cases h : f.natDegree = 0
  · use 1
    rw [hf.natDegree_eq_zero.mp]
    · simp only [monic_one, natDegree_one, Polynomial.map_one, sub_self, norm_zero, hε,
      implies_true, and_self]
    · exact h
  choose c hc using fun i ↦ Metric.denseRange_iff.mp hd (f.coeff i) ε hε
  have hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree
      = f.natDegree := by
    calc
      _ = (C (1 : K) * X ^ f.natDegree).natDegree := by
        apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
        simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
        rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]
        apply Polynomial.natDegree_sum_le_of_forall_le
        refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
        simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi
      _ = f.natDegree := by
        simp
  use C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i
  refine ⟨?_, hdeg.symm, fun n ↦ ?_⟩
  · rw [Monic, leadingCoeff, hdeg]
    simp
  · rcases lt_trichotomy n f.natDegree with h | h | h
    · simpa [h, ne_of_lt h, ← dist_eq_norm_sub'] using hc n
    · simp [h, hf, hε]
    · simp [not_lt_of_gt h, ne_of_gt h, coeff_eq_zero_of_natDegree_lt h, hε]

Goal state after:
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‖
⊢ ‖(∑ x_1, B.repr ((B.repr x) x_1 • (B x_1 * ∑ i, (B.repr y) i • B i))) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
map_smul,

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‖
⊢ ‖(∑ x_1, (B.repr x) x_1 • B.repr (B x_1 * ∑ i, (B.repr y) i • B i)) 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: 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
⊢ seminormFromBounded' f x = f x

Tactic:
seminormFromBounded'

Goal state after:
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, f (x * y) / f y = f x
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 / f y) * f y

Tactic:
div_self hy0,

Goal state after:
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 * 1 * f y
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
k : K
y : E
⊢ (spectralAlgNorm K L) ↑(id2 (k • y)) ≤ ‖k‖ * (spectralAlgNorm K L) ↑(id2 y)

Tactic:
map_smul,

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
k : K
y : E
⊢ (spectralAlgNorm K L) ↑(k • id2 y) ≤ ‖k‖ * (spectralAlgNorm K L) ↑(id2 y)
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:
by
  rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]

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

Goal state before:
pp: R : Type u_1
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x y : L
⊢ spectralNorm K L (x - y) = spectralNorm K L (-x + y)

Tactic:
by
      rw [← spectralNorm_neg, sub_eq_add_neg, neg_add, neg_neg]
      exact Algebra.IsAlgebraic.isAlgebraic (x - y)

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

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
⊢ Multiset.count r (Multiset.replicate (minpoly K x).natDegree ((spectralMulAlgNorm K E) ((algebraMap L E) x))) =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)

Tactic:
Multiset.count_replicate

Goal state after:
K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
⊢ (if (spectralMulAlgNorm K E) ((algebraMap L E) x) = r then (minpoly K x).natDegree else 0) =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖

Tactic:
by
  simpa using ContinuousLinearMap.le_of_opNorm_le _ (inclusionInDoubleDual_norm_le 𝕜 E) x

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
this : ∀ {U : Set ℝ}, IsOpen U → 0 ∉ U → ∀ x ∈ U, 0 < x → U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)
hx₀ : 0 < -x
⊢ 0 ∉ -U

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
this : ∀ {U : Set ℝ}, IsOpen U → 0 ∉ U → ∀ x ∈ U, 0 < x → U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) x ↑y)
hx₀ : 0 < -x
⊢ -x ∈ -U

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ≤ P ⊔ Q

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ (P ⊔ Q))
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ Q ≤ P ⊔ Q

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑Q = ↑(Q ⊓ (P ⊔ Q))
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 ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1

Tactic:
show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring

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
⊢ ‖∏ i ∈ t, (1 + f i) - 1 + f x * ∏ x ∈ t, (1 + f x)‖ ≤ Real.exp ‖f x‖ * Real.exp (∑ x ∈ t, ‖f x‖) - 1
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ R) → Q ≤ R → P ⊔ Q ≤ R
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ R) → Q ≤ R → P ⊔ Q ≤ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ R) → ↑Q = ↑(Q ⊓ R) → P ⊔ Q ≤ R
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ R) → ↑Q = ↑(Q ⊓ R) → P ⊔ Q ≤ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ R) → ↑Q = ↑(Q ⊓ R) → ↑(P ⊔ Q) = ↑((P ⊔ Q) ⊓ R)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ P

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑(P ⊓ Q) = ↑(P ⊓ Q ⊓ P)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ Q

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑(P ⊓ Q) = ↑(P ⊓ Q ⊓ Q)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ Q → P ≤ R → P ≤ Q ⊓ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ Q) → P ≤ R → P ≤ Q ⊓ R
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ Q) → P ≤ R → P ≤ Q ⊓ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ Q) → ↑P = ↑(P ⊓ R) → P ≤ Q ⊓ R
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ Q) → ↑P = ↑(P ⊓ R) → P ≤ Q ⊓ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑(P ⊓ Q) → ↑P = ↑(P ⊓ R) → ↑P = ↑(P ⊓ (Q ⊓ R))
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove ((fun x ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x ∈ {x | x.re ≤ ?m.93}

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R

Tactic:
le_def,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑((P ⊔ Q) ⊓ (P ⊔ R) ⊓ (P ⊔ Q ⊓ R))
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: case e'_5
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
x✝¹ : Finset ι
x✝ : ↑K
⊢ ∏ i ∈ x✝¹, (1 + f i ↑x✝) = (∏ b ∈ x✝¹, (fun i ↦ 1 + f' i) b) x✝

pp: case e'_6
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
⊢ (fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val = ⇑(∏' (b : ι), (1 + f' b))

Tactic:
· simp [f']

Goal state after:
case e'_6
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
⊢ (fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val = ⇑(∏' (b : ι), (1 + f' b))
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
⊢ ‖{ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ K * ‖x‖

Tactic:
by
      rw [← norm_toNorm]
      conv_rhs => rw [← norm_toNorm, ← abs_of_nonneg hK, ← Real.norm_eq_abs, ← norm_smul]
      apply norm_mono (zero_lt_one.trans_le Fact.out).ne' fun i ↦ ?_
      simpa [abs_of_nonneg hK] using key ..

Goal state after: