awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
have H : ∀ (r : R),
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) sorry :
          ↥(even Q)) :
      A)
    ((g : (a : ↥(even Q)) → A)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) sorry :
          ↥(even Q)) :
      A)
Tactic: induction x, hx using even_induction with
  | algebraMap r =>
    exact (f.commutes r).trans (g.commutes r).symm
  | add x y hx hy ihx ihy =>
    have := congr_arg₂ (· + ·) ihx ihy
    exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)
  | ι_mul_ι_mul m₁ m₂ x hx ih =>
    have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
    exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
H :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
            ↥(even Q)) :
        A)
      ((g : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
            ↥(even Q)) :
        A)
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
have H₁ : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0)
  (ihx :
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A))
  (ihy :
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)),
  Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) sorry) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) sorry) : A)
Tactic: induction x, hx using even_induction with
  | algebraMap r =>
    exact (f.commutes r).trans (g.commutes r).symm
  | add x y hx hy ihx ihy =>
    have := congr_arg₂ (· + ·) ihx ihy
    exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)
  | ι_mul_ι_mul m₁ m₂ x hx ih =>
    have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
    exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (m₁ + m₂) : A) a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
have rw : HAdd.hAdd (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A)
      ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) *
    a.1 =
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
Tactic: rw [map_add, add_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
rw :
  HAdd.hAdd (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A)
        ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) *
      a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (m₁ + m₂) : A) a.1 =
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
      HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
have rw₁ : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1 =
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₁ : A) a.1 +
    HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m₂ : A) a.1
Tactic: rw [map_add, add_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : EvenHom Q A
c : R
m : M
a : A × ↥(S f)
m₃ : M
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (c • m) : A) a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
have rw : HSMul.hSMul (β := A) c ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) * a.1 =
  c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
Tactic: rw [map_smul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : EvenHom Q A
c : R
m : M
a : A × ↥(S f)
m₃ : M
rw :
  HSMul.hSMul (β := A) c ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) * a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) (c • m) : A) a.1 =
    c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
have rw₁ : c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1 =
  c • HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₃ : M →ₗ[R] A) : (a : M) → A) m : A) a.1
Tactic: rw [map_smul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
x : A × ↥(S f)
⊢ (((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
      ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
          (a : A × ↥(S f)) → A × ↥(S f))
        x) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) x
have obtain : ∀ (a : A) (g : M →ₗ[R] A) (hg : g ∈ S f),
  (((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
      ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
          (a : A × ↥(S f)) → A × ↥(S f))
        (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)
Tactic: obtain ⟨a, ⟨g, hg⟩⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
      ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
          (a : A × ↥(S f)) → A × ↥(S f))
        (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)
have fst : ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
      ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
          (a : A × ↥(S f)) → A × ↥(S f))
        (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).1 =
  (HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).1
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
fst :
  ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
        ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
            (a : A × ↥(S f)) → A × ↥(S f))
          (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).1 =
    (HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).1
⊢ (((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
      ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
          (a : A × ↥(S f)) → A × ↥(S f))
        (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)
have snd : (↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
          ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
              (a : A × ↥(S f)) → A × ↥(S f))
            (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
    M →ₗ[R] A) =
  (↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
    M →ₗ[R] A)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) : (a : A × ↥(S f)) → A × ↥(S f))
        ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
            (a : A × ↥(S f)) → A × ↥(S f))
          (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).1 =
    (HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).1
have fst : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) a
Tactic: change f.bilin m m * a = Q m • a
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) a
have fst : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a
Tactic: rw [Algebra.smul_def, f.contract]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
fst :
  HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a
⊢ HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m : A) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) a
have fst₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a =
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) : A) a
Tactic: rw [Algebra.smul_def, f.contract]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
              (a : A × ↥(S f)) → A × ↥(S f))
            ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                (a : A × ↥(S f)) → A × ↥(S f))
              (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
      M →ₗ[R] A) =
    (↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
      M →ₗ[R] A)
have snd : ∀ (m₁ : M),
  Eq.{u_3 + 1} (α := A)
    (((↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                    (a : A × ↥(S f)) → A × ↥(S f))
                  ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                      (a : A × ↥(S f)) → A × ↥(S f))
                    (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)
    (((↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)
Tactic: ext m₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ Eq.{u_3 + 1} (α := A)
    (((↑((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                    (a : A × ↥(S f)) → A × ↥(S f))
                  ((((fFold f : (a : M) → A × ↥(S f) →ₗ[R] A × ↥(S f)) m : A × ↥(S f) →ₗ[R] A × ↥(S f)) :
                      (a : A × ↥(S f)) → A × ↥(S f))
                    (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg))).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)
    (((↑(HSMul.hSMul (α := R) ((Q : (a : M) → R) m : R) (a, Subtype.mk (p := fun (x : M →ₗ[R] A) ↦ x ∈ S f) g hg)).2 :
            M →ₗ[R] A) :
          (a : M) → A)
        m₁ :
      A)
have snd : HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
    ((g : (a : M) → A) m : A) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
Tactic: change f.bilin _ _ * g m = Q m • g m₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
have snd : ∀ (x : M →ₗ[R] A)
  (h :
    Membership.mem (γ := Set (M →ₗ[R] A))
      {f' : M →ₗ[R] A |
        ∃ (x : A) (m₂ : M),
          f' =
            (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
              (LinearMap.mulRight R x)}
      x),
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((x : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
snd :
  ∀ (x : M →ₗ[R] A)
    (h :
      Membership.mem (γ := Set (M →ₗ[R] A))
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)}
        x),
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
have snd₁ : HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
    ((0 : (a : M) → A) m : A) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((0 : (a : M) → A) m₁ : A)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
snd :
  ∀ (x : M →ₗ[R] A)
    (h :
      Membership.mem (γ := Set (M →ₗ[R] A))
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)}
        x),
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
snd₁ :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((0 : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((0 : (a : M) → A) m₁ : A)
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
have snd₂ : ∀ (x y : M →ₗ[R] A)
  (hx :
    Membership.mem (γ := Submodule R (M →ₗ[R] A))
      (Submodule.span R
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)})
      x)
  (hy :
    Membership.mem (γ := Submodule R (M →ₗ[R] A))
      (Submodule.span R
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)})
      y),
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A) →
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
          ((y : (a : M) → A) m : A) =
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (a : M) → A) m₁ : A) →
      HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
          ((x + y : (a : M) → A) m : A) =
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
b : A
m₃ : M
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((((LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₃) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R b) :
              M →ₗ[R] A) :
            (a : M) → A)
          m :
        A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R)
      ((((LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₃) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R b) :
              M →ₗ[R] A) :
            (a : M) → A)
          m₁ :
        A)
have snd : HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
    (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m : M →ₗ[R] A) : (a : M) → A) m₃ : A) b) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R)
    (HMul.hMul (α := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m₃ : A) b)
Tactic: change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)