awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h :
  ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦
      fst.{u_3, u_4} (M := M)
        ((expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)
⊢ (Summable (α := tsze R M) fun (n : ℕ) ↦
      (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) →
    Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦
      fst.{u_3, u_4} (M := M)
        ((expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)

Tactic:
(Summable.map · (TrivSqZeroExt.fstHom ℚ R M).toLinearMap continuous_fst)

Premises used: AlgHom.toLinearMap, Rat, TrivSqZeroExt.fst, TrivSqZeroExt.fstHom, TrivSqZeroExt.continuous_fst, Summable.map
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
h :
  ¬Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦
      fst.{u_3, u_4} (M := M)
        ((expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)
⊢ (Summable (α := tsze R M) fun (n : ℕ) ↦
      (expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) →
    Summable.{u_3, 0} (α := R) fun (n : ℕ) ↦
      fst.{u_3, u_4} (M := M)
        ((expSeries ℚ (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x)

Tactic:
exact (Summable.map · (TrivSqZeroExt.fstHom ℚ R M).toLinearMap continuous_fst)

Premises used: AlgHom.toLinearMap, Rat, TrivSqZeroExt.fstHom, TrivSqZeroExt.continuous_fst, Summable.map
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : R
hx :
  HSMul.hSMul (β := M) (MulOpposite.op (fst.{u_3, u_4} (M := M) (inl x))) (snd (inl x)) =
    HSMul.hSMul (β := M) (fst.{u_3, u_4} (M := M) (inl x)) (snd (inl x))
⊢ Eq (α := tsze R M) (exp (inl x)) (inl (exp x))

Tactic:
rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]

Premises used: smul_zero, TrivSqZeroExt.snd_inl, TrivSqZeroExt.inr_zero, TrivSqZeroExt.exp_def_of_smul_comm, add_zero, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
x : R
hx :
  HSMul.hSMul (β := M) (MulOpposite.op (fst.{u_3, u_4} (M := M) (inl x))) 0 =
    HSMul.hSMul (β := M) (fst.{u_3, u_4} (M := M) (inl x)) 0
hx₁ : HSMul.hSMul (β := M) (MulOpposite.op x) 0 = HSMul.hSMul (β := M) x 0
hx₂ : 0 = HSMul.hSMul (β := M) x 0
hx₃ hx₄ : Eq.{u_4 + 1} (α := M) 0 0
⊢ HSMul.hSMul (β := M) (MulOpposite.op (fst.{u_3, u_4} (M := M) (inl x))) (snd (inl x)) =
    HSMul.hSMul (β := M) (fst.{u_3, u_4} (M := M) (inl x)) (snd (inl x))

Tactic:
rw [snd_inl, fst_inl, smul_zero, smul_zero]

Premises used: smul_zero, TrivSqZeroExt.snd_inl, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
m : M
hx :
  HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) (MulOpposite.op (fst (inr m))) (snd.{u_3, u_4} (R := R) (inr m)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (fst (inr m)) (snd.{u_3, u_4} (R := R) (inr m))
⊢ exp (inr m) = HAdd.hAdd (α := tsze R M) 1 (inr m)

Tactic:
rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]

Premises used: TrivSqZeroExt.snd_inr, TrivSqZeroExt.fst_inr, one_smul, NormedSpace.exp_zero, TrivSqZeroExt.exp_def_of_smul_comm, TrivSqZeroExt.inl_one
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace M
inst_7 : IsTopologicalRing R
inst_8 : IsTopologicalAddGroup M
inst_9 : ContinuousSMul R M
inst_10 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : Algebra ℚ R
inst_12 : Module ℚ M
inst_13 : T2Space R
inst_14 : T2Space M
m : M
hx :
  HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) (MulOpposite.op (fst (inr m))) m =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (fst (inr m)) m
hx₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) (MulOpposite.op 0) m = HSMul.hSMul.{u_3, u_4, u_4} (α := R) 0 m
hx₂ : HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) 0 m = HSMul.hSMul.{u_3, u_4, u_4} (α := R) 0 m
hx₃ : 0 = HSMul.hSMul.{u_3, u_4, u_4} (α := R) 0 m
hx₄ hx₅ : Eq.{u_4 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) (MulOpposite.op (fst (inr m))) (snd.{u_3, u_4} (R := R) (inr m)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (fst (inr m)) (snd.{u_3, u_4} (R := R) (inr m))

Tactic:
rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]

Premises used: TrivSqZeroExt.snd_inr, TrivSqZeroExt.fst_inr, MulOpposite.op_zero, zero_smul
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Algebra ℚ R
inst_3 : Module ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace M
inst_9 : IsTopologicalRing R
inst_10 : IsTopologicalAddGroup M
inst_11 : ContinuousSMul R M
inst_12 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
⊢ exp x = inl (exp x.fst) + inr (exp x.fst • x.snd)

Tactic:
exp_def_of_smul_comm x (op_smul_eq_smul _ _)

Premises used: TrivSqZeroExt.exp_def_of_smul_comm, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Algebra ℚ R
inst_3 : Module ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace M
inst_9 : IsTopologicalRing R
inst_10 : IsTopologicalAddGroup M
inst_11 : ContinuousSMul R M
inst_12 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).fst = exp x.fst
rw₁ : fst.{u_3, u_4} (M := M) (inl (exp x.fst)) + fst (inr (exp x.fst • x.snd)) = exp x.fst
rw₂ : exp x.fst + fst (inr (exp x.fst • x.snd)) = exp x.fst
rw₃ : exp x.fst + 0 = exp x.fst
rw₄ rw₅ : exp x.fst = exp x.fst
⊢ (exp x).fst = exp x.fst

Tactic:
rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]

Premises used: TrivSqZeroExt.fst_inr, TrivSqZeroExt.fst_add, TrivSqZeroExt.exp_def, add_zero, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Algebra ℚ R
inst_3 : Module ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace M
inst_9 : IsTopologicalRing R
inst_10 : IsTopologicalAddGroup M
inst_11 : ContinuousSMul R M
inst_12 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).snd = exp x.fst • x.snd
rw₁ : snd (inl (exp x.fst)) + snd.{u_3, u_4} (R := R) (inr (exp x.fst • x.snd)) = exp x.fst • x.snd
rw₂ : 0 + snd.{u_3, u_4} (R := R) (inr (exp x.fst • x.snd)) = exp x.fst • x.snd
rw₃ : 0 + exp x.fst • x.snd = exp x.fst • x.snd
rw₄ rw₅ : exp x.fst • x.snd = exp x.fst • x.snd
⊢ (exp x).snd = exp x.fst • x.snd

Tactic:
rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]

Premises used: TrivSqZeroExt.snd_add, TrivSqZeroExt.snd_inr, zero_add, TrivSqZeroExt.exp_def, TrivSqZeroExt.snd_inl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Algebra ℚ R
inst_3 : Module ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace M
inst_9 : IsTopologicalRing R
inst_10 : IsTopologicalAddGroup M
inst_11 : ContinuousSMul R M
inst_12 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
inst_15 : Invertible x.fst
rw :
  x =
    HSMul.hSMul (β := tsze R M) x.fst
      (exp (inr (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd)))
rw₁ :
  x =
    x.fst • HAdd.hAdd (α := tsze R M) 1 (inr (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd))
rw₂ :
  x =
    HSMul.hSMul (β := tsze R M) x.fst 1 +
      HSMul.hSMul (β := tsze R M) x.fst (inr (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd))
rw₃ :
  x =
    HSMul.hSMul (β := tsze R M) x.fst (inl 1) +
      HSMul.hSMul (β := tsze R M) x.fst (inr (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd))
rw₄ :
  x =
    inl (HSMul.hSMul (β := R) x.fst 1) +
      HSMul.hSMul (β := tsze R M) x.fst (inr (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd))
rw₅ :
  x =
    inl (HSMul.hSMul (β := R) x.fst 1) +
      inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd)
rw₆ : x = inl (x.fst * 1) + inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd)
rw₇ : x = inl x.fst + inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • x.snd)
rw₈ : x = inl x.fst + inr ((x.fst * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) • x.snd)
rw₉ : x = inl x.fst + inr (HSMul.hSMul.{u_3, u_4, u_4} (α := R) 1 x.snd)
rw₁₀ : x = inl x.fst + inr x.snd
rw₁₁ rw₁₂ : x = x
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))

Tactic:
rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one,
    smul_smul, mul_invOf_self, one_smul, inl_fst_add_inr_snd_eq]

Premises used: TrivSqZeroExt.exp_inr, TrivSqZeroExt.inl_fst_add_inr_snd_eq, smul_smul, TrivSqZeroExt.inl_smul, mul_invOf_self, one_smul, TrivSqZeroExt.inr_smul, smul_eq_mul, mul_one, smul_add, TrivSqZeroExt.inl_one
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : Field R
inst_1 : AddCommGroup M
inst_2 : Algebra ℚ R
inst_3 : Module ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace M
inst_9 : IsTopologicalRing R
inst_10 : IsTopologicalAddGroup M
inst_11 : ContinuousSMul R M
inst_12 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_13 : T2Space R
inst_14 : T2Space M
x : tsze R M
hx : x.fst ≠ 0
⊢ x = x.fst • exp (HSMul.hSMul (β := tsze R M) x.fst⁻¹ (inr x.snd))

Tactic:
letI : Invertible x.fst := invertibleOfNonzero hx
  eq_smul_exp_of_invertible _

Premises used: TrivSqZeroExt.eq_smul_exp_of_invertible
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
⊢ Eq (α := UniformSpace (tsze R M)) instUniformSpace PseudoMetricSpace.toUniformSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
⊢ 0 < ENNReal.toReal 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
rw :
  (‖WithLp.fst (p := 1) (WithLp.toLp 1 x)‖ ^ ENNReal.toReal 1 +
        ‖WithLp.snd (p := 1) (WithLp.toLp 1 x)‖ ^ ENNReal.toReal 1) ^
      (1 / ENNReal.toReal 1) =
    ‖x.fst‖ + ‖x.snd‖
⊢ norm (E := WithLp 1 (R × M)) (WithLp.toLp 1 x) = ‖x.fst‖ + ‖x.snd‖

Tactic:
rw [WithLp.prod_norm_eq_add (by norm_num)]

Premises used: WithLp.prod_norm_eq_add
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
⊢ (‖WithLp.fst (p := 1) (WithLp.toLp 1 x)‖ ^ ENNReal.toReal 1 +
        ‖WithLp.snd (p := 1) (WithLp.toLp 1 x)‖ ^ ENNReal.toReal 1) ^
      (1 / ENNReal.toReal 1) =
    ‖x.fst‖ + ‖x.snd‖

Tactic:
simp only [WithLp.toLp_fst, ENNReal.toReal_one, Real.rpow_one, WithLp.toLp_snd, ne_eq,
    one_ne_zero, not_false_eq_true, div_self, fst, snd]

Premises used: TrivSqZeroExt.snd, WithLp.toLp_snd, ENNReal.toReal_one, ne_eq, TrivSqZeroExt.fst, Real.rpow_one, WithLp.toLp_fst, one_ne_zero, not_false_eq_true, div_self
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
a : (↑‖x‖₊ : ℝ) = (↑(‖x.fst‖₊ + ‖x.snd‖₊) : ℝ)
⊢ ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
⊢ (↑‖x‖₊ : ℝ) = (↑(‖x.fst‖₊ + ‖x.snd‖₊) : ℝ)

Tactic:
simp [norm_def]

Premises used: TrivSqZeroExt.norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
r : R
⊢ norm (E := tsze R M) (inl r) = ‖r‖

Tactic:
simp [norm_def]

Premises used: TrivSqZeroExt.norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
m : M
⊢ norm (E := tsze R M) (inr m) = ‖m‖

Tactic:
simp [norm_def]

Premises used: TrivSqZeroExt.norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
r : R
⊢ nnnorm (E := tsze R M) (inl r) = ‖r‖₊

Tactic:
simp [nnnorm_def]

Premises used: TrivSqZeroExt.nnnorm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
m : M
⊢ nnnorm (E := tsze R M) (inr m) = ‖m‖₊

Tactic:
simp [nnnorm_def]

Premises used: TrivSqZeroExt.nnnorm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
simp_rw :
  ‖((r₁, m₁) * (r₂, m₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
    (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)
⊢ ‖(r₁, m₁) * (r₂, m₂)‖ ≤ ‖(r₁, m₁)‖ * ‖(r₂, m₂)‖

Tactic:
simp_rw [norm_def]

Premises used: TrivSqZeroExt.norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
h₁ : ‖r₁ * r₂‖ ≤ ‖r₁‖ * ‖r₂‖
h₂ : ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖
⊢ ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ * r₂‖ ≤ ‖r₁‖ * ‖r₂‖

Tactic:
apply norm_mul_le

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖

Tactic:
norm_add_le_of_le ?_ ?_

Premises used: norm_add_le_of_le
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
h₂ : ‖r₁ • m₂‖ ≤ ‖r₁‖ * ‖m₂‖
h₃ : ‖MulOpposite.op r₂ • m₁‖ ≤ ‖r₂‖ * ‖m₁‖
⊢ ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖

Tactic:
refine norm_add_le_of_le ?_ ?_

Premises used: norm_add_le_of_le
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ • m₂‖ ≤ ‖r₁‖ * ‖m₂‖

Tactic:
apply norm_smul_le

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖MulOpposite.op r₂ • m₁‖ ≤ ‖r₂‖ * ‖m₁‖

Tactic:
apply norm_smul_le

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
h : 0 ≤ ‖m₁‖ * ‖m₂‖
⊢ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖

Tactic:
apply le_add_of_nonneg_right

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ 0 ≤ ‖m₁‖ * ‖m₂‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖)

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
calc : ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)
calc₁ : ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖
calc₂ : ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖)
⊢ ‖((r₁, m₁) * (r₂, m₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
    (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)

Tactic:
calc ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
      gcongr
      · apply norm_mul_le
      · refine norm_add_le_of_le ?_ ?_ <;>
        apply norm_smul_le
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) := by
      apply le_add_of_nonneg_right
      positivity
    _ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring

Premises used: Norm.norm, HMul.hMul, HAdd.hAdd, MulOpposite.op
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
⊢ IsBoundedSMul S (tsze R M)

Tactic:
WithLp.isBoundedSMulSeminormedAddCommGroupToProd 1 R M

Premises used: TrivSqZeroExt.snd, WithLp.isBoundedSMulSeminormedAddCommGroupToProd, TrivSqZeroExt, Set.Mem, setOf, TrivSqZeroExt.fst, OfNat.ofNat