awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
rw :
  LinearMap.range
      (AlgHom.toLinearMap
          ((lift Q :
              (a :
                  { f : M →ₗ[R] A //
                    ∀ (m : M),
                      (f : (a : M) → A) m * (f : (a : M) → A) m =
                        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
                CliffordAlgebra Q →ₐ[R] A)
            (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
              ∀ (m : M),
                HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                  (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
              f cond)) ∘ₗ
        ι Q) =
    f.range
rw₁ rw₂ : f.range = f.range
⊢ Submodule.map
      (AlgHom.toLinearMap
        ((lift Q :
            (a :
                { f : M →ₗ[R] A //
                  ∀ (m : M),
                    (f : (a : M) → A) m * (f : (a : M) → A) m =
                      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
              CliffordAlgebra Q →ₐ[R] A)
          (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
            ∀ (m : M),
              HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
            f cond)))
      (ι Q).range =
    f.range

Tactic:
rw [← LinearMap.range_comp, ι_comp_lift]

Premises used: CliffordAlgebra.ι_comp_lift, LinearMap.range_comp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
⊢ (map f).toLinearMap ∘ₗ ι Q₁ = ι Q₂ ∘ₗ f.toLinearMap

Tactic:
ι_comp_lift _ _

Premises used: CliffordAlgebra.ι_comp_lift, CliffordAlgebra.map
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
m : M₁
⊢ Eq (α := CliffordAlgebra Q₂)
    ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₂)
    ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((f : (a : M₁) → M₂) m) : CliffordAlgebra Q₂)

Tactic:
lift_ι_apply _ _ m

Premises used: CliffordAlgebra.lift_ι_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
a :
  ∀ (m : M₁),
    Eq (α := CliffordAlgebra Q₁)
      (((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m : CliffordAlgebra Q₁)
      ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁)) ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m :
        CliffordAlgebra Q₁)
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ Eq (α := CliffordAlgebra Q₁)
    (((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m : CliffordAlgebra Q₁)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁)) ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m :
      CliffordAlgebra Q₁)

Tactic:
map_apply_ι _ m

Premises used: CliffordAlgebra.map_apply_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ Eq (α := CliffordAlgebra Q₁)
    (((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m : CliffordAlgebra Q₁)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁)) ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m :
      CliffordAlgebra Q₁)

Tactic:
exact map_apply_ι _ m

Premises used: CliffordAlgebra.map_apply_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
a :
  ∀ (m : M₁),
    Eq (α := CliffordAlgebra Q₃)
      ((((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₃) m : CliffordAlgebra Q₃)
      (((map (f.comp g)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₃) m : CliffordAlgebra Q₃)
⊢ (map f).comp (map g) = map (f.comp g)

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
a :
  Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((g : (a : M₁) → M₂) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
a₁ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
a₂ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f.comp g : (a : M₁) → M₃) m) : CliffordAlgebra Q₃)
a₃ a₄ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
⊢ Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((map g : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)

Tactic:
rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]

Premises used: CliffordAlgebra.map_apply_ι, QuadraticMap.Isometry.comp_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
⊢ Submodule.map (map f).toLinearMap (ι Q₁).range = Submodule.map (ι Q₂) f.range

Tactic:
(ι_range_map_lift _ _).trans (LinearMap.range_comp _ _)

Premises used: CliffordAlgebra.ι_range_map_lift, LinearMap.range_comp, CliffordAlgebra.map, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₂) → M₁) (⇑f : (a : M₁) → M₂)
⊢ LeftInverse (α := CliffordAlgebra Q₁) (β := CliffordAlgebra Q₂)
    (⇑(map g) : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁)
    (⇑(map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂)

Tactic:
fun x => ?_

Premises used: Function.LeftInverse
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₂) → M₁) (⇑f : (a : M₁) → M₂)
refine :
  ∀ (x : CliffordAlgebra Q₁),
    (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁)
        ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
      x
⊢ LeftInverse (α := CliffordAlgebra Q₁) (β := CliffordAlgebra Q₂)
    (⇑(map g) : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁)
    (⇑(map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂)

Tactic:
refine fun x => ?_
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₂) → M₁) (⇑f : (a : M₁) → M₂)
x : CliffordAlgebra Q₁
⊢ g.comp f = QuadraticMap.Isometry.id Q₁

Tactic:
replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₂ : (map (QuadraticMap.Isometry.id Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₃ : (AlgHom.id R (CliffordAlgebra Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₄ : id x = x
rw₅ rw₆ : x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x

Tactic:
rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]

Premises used: CliffordAlgebra.map_id, AlgHom.coe_id, AlgHom.comp_apply, CliffordAlgebra.map_comp_map, id_eq
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
r : R
⊢ Eq (α := CliffordAlgebra Q₂)
    ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂)
        ((algebraMap R (CliffordAlgebra Q₁) : (a : R) → CliffordAlgebra Q₁) r) :
      CliffordAlgebra Q₂)
    ((algebraMap R (CliffordAlgebra Q₂) : (a : R) → CliffordAlgebra Q₂) r : CliffordAlgebra Q₂)

Tactic:
simp only [AlgHom.commutes]

Premises used: AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
y : M₂
x : M₁
hx : (f : (a : M₁) → M₂) x = y
⊢ Eq (α := CliffordAlgebra Q₂)
    ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) x) :
      CliffordAlgebra Q₂)
    ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) y : CliffordAlgebra Q₂)

Tactic:
simp only [map_apply_ι, hx]

Premises used: CliffordAlgebra.map_apply_ι
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
x_1 x_2 : CliffordAlgebra Q₂
h : ∃ (a : CliffordAlgebra Q₁), (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) a = x_1
h_1 : ∃ (a : CliffordAlgebra Q₁), (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) a = x_2
x : CliffordAlgebra Q₁
hx : (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x = x_1
y : CliffordAlgebra Q₁
hy : (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) y = x_2
⊢ (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) (x * y) = x_1 * x_2

Tactic:
simp only [map_mul, hx, hy]

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
x_1 x_2 : CliffordAlgebra Q₂
h : ∃ (a : CliffordAlgebra Q₁), (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) a = x_1
h_1 : ∃ (a : CliffordAlgebra Q₁), (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) a = x_2
x : CliffordAlgebra Q₁
hx : (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x = x_1
y : CliffordAlgebra Q₁
hy : (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) y = x_2
⊢ (map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) (x + y) = x_1 + x_2

Tactic:
simp only [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (QuadraticMap.Isometry.id Q₂) = AlgHom.id R (CliffordAlgebra Q₂)

Tactic:
map_id Q₂

Premises used: CliffordAlgebra.map_id
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
h : e.toIsometry.comp e.symm.toIsometry = QuadraticMap.Isometry.id Q₂
⊢ map (e.toIsometry.comp e.symm.toIsometry) = AlgHom.id R (CliffordAlgebra Q₂)

Tactic:
convert! map_id Q₂ using 2

Premises used: CliffordAlgebra.map_id
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
h :
  ∀ (m : M₂),
    Eq (α := M₂) ((e.toIsometry.comp e.symm.toIsometry : (a : M₂) → M₂) m : M₂)
      ((QuadraticMap.Isometry.id Q₂ : (a : M₂) → M₂) m : M₂)
⊢ e.toIsometry.comp e.symm.toIsometry = QuadraticMap.Isometry.id Q₂

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
m : M₂
⊢ Eq (α := M₂) ((e.toIsometry.comp e.symm.toIsometry : (a : M₂) → M₂) m : M₂)
    ((QuadraticMap.Isometry.id Q₂ : (a : M₂) → M₂) m : M₂)

Tactic:
e.toLinearEquiv.apply_symm_apply m

Premises used: LinearEquiv.apply_symm_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
m : M₂
⊢ Eq (α := M₂) ((e.toIsometry.comp e.symm.toIsometry : (a : M₂) → M₂) m : M₂)
    ((QuadraticMap.Isometry.id Q₂ : (a : M₂) → M₂) m : M₂)

Tactic:
exact e.toLinearEquiv.apply_symm_apply m

Premises used: LinearEquiv.apply_symm_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
map_id Q₁

Premises used: CliffordAlgebra.map_id
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
h : e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁
⊢ map (e.symm.toIsometry.comp e.toIsometry) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
convert! map_id Q₁ using 2

Premises used: CliffordAlgebra.map_id
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
h :
  ∀ (m : M₁),
    Eq (α := M₁) ((e.symm.toIsometry.comp e.toIsometry : (a : M₁) → M₁) m : M₁)
      ((QuadraticMap.Isometry.id Q₁ : (a : M₁) → M₁) m : M₁)
⊢ e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
m : M₁
⊢ Eq (α := M₁) ((e.symm.toIsometry.comp e.toIsometry : (a : M₁) → M₁) m : M₁)
    ((QuadraticMap.Isometry.id Q₁ : (a : M₁) → M₁) m : M₁)

Tactic:
e.toLinearEquiv.symm_apply_apply m

Premises used: LinearEquiv.symm_apply_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
m : M₁
⊢ Eq (α := M₁) ((e.symm.toIsometry.comp e.toIsometry : (a : M₁) → M₁) m : M₁)
    ((QuadraticMap.Isometry.id Q₁ : (a : M₁) → M₁) m : M₁)

Tactic:
exact e.toLinearEquiv.symm_apply_apply m

Premises used: LinearEquiv.symm_apply_apply, QuadraticMap.IsometryEquiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ (equivOfIsometry e).symm = equivOfIsometry e.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, QuadraticMap.IsometryEquiv.symm, AlgEquiv.symm, AlgEquiv.ofAlgHom, CliffordAlgebra.equivOfIsometry, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
h :
  ∀ (x : CliffordAlgebra Q₁),
    Eq (α := CliffordAlgebra Q₃)
      (((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x :
        CliffordAlgebra Q₃)
      ((equivOfIsometry (e₁₂.trans e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x : CliffordAlgebra Q₃)
⊢ (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ Eq (α := CliffordAlgebra Q₃)
    (((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x :
      CliffordAlgebra Q₃)
    ((equivOfIsometry (e₁₂.trans e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x : CliffordAlgebra Q₃)

Tactic:
AlgHom.congr_fun (map_comp_map _ _) x

Premises used: QuadraticMap.Isometry.comp, QuadraticMap.IsometryEquiv.toIsometry, AlgHom.congr_fun, CliffordAlgebra.map_comp_map