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 : 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
have neg : (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: refine mt ?_ h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ Eq (α := tsze R M) (exp (inl x)) (inl (exp x))
have 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))
Tactic: rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have 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
Tactic: rw [snd_inl, fst_inl, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₁ : HSMul.hSMul (β := M) (MulOpposite.op x) 0 = HSMul.hSMul (β := M) x 0
Tactic: rw [snd_inl, fst_inl, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₂ : 0 = HSMul.hSMul (β := M) x 0
Tactic: rw [snd_inl, fst_inl, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [snd_inl, fst_inl, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ exp (inr m) = HAdd.hAdd (α := tsze R M) 1 (inr m)
have 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))
Tactic: rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have 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
Tactic: rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have 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
Tactic: rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₂ : HSMul.hSMul.{u_3, u_4, u_4} (α := Rᵐᵒᵖ) 0 m = HSMul.hSMul.{u_3, u_4, u_4} (α := R) 0 m
Tactic: rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₃ : 0 = HSMul.hSMul.{u_3, u_4, u_4} (α := R) 0 m
Tactic: rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ 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))
have hx₄ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
-- 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
⊢ (exp x).fst = exp x.fst
have rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).fst = exp x.fst
Tactic: rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
-- 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
rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).fst = exp x.fst
⊢ (exp x).fst = exp x.fst
have rw₁ : fst.{u_3, u_4} (M := M) (inl (exp x.fst)) + fst (inr (exp x.fst • x.snd)) = exp x.fst
Tactic: rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
-- 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
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
⊢ (exp x).fst = exp x.fst
have rw₂ : exp x.fst + fst (inr (exp x.fst • x.snd)) = exp x.fst
Tactic: rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
-- 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
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
⊢ (exp x).fst = exp x.fst
have rw₃ : exp x.fst + 0 = exp x.fst
Tactic: rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
-- 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
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
⊢ (exp x).fst = exp x.fst
have rw₄ : exp x.fst = exp x.fst
Tactic: rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]
-- 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
⊢ (exp x).snd = exp x.fst • x.snd
have rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).snd = exp x.fst • x.snd
Tactic: rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
-- 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
rw : (inl (exp x.fst) + inr (exp x.fst • x.snd)).snd = exp x.fst • x.snd
⊢ (exp x).snd = exp x.fst • x.snd
have rw₁ : snd (inl (exp x.fst)) + snd.{u_3, u_4} (R := R) (inr (exp x.fst • x.snd)) = exp x.fst • x.snd
Tactic: rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
-- 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
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
⊢ (exp x).snd = exp x.fst • x.snd
have rw₂ : 0 + snd.{u_3, u_4} (R := R) (inr (exp x.fst • x.snd)) = exp x.fst • x.snd
Tactic: rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
-- 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
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
⊢ (exp x).snd = exp x.fst • x.snd
have rw₃ : 0 + exp x.fst • x.snd = exp x.fst • x.snd
Tactic: rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
-- 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
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
⊢ (exp x).snd = exp x.fst • x.snd
have rw₄ : exp x.fst • x.snd = exp x.fst • x.snd
Tactic: rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
-- 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
⊢ 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
    (exp (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)))
⊢ x =
    x.fst •
      exp (HSMul.hSMul (β := tsze R M) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x.fst _) (inr x.snd))
have rw₁ : x = x.fst • HAdd.hAdd (α := tsze R M) 1 (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))
⊢ 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 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]