Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘ Ctrl+โ†“ to navigate, Ctrl+๐Ÿ–ฑ๏ธ to focus. On Mac, use โŒ˜ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import DuperXp
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring

open QuadraticForm BilinForm ExteriorAlgebra FiniteDimensional

open Function
open BigOperators
open FiniteDimensional

universe uฮบ uR uM uฮน

variable {
ฮบ: Type uฮบ
ฮบ : 
Type uฮบ: Type (uฮบ + 1)
Type uฮบ}
variable {
R: Type uR
R : 
Type uR: Type (uR + 1)
Type uR} [
CommRing: Type uR โ†’ Type uR
CommRing 
R: Type uR
R] [
Invertible: {ฮฑ : Type uR} โ†’ [inst : Mul ฮฑ] โ†’ [inst : One ฮฑ] โ†’ ฮฑ โ†’ Type uR
Invertible (
2: R
2 : 
R: Type uR
R)] [
Nontrivial: Type uR โ†’ Prop
Nontrivial 
R: Type uR
R]
variable {
M: Type uM
M : 
Type uM: Type (uM + 1)
Type uM} [
AddCommGroup: Type uM โ†’ Type uM
AddCommGroup 
M: Type uM
M] [
Module: (R : Type uR) โ†’ (M : Type uM) โ†’ [inst : Semiring R] โ†’ [inst : AddCommMonoid M] โ†’ Type (max uR uM)
Module 
R: Type uR
R 
M: Type uM
M]
-- variable {B : BilinForm R M}
variable (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type uR) โ†’
  (M : Type uM) โ†’ [inst : CommSemiring R] โ†’ [inst_1 : AddCommMonoid M] โ†’ [inst : Module R M] โ†’ Type (max uR uM)
QuadraticForm 
R: Type uR
R 
M: Type uM
M) {
Cl: CliffordAlgebra Q
Cl : 
CliffordAlgebra: {R : Type uR} โ†’
  [inst : CommRing R] โ†’
    {M : Type uM} โ†’ [inst_1 : AddCommGroup M] โ†’ [inst_2 : Module R M] โ†’ QuadraticForm R M โ†’ Type (max uM uR)
CliffordAlgebra 
Q: QuadraticForm R M
Q} {
Ex: ExteriorAlgebra R M
Ex : 
ExteriorAlgebra: (R : Type uR) โ†’ [inst : CommRing R] โ†’ (M : Type uM) โ†’ [inst_1 : AddCommGroup M] โ†’ [inst : Module R M] โ†’ Type (max uM uR)
ExteriorAlgebra 
R: Type uR
R 
M: Type uM
M}
variable [
Module.Finite: (R : Type uR) โ†’ (M : Type uM) โ†’ [inst : Semiring R] โ†’ [inst_1 : AddCommMonoid M] โ†’ [inst : Module R M] โ†’ Prop
Module.Finite 
R: Type uR
R 
M: Type uM
M] [
Module.Free: (R : Type uR) โ†’ (M : Type uM) โ†’ [inst : Semiring R] โ†’ [inst_1 : AddCommMonoid M] โ†’ [inst : Module R M] โ†’ Prop
Module.Free 
R: Type uR
R 
M: Type uM
M]

set_option trace.duper.printProof true
set_option trace.duper.proofReconstruction true


example: โˆ€ {R : Type uR} [inst : CommRing R] [inst_1 : Invertible 2] {M : Type uM} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (Q : QuadraticForm R M), finrank R (CliffordAlgebra Q) = finrank R (ExteriorAlgebra R M)
example : 
finrank: (R : Type uR) โ†’ (M : Type (max uM uR)) โ†’ [inst : Semiring R] โ†’ [inst_1 : AddCommGroup M] โ†’ [inst : Module R M] โ†’ โ„•
finrank 
R: Type uR
R (
CliffordAlgebra: {R : Type uR} โ†’
  [inst : CommRing R] โ†’
    {M : Type uM} โ†’ [inst_1 : AddCommGroup M] โ†’ [inst_2 : Module R M] โ†’ QuadraticForm R M โ†’ Type (max uM uR)
CliffordAlgebra 
Q: QuadraticForm R M
Q) = 
finrank: (R : Type uR) โ†’ (M : Type (max uM uR)) โ†’ [inst : Semiring R] โ†’ [inst_1 : AddCommGroup M] โ†’ [inst : Module R M] โ†’ โ„•
finrank 
R: Type uR
R (
ExteriorAlgebra: (R : Type uR) โ†’ [inst : CommRing R] โ†’ (M : Type uM) โ†’ [inst_1 : AddCommGroup M] โ†’ [inst : Module R M] โ†’ Type (max uM uR)
ExteriorAlgebra 
R: Type uR
R 
M: Type uM
M) := 
Goals accomplished! ๐Ÿ™

  
Goals accomplished! ๐Ÿ™


-- count_heartbeats in -- never ends

/-
(deterministic) timeout at `match`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information
-/
-- example : finrank R (CliffordAlgebra Q) = finrank R (ExteriorAlgebra R M) := by
--   duper [LinearEquiv.finrank_eq, CliffordAlgebra.equivExterior]
--   done

-- example : finrank R (CliffordAlgebra Q) = finrank R (ExteriorAlgebra R M) := by
--   let clause_1_0 := eq_true ยซ_exHyp_uniq.139473ยป;
--   let clause_3_0 := eq_true ยซ_exHyp_uniq.139477ยป;
--   let clause_5_0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause_1_0;
--   let clause_6_0 := (fun h => of_eq_true h) (clause_5_0 ยซ_exHyp_uniq.139432ยป);
--   let clause_7_0 := (fun h => Duper.clausify_not h) clause_3_0;
--   let clause_8_0 := (fun h => Duper.not_of_eq_false h) clause_7_0;
--   let clause_9_0 := (fun heq => (fun h => Eq.mp (congrArg (fun x => x โ‰  e!_2) heq) h) clause_8_0) clause_6_0;
--   exact (fun h => (h rfl).elim) clause_9_0
--   done