awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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))
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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))
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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))
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₅ : x =
  inl (HSMul.hSMul (β := R) x.fst 1) +
    inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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)
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₆ : x = inl (x.fst * 1) + inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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)
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₇ : x = inl x.fst + inr (x.fst • @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _ • 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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)
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₈ : x = inl x.fst + inr ((x.fst * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) • 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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)
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₉ : x = inl x.fst + inr (HSMul.hSMul.{u_3, u_4, u_4} (α := R) 1 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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)
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₁₀ : x = inl 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₁₁ : x = x
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
R : Type u_3
M : Type u_4
inst : SeminormedRing R
inst_1 : SeminormedAddCommGroup M
x : tsze R M
⊢ norm (E := WithLp 1 (R × M)) (WithLp.toLp 1 x) = ‖x.fst‖ + ‖x.snd‖
have 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‖
Tactic: rw [WithLp.prod_norm_eq_add (by norm_num)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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‖₊
have a : (↑‖x‖₊ : ℝ) = (↑(‖x.fst‖₊ + ‖x.snd‖₊) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₂)‖ ≤ ‖(r₁, m₁)‖ * ‖(r₂, m₂)‖
have simp_rw : ‖((r₁, m₁) * (r₂, m₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
  (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)
Tactic: simp_rw [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)
have h₁ : ‖r₁ * r₂‖ ≤ ‖r₁‖ * ‖r₂‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₂‖
⊢ ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)
have h₂ : ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₁‖
have h₂ : ‖r₁ • m₂‖ ≤ ‖r₁‖ * ‖m₂‖
Tactic: refine norm_add_le_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₂‖
⊢ ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖
have h₃ : ‖MulOpposite.op r₂ • m₁‖ ≤ ‖r₂‖ * ‖m₁‖
Tactic: refine norm_add_le_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖
have h : 0 ≤ ‖m₁‖ * ‖m₂‖
Tactic: apply le_add_of_nonneg_right
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
    (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)
have calc : ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖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