awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)

Tactic:
algebraMap r
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)

Tactic:
exact algebraMap r
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x _x _y : CliffordAlgebra Q
_i : ℕ
hx : _x ∈ (ι Q).range ^ _i
hy : _y ∈ (ι Q).range ^ _i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)

Tactic:
add _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x _x _y : CliffordAlgebra Q
_i : ℕ
hx : _x ∈ (ι Q).range ^ _i
hy : _y ∈ (ι Q).range ^ _i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)

Tactic:
exact add _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x_2 : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
mem : ∀ (m : M), P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
⊢ P (x * m)

Tactic:
obtain ⟨m, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x_2 : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : M
⊢ P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))

Tactic:
mul_ι _ _ px
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x_2 : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : M
⊢ P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))

Tactic:
exact mul_ι _ _ px
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x_1 : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
mem : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
mem₁ :
  ∀ (_x _y : CliffordAlgebra Q) (_i : ℕ),
    _x ∈ (ι Q).range ^ _i → _y ∈ (ι Q).range ^ _i → ∀ (ihx : P _x) (ihy : P _y), P (_x + _y)
mem₂ :
  ∀ (_i : ℕ) (x : CliffordAlgebra Q) (_hx : x ∈ (ι Q).range ^ _i) (px : P x) (m : CliffordAlgebra Q)
    (hm : m ∈ (ι Q).range), P (x * m)
⊢ P x

Tactic:
induction hx using Submodule.pow_induction_on_right' with
    | algebraMap r => exact algebraMap r
    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
    | mul_mem _i x _hx px m hm =>
      obtain ⟨m, rfl⟩ := hm
      exact mul_ι _ _ px

Premises used: rfl, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x : CliffordAlgebra Q
⊢ P 0

Tactic:
simpa only [map_zero] using algebraMap 0

Premises used: map_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x _x _y : CliffordAlgebra Q
hx : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _x
hy : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _y
ihx : P _x
ihy : P _y
⊢ P (_x + _y)

Tactic:
add _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x _x _y : CliffordAlgebra Q
hx : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _x
hy : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _y
ihx : P _x
ihy : P _y
⊢ P (_x + _y)

Tactic:
exact add _ _ ihx ihy
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q),
    P x → P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
x : CliffordAlgebra Q
this : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) x
mem : ∀ (i : ℕ) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ i), P x
zero : P 0
add₁ :
  ∀ (_x _y : CliffordAlgebra Q),
    Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _x →
      Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) _y →
        ∀ (ihx : P _x) (ihy : P _y), P (_x + _y)
⊢ P x

Tactic:
induction this using Submodule.iSup_induction' with
  | mem i x hx =>
    induction hx using Submodule.pow_induction_on_right' with
    | algebraMap r => exact algebraMap r
    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
    | mul_mem _i x _hx px m hm =>
      obtain ⟨m, rfl⟩ := hm
      exact mul_ι _ _ px
  | zero => simpa only [map_zero] using algebraMap 0
  | add _x _y _ _ ihx ihy =>
    exact add _ _ ihx ihy

Premises used: map_zero, OfNat.ofNat, rfl, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
⊢ ∀ (x : CliffordAlgebra Q), P x

Tactic:
reverse_involutive.surjective.forall.2 ?_

Premises used: Iff.mpr, Function.Surjective.forall, Function.Involutive.surjective, CliffordAlgebra.reverse_involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
refine : ∀ (x : CliffordAlgebra Q), P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
⊢ ∀ (x : CliffordAlgebra Q), P x

Tactic:
refine reverse_involutive.surjective.forall.2 ?_

Premises used: Iff.mpr, Function.Surjective.forall, Function.Involutive.surjective, CliffordAlgebra.reverse_involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
r : R
⊢ P
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))

Tactic:
simpa only [reverse.commutes] using algebraMap r

Premises used: CliffordAlgebra.reverse.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
x y : CliffordAlgebra Q
hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
hy : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y)
⊢ P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y))

Tactic:
simpa only [map_add] using add _ _ hx hy

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
m : M
x : CliffordAlgebra Q
hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
⊢ P
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)))

Tactic:
simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx

Premises used: CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul :
  ∀ (x : CliffordAlgebra Q) (m : M),
    P x → P (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
x : CliffordAlgebra Q
algebraMap₁ :
  ∀ (r : R),
    P
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))
add₁ :
  ∀ (x y : CliffordAlgebra Q) (hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x))
    (hy : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y)),
    P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y))
mul_ι :
  ∀ (m : M) (x : CliffordAlgebra Q) (hx : P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)),
    P
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)))
⊢ P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)

Tactic:
induction x using CliffordAlgebra.right_induction with
  | algebraMap r => simpa only [reverse.commutes] using algebraMap r
  | add _ _ hx hy => simpa only [map_add] using add _ _ hx hy
  | mul_ι _ _ hx => simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx

Premises used: map_add, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.reverse.commutes, CliffordAlgebra.reverse_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
have : (v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)) → M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
have : (l : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q) → M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
have l := v_mul.compl₂ (LinearMap.fst _ _ N)
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
l : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
exact
    { toFun := fun m => (l m).prod (f m)
      map_add' := fun v₂ v₂ =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
      map_smul' := fun c v =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x)
            (LinearMap.congr_fun (f.map_smul _ _) x) }
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
m : M
x_fx : CliffordAlgebra Q × N
⊢ Eq (α := CliffordAlgebra Q × N)
    ((((foldr'Aux Q f : (a : M) → Module.End R (CliffordAlgebra Q × N)) m : Module.End R (CliffordAlgebra Q × N)) :
          (a : CliffordAlgebra Q × N) → CliffordAlgebra Q × N)
        x_fx :
      CliffordAlgebra Q × N)
    ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x_fx.1,
        (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
            (a : CliffordAlgebra Q × N) → N)
          x_fx) :
      CliffordAlgebra Q × N)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
v : M
x_fx : CliffordAlgebra Q × N
simp :
  (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1),
      (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x_fx.1,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) v : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              x_fx) :
          CliffordAlgebra Q × N)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx
⊢ (((foldr'Aux Q f : (a : M) → Module.End R (CliffordAlgebra Q × N)) v : Module.End R (CliffordAlgebra Q × N)) :
        (a : CliffordAlgebra Q × N) → CliffordAlgebra Q × N)
      ((((foldr'Aux Q f : (a : M) → Module.End R (CliffordAlgebra Q × N)) v : Module.End R (CliffordAlgebra Q × N)) :
          (a : CliffordAlgebra Q × N) → CliffordAlgebra Q × N)
        x_fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) x_fx

Tactic:
simp only [foldr'Aux_apply_apply]

Premises used: CliffordAlgebra.foldr'Aux_apply_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
r : R
⊢ (foldr' Q f hf n : (a : CliffordAlgebra Q) → N)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    r • n

Tactic:
congr_arg Prod.snd (foldr_algebraMap _ _ _ _ _)

Premises used: congr_arg, CliffordAlgebra.foldr_algebraMap, Prod.snd
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
⊢ Eq.{u_3 + 1} (α := N)
    ((foldr' Q f hf n : (a : CliffordAlgebra Q) → N) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) : N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        (1, n) :
      N)

Tactic:
congr_arg Prod.snd (foldr_ι _ _ _ _ _)

Premises used: CliffordAlgebra.foldr_ι, congr_arg, Prod.snd