awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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 : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
a b : CliffordAlgebra Q
rw :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
      N)
    ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        (a * b) :
      N)
    ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
              ((((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                  (a : CliffordAlgebra Q) → N)
                a) :
            CliffordAlgebra Q →ₗ[R] N) :
          (a : CliffordAlgebra Q) → N)
        b :
      N)
have rw₂ : Eq.{u_3 + 1} (α := N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) : CliffordAlgebra Q) :
    N)
  ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N)
            ((((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) :
                (a : CliffordAlgebra Q) → N)
              ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)) :
          CliffordAlgebra Q →ₗ[R] N) :
        (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q) :
    N)
Tactic: rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
l : List M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
have rw : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
  List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
Tactic: rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
l : List M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
have rw₁ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
  List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
Tactic: rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
l : List M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
have rw₂ : (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
    (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l.reverse)) =
  List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
Tactic: rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
l : List M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₂ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l.reverse)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
have rw₃ : List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n l.reverse =
  List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
Tactic: rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
l : List M
f : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N →ₗ[R] N)
hf :
  ∀ (m : M) (x : N),
    (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N)
        ((((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) x : N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) x
n : N
rw :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₁ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l))) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₂ :
  (((foldr Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l.reverse)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
rw₃ :
  List.foldr (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] N) m : N →ₗ[R] N) : (a : N) → N) n) n l.reverse =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
⊢ (((foldl Q f hf : (a : N) → CliffordAlgebra Q →ₗ[R] N) n : CliffordAlgebra Q →ₗ[R] N) : (a : CliffordAlgebra Q) → N)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) l)) =
    List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
have rw₄ : List.foldl (fun (x : N) (y : M) ↦ (((f : (a : M) → N →ₗ[R] N) y : N →ₗ[R] N) : (a : N) → N) x) n l =
  List.foldl (fun (m : N) (n : M) ↦ (((f : (a : M) → N →ₗ[R] N) n : N →ₗ[R] N) : (a : N) → N) m) n l
Tactic: rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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 x
have have : ∀ (this : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) ⊤ x), P x
Tactic: have : x ∈ ⊤ := Submodule.mem_top (R := R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (hypothesis)
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)) ⊤ x
⊢ P x
have this₁ : Membership.mem (γ := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) x
Tactic: rw [← iSup_ι_range_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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
⊢ P (x * m)
have mem : ∀ (m : M), P (HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
Tactic: obtain ⟨m, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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)
⊢ P x
have mem₁ : ∀ (_x _y : CliffordAlgebra Q) (_i : ℕ),
  _x ∈ (ι Q).range ^ _i → _y ∈ (ι Q).range ^ _i → ∀ (ihx : P _x) (ihy : P _y), P (_x + _y)
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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)
⊢ P x
have mem₂ : ∀ (_i : ℕ) (x : CliffordAlgebra Q) (_hx : x ∈ (ι Q).range ^ _i) (px : P x) (m : CliffordAlgebra Q)
  (hm : m ∈ (ι Q).range), P (x * m)
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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
⊢ P x
have mem : ∀ (i : ℕ) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ i), 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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
⊢ P x
have zero : P 0
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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
⊢ P x
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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
have refine : ∀ (x : CliffordAlgebra Q), P ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
Tactic: refine reverse_involutive.surjective.forall.2 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (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
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 ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x)
have algebraMap₁ : ∀ (r : R),
  P
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r))
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
Cleared hypotheses: x