awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
have h₁ : ∀ (x : M),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q)
h₁ :
  ∀ (x : M),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
        CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
have h₂ : ∀ (a b : CliffordAlgebra Q)
  (ha :
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q))
  (hb :
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
        CliffordAlgebra Q)),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
      CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range
have rw : Submodule.map (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range
Tactic: rw [← submodule_map_involute_eq_comap, ι_range_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
rw : Submodule.map (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range
⊢ Submodule.comap (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range
have rw₁ : (ι Q).range = (ι Q).range
Tactic: rw [← submodule_map_involute_eq_comap, ι_range_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
have simp_rw : Eq (α := Submodule R (CliffordAlgebra Q))
  (Submodule.map (AlgHom.toLinearMap involute) (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map (AlgHom.toLinearMap involute) (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
have simp_rw₁ : Eq (α := Submodule R (CliffordAlgebra Q))
  (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map (AlgHom.toLinearMap involute) ((ι Q).range ^ (↑i : ℕ)))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map (AlgHom.toLinearMap involute) (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₁ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map (AlgHom.toLinearMap involute) ((ι Q).range ^ (↑i : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
have simp_rw₂ : Eq (α := Submodule R (CliffordAlgebra Q))
  (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map (AlgHom.toLinearMap involute) (ι Q).range ^ (↑i : ℕ))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
have rw : Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
Tactic: rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
rw : Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
⊢ Submodule.comap (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
have rw₁ : evenOdd Q n = evenOdd Q n
Tactic: rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Submodule.map reverse (ι Q).range = (ι Q).range
have rw : Submodule.map
    ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
      (↑(MulOpposite.opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ))
    (ι Q).range =
  (ι Q).range
Tactic: rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp,
    ← Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap reverse (ι Q).range = (ι Q).range
have rw : Submodule.map reverse (ι Q).range = (ι Q).range
Tactic: rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
rw : Submodule.map reverse (ι Q).range = (ι Q).range
⊢ Submodule.comap reverse (ι Q).range = (ι Q).range
have rw₁ : (ι Q).range = (ι Q).range
Tactic: rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
have simp_rw : Submodule.map
    ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
      AlgHom.toLinearMap reverseOp)
    (p * q) =
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      q *
    Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      p
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p * q) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        q *
      Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
have simp_rw₁ : Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
    (Submodule.map (AlgHom.toLinearMap reverseOp) (p * q)) =
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) q) *
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p)
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p * q) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        q *
      Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p
simp_rw₁ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) (p * q)) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) q) *
      Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
have simp_rw₂ : Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
    (Submodule.map (AlgHom.toLinearMap reverseOp) p * Submodule.map (AlgHom.toLinearMap reverseOp) q) =
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) q) *
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p)
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p
have simp_rw : Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
Tactic: simp_rw [← submodule_map_reverse_eq_comap, submodule_map_mul_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
have simp_rw : Submodule.map
    ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
      AlgHom.toLinearMap reverseOp)
    (p ^ n) =
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      p ^
    n
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p ^ n) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p ^
      n
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
have simp_rw₁ : Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
    (Submodule.map (AlgHom.toLinearMap reverseOp) (p ^ n)) =
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p) ^
    n
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p ^ n) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p ^
      n
simp_rw₁ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) (p ^ n)) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p) ^
      n
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
have simp_rw₂ : Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
    (Submodule.map (AlgHom.toLinearMap reverseOp) p ^ n) =
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p) ^
    n
Tactic: simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n
have simp_rw : Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
Tactic: simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n
have simp_rw : Eq (α := Submodule R (CliffordAlgebra Q))
  (Submodule.map reverse (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map reverse (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n
have simp_rw₁ : Eq (α := Submodule R (CliffordAlgebra Q))
  (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map reverse ((ι Q).range ^ (↑i : ℕ)))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map reverse (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₁ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map reverse ((ι Q).range ^ (↑i : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n
have simp_rw₂ : Eq (α := Submodule R (CliffordAlgebra Q))
  (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map reverse (ι Q).range ^ (↑i : ℕ))
  (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
Tactic: simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n
have rw : Submodule.map reverse (evenOdd Q n) = evenOdd Q n
Tactic: rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
n : ZMod 2
rw : Submodule.map reverse (evenOdd Q n) = evenOdd Q n
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n
have rw₁ : evenOdd Q n = evenOdd Q n
Tactic: rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add : HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  x + y
Tactic: rw [map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
have add₁ : HAdd.hAdd (β := CliffordAlgebra Q) x ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
  x + y
Tactic: rw [map_add, ihx, ihy]