awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw :
  ∀ (x : ExteriorAlgebra R M),
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      x
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    ⊤

Tactic:
rw [Submodule.eq_top_iff']

Premises used: Submodule.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    0

Tactic:
Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m m' : ExteriorAlgebra R M
hm :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    m
hm' :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    m'
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (m + m')

Tactic:
Submodule.add_mem _ hm hm'

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m m' : ExteriorAlgebra R M
hm :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    m
hm' :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    m'
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (m + m')

Tactic:
exact Submodule.add_mem _ hm hm'

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm : ↥(⋀[R]^i M)
homogeneous :
  ∀ (m : ExteriorAlgebra R M) (hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m),
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) m hm) :
        ExteriorAlgebra R M)
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑hm : ExteriorAlgebra R M)

Tactic:
let ⟨m, hm⟩ := hm
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
homogeneous :
  (↑(⋀[R]^i M) : Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) m hm) :
      ExteriorAlgebra R M)

Tactic:
apply Set.mem_of_mem_of_subset hm

Premises used: Set.mem_of_mem_of_subset
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
homogeneous :
  (↑(Submodule.span R (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M))) :
      Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))
⊢ (↑(⋀[R]^i M) : Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))

Tactic:
rw [← ιMulti_span_fixedDegree]

Premises used: ExteriorAlgebra.ιMulti_span_fixedDegree
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
⊢ (↑(Submodule.span R (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M))) :
      Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))

Tactic:
Submodule.span_mono fun _ hx ↦ ?_

Premises used: Set.Mem, Set.Subset, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
homogeneous :
  ∀ (x : ExteriorAlgebra R M)
    (hx :
      Membership.mem (γ := Set (ExteriorAlgebra R M))
        (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M)) x),
    Membership.mem (γ := Set (ExteriorAlgebra R M))
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
      x
⊢ (↑(Submodule.span R (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M))) :
      Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))

Tactic:
refine Submodule.span_mono fun _ hx ↦ ?_

Premises used: Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
x : ExteriorAlgebra R M
hx :
  Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M)) x
homogeneous :
  ∀ (y : Fin i → M),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
      ((ιMulti R i : (a : Fin i → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
⊢ Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    x

Tactic:
obtain ⟨y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
y : Fin i → M
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    ((ιMulti R i : (a : Fin i → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)

Tactic:
⟨⟨_, y⟩, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Sigma.mk, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
y : Fin i → M
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    ((ιMulti R i : (a : Fin i → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)

Tactic:
exact ⟨⟨_, y⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : ExteriorAlgebra R M
zero :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    0
add :
  ∀ (m m' : ExteriorAlgebra R M)
    (hm :
      Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
        (Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
        m)
    (hm' :
      Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
        (Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
        m'),
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      (m + m')
homogeneous :
  ∀ {i : ℕ} (hm : ↥(⋀[R]^i M)),
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      (↑hm : ExteriorAlgebra R M)
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    x

Tactic:
induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
  | zero => exact Submodule.zero_mem _
  | add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
  | homogeneous hm =>
    let ⟨m, hm⟩ := hm
    apply Set.mem_of_mem_of_subset hm
    rw [← ιMulti_span_fixedDegree]
    refine Submodule.span_mono fun _ hx ↦ ?_
    obtain ⟨y, rfl⟩ := hx
    exact ⟨⟨_, y⟩, rfl⟩

Premises used: ExteriorAlgebra.ιMulti_span_fixedDegree, Submodule.zero_mem, Submodule.span_mono, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
ι : Type u_5
⊢ Module R (M [⋀^ι]→ₗ[R] N)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
refine LinearMap.compr₂ this ?_

Premises used: LinearMap.compr₂
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine : M [⋀^Fin 0]→ₗ[R] N ≃ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] N

Tactic:
refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)

Premises used: LinearMap.proj, LinearMap.comp, LinearEquiv.toLinearMap, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ M [⋀^Fin 0]→ₗ[R] N ≃ₗ[R] N

Tactic:
exact AlternatingMap.constLinearEquivOfIsEmpty.symm

Premises used: LinearEquiv.symm, AlternatingMap.constLinearEquivOfIsEmpty
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
M₁ : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
suffices
    (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R]
      ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N by
    refine LinearMap.compr₂ this ?_
    refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
    exact AlternatingMap.constLinearEquivOfIsEmpty.symm
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
refine_1 : M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_2 :
  ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (((LinearMap.mk₂ R
                  (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                    (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                  ⋯ ⋯ ⋯ ⋯ :
                (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              m :
            ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
          (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((((LinearMap.mk₂ R
                      (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                        (AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                      ⋯ ⋯ ⋯ ⋯ :
                    (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  m :
                ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
              (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
            x :
          (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) =
      HSMul.hSMul (α := R) ((0 : (a : M) → R) m : R) x
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

Tactic:
refine CliffordAlgebra.foldl _ ?_ ?_

Premises used: CliffordAlgebra.foldl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
refine_1 :
  ∀ (m₁ m₂ : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (m₁ + m₂) f =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₁ f)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₂ f)
refine_1₁ :
  ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (c • m) f =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
refine_1₂ :
  ∀ (m : M) (f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m (f₁ + f₂) =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₁)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f₂)
refine_1₃ :
  ∀ (c : R) (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m (c • f) =
      HSMul.hSMul (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) c
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m f)
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

Tactic:
refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_

Premises used: LinearMap.mk₂
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
m₁ m₂ : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
refine_1 :
  ∀ (i : ℕ),
    (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        (m₁ + m₂) f i =
      HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (β := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₁ f)
        ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
            ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
          m₂ f)
        i
⊢ (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
        ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
      (m₁ + m₂) f =
    HAdd.hAdd (α := (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₁ f)
      ((fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
          ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m : M [⋀^Fin i]→ₗ[R] N))
        m₂ f)

Tactic:
ext i : 1