[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
⊢ Homotopic (const X y) (const X y)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : Nullhomotopic f
g : C(Y, Z)
⊢ Nullhomotopic (comp g f)
[PROOFSTEP]
cases' hf with y hy
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : Homotopic f (const X y)
⊢ Nullhomotopic (comp g f)
[PROOFSTEP]
use g y
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : Homotopic f (const X y)
⊢ Homotopic (comp g f) (const X (↑g y))
[PROOFSTEP]
exact Homotopic.hcomp hy (Homotopic.refl g)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : Nullhomotopic f
g : C(X, Y)
⊢ Nullhomotopic (comp f g)
[PROOFSTEP]
cases' hf with y hy
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : Homotopic f (const Y y)
⊢ Nullhomotopic (comp f g)
[PROOFSTEP]
use y
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : Homotopic f (const Y y)
⊢ Homotopic (comp f g) (const X y)
[PROOFSTEP]
exact Homotopic.hcomp (Homotopic.refl g) hy
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
⊢ Nullhomotopic (ContinuousMap.id X)
[PROOFSTEP]
obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X
[GOAL]
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Nullhomotopic (ContinuousMap.id X)
[PROOFSTEP]
use hv.invFun ()
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Homotopic (ContinuousMap.id X) (const X (↑hv.invFun ()))
[PROOFSTEP]
convert hv.left_inv.symm
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
constructor
[GOAL]
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
intro
[GOAL]
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
apply id_nullhomotopic
[GOAL]
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
[PROOFSTEP]
rintro ⟨p, h⟩
[GOAL]
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y
[PROOFSTEP]
refine
  {
    hequiv_unit' :=
      ⟨{  toFun := ContinuousMap.const _ ()
          invFun := ContinuousMap.const _ p
          left_inv := ?_
          right_inv := ?_ }⟩ }
[GOAL]
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
[PROOFSTEP]
exact h.symm
[GOAL]
case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
[PROOFSTEP]
convert Homotopic.refl (ContinuousMap.id Unit)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
⊢ PathConnectedSpace X
[PROOFSTEP]
obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
⊢ PathConnectedSpace X
[PROOFSTEP]
have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ PathConnectedSpace X
[PROOFSTEP]
rw [pathConnectedSpace_iff_eq]
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ
[PROOFSTEP]
use p
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ
[PROOFSTEP]
ext
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
x✝ : X
⊢ x✝ ∈ pathComponent p ↔ x✝ ∈ Set.univ
[PROOFSTEP]
tauto


[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ Homotopic (comp (toContinuousMap (Homeomorph.symm h)) (toContinuousMap h)) (ContinuousMap.id X)
[PROOFSTEP]
rw [symm_comp_toContinuousMap]
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ Homotopic (comp (toContinuousMap h) (toContinuousMap (Homeomorph.symm h))) (ContinuousMap.id Y)
[PROOFSTEP]
rw [toContinuousMap_comp_symm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₁.invFun h₂.invFun) (comp h₂.toFun h₁.toFun)) (ContinuousMap.id X)
[PROOFSTEP]
refine Homotopic.trans ?_ h₁.left_inv
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₁.invFun h₂.invFun) (comp h₂.toFun h₁.toFun)) (comp h₁.invFun h₁.toFun)
[PROOFSTEP]
exact ((Homotopic.refl _).hcomp h₂.left_inv).hcomp (Homotopic.refl _)
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₂.toFun h₁.toFun) (comp h₁.invFun h₂.invFun)) (ContinuousMap.id Z)
[PROOFSTEP]
refine Homotopic.trans ?_ h₂.right_inv
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₂.toFun h₁.toFun) (comp h₁.invFun h₂.invFun)) (comp h₂.toFun h₂.invFun)
[PROOFSTEP]
exact ((Homotopic.refl _).hcomp h₁.right_inv).hcomp (Homotopic.refl _)


[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx
[PROOFSTEP]
simp only [contractLeftAux_apply_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ ↑d v • (↑(ι Q) v * x) - ↑(ι Q) v * (↑d v • x - ↑(ι Q) v * fx) = ↑Q v • fx
[PROOFSTEP]
rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self, zero_add]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑((fun d =>
            foldr' Q (contractLeftAux Q d)
              (_ :
                ∀ (v : M) (x fx : CliffordAlgebra Q),
                  ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
              0)
          (d₁ + d₂))
      x =
    ↑((fun d =>
              foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            d₁ +
          (fun d =>
              foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            d₂)
      x
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      x =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0 +
          foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
      x
[PROOFSTEP]
rw [LinearMap.add_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      x =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        x +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        x
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
r : R
⊢ ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      (↑(algebraMap R (CliffordAlgebra Q)) r) =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(algebraMap R (CliffordAlgebra Q)) r) +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(algebraMap R (CliffordAlgebra Q)) r)
[PROOFSTEP]
simp_rw [foldr'_algebraMap, smul_zero, zero_add]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x y : CliffordAlgebra Q
hx :
  ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      x =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        x +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        x
hy :
  ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      y =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        y +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        y
⊢ ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      (x + y) =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        (x + y) +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        (x + y)
[PROOFSTEP]
rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      m =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        m +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      (↑(ι Q) x * m) =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(ι Q) x * m) +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(ι Q) x * m)
[PROOFSTEP]
rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      m =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        m +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(↑(contractLeftAux Q (d₁ + d₂)) x)
      (m,
        ↑(foldr' Q (contractLeftAux Q d₁)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
                0)
            m +
          ↑(foldr' Q (contractLeftAux Q d₂)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
                0)
            m) =
    ↑(↑(contractLeftAux Q d₁) x)
        (m,
          ↑(foldr' Q (contractLeftAux Q d₁)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
                0)
            m) +
      ↑(↑(contractLeftAux Q d₂) x)
        (m,
          ↑(foldr' Q (contractLeftAux Q d₂)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
                0)
            m)
[PROOFSTEP]
dsimp only [contractLeftAux_apply_apply]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (d₁ + d₂))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (d₁ + d₂)) v) (x, fx)) =
                ↑Q v • fx)
          0)
      m =
    ↑(foldr' Q (contractLeftAux Q d₁)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
            0)
        m +
      ↑(foldr' Q (contractLeftAux Q d₂)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(d₁ + d₂) x • m -
      ↑(ι Q) x *
        (↑(foldr' Q (contractLeftAux Q d₁)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
                0)
            m +
          ↑(foldr' Q (contractLeftAux Q d₂)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
                0)
            m) =
    ↑d₁ x • m -
        ↑(ι Q) x *
          ↑(foldr' Q (contractLeftAux Q d₁)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₁) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₁) v) (x, fx)) = ↑Q v • fx)
                0)
            m +
      (↑d₂ x • m -
        ↑(ι Q) x *
          ↑(foldr' Q (contractLeftAux Q d₂)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d₂) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d₂) v) (x, fx)) = ↑Q v • fx)
                0)
            m)
[PROOFSTEP]
rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(AddHom.toFun
          {
            toFun := fun d =>
              foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0,
            map_add' :=
              (_ :
                ∀ (d₁ d₂ : Module.Dual R M),
                  (fun d =>
                        foldr' Q (contractLeftAux Q d)
                          (_ :
                            ∀ (v : M) (x fx : CliffordAlgebra Q),
                              ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                ↑Q v • fx)
                          0)
                      (d₁ + d₂) =
                    (fun d =>
                          foldr' Q (contractLeftAux Q d)
                            (_ :
                              ∀ (v : M) (x fx : CliffordAlgebra Q),
                                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                  ↑Q v • fx)
                            0)
                        d₁ +
                      (fun d =>
                          foldr' Q (contractLeftAux Q d)
                            (_ :
                              ∀ (v : M) (x fx : CliffordAlgebra Q),
                                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                  ↑Q v • fx)
                            0)
                        d₂) }
          (c • d))
      x =
    ↑(↑(RingHom.id R) c •
          AddHom.toFun
            {
              toFun := fun d =>
                foldr' Q (contractLeftAux Q d)
                  (_ :
                    ∀ (v : M) (x fx : CliffordAlgebra Q),
                      ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                  0,
              map_add' :=
                (_ :
                  ∀ (d₁ d₂ : Module.Dual R M),
                    (fun d =>
                          foldr' Q (contractLeftAux Q d)
                            (_ :
                              ∀ (v : M) (x fx : CliffordAlgebra Q),
                                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                  ↑Q v • fx)
                            0)
                        (d₁ + d₂) =
                      (fun d =>
                            foldr' Q (contractLeftAux Q d)
                              (_ :
                                ∀ (v : M) (x fx : CliffordAlgebra Q),
                                  ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                    ↑Q v • fx)
                              0)
                          d₁ +
                        (fun d =>
                            foldr' Q (contractLeftAux Q d)
                              (_ :
                                ∀ (v : M) (x fx : CliffordAlgebra Q),
                                  ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) =
                                    ↑Q v • fx)
                              0)
                          d₂) }
            d)
      x
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      x =
    ↑(↑(RingHom.id R) c •
          foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
      x
[PROOFSTEP]
rw [LinearMap.smul_apply, RingHom.id_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      x =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        x
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
r : R
⊢ ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      (↑(algebraMap R (CliffordAlgebra Q)) r) =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(algebraMap R (CliffordAlgebra Q)) r)
[PROOFSTEP]
simp_rw [foldr'_algebraMap, smul_zero]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x y : CliffordAlgebra Q
hx :
  ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      x =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        x
hy :
  ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      y =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        y
⊢ ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      (x + y) =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        (x + y)
[PROOFSTEP]
rw [map_add, map_add, smul_add, hx, hy]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      m =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      (↑(ι Q) x * m) =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        (↑(ι Q) x * m)
[PROOFSTEP]
rw [foldr'_ι_mul, foldr'_ι_mul, hx]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      m =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(↑(contractLeftAux Q (c • d)) x)
      (m,
        c •
          ↑(foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            m) =
    c •
      ↑(↑(contractLeftAux Q d) x)
        (m,
          ↑(foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            m)
[PROOFSTEP]
dsimp only [contractLeftAux_apply_apply]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx :
  ↑(foldr' Q (contractLeftAux Q (c • d))
          (_ :
            ∀ (v : M) (x fx : CliffordAlgebra Q),
              ↑(↑(contractLeftAux Q (c • d)) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q (c • d)) v) (x, fx)) = ↑Q v • fx)
          0)
      m =
    c •
      ↑(foldr' Q (contractLeftAux Q d)
            (_ :
              ∀ (v : M) (x fx : CliffordAlgebra Q),
                ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
            0)
        m
⊢ ↑(c • d) x • m -
      ↑(ι Q) x *
        c •
          ↑(foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            m =
    c •
      (↑d x • m -
        ↑(ι Q) x *
          ↑(foldr' Q (contractLeftAux Q d)
                (_ :
                  ∀ (v : M) (x fx : CliffordAlgebra Q),
                    ↑(↑(contractLeftAux Q d) v) (↑(ι Q) v * x, ↑(↑(contractLeftAux Q d) v) (x, fx)) = ↑Q v • fx)
                0)
            m)
[PROOFSTEP]
rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ↑(↑contractLeft d) (↑(ι Q) a * b) = ↑d a • b - ↑(ι Q) a * ↑(↑contractLeft d) b
[PROOFSTEP]
refine foldr'_ι_mul _ _ ?_ _ _ _
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ↑(↑(contractLeftAux Q d) m) (↑(ι Q) m * x, ↑(↑(contractLeftAux Q d) m) (x, fx)) = ↑Q m • fx
[PROOFSTEP]
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ↑(↑contractRight (b * ↑(ι Q) a)) d = ↑d a • b - ↑(↑contractRight b) d * ↑(ι Q) a
[PROOFSTEP]
rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul, reverse_reverse,
  reverse.map_mul, reverse_ι, contractRight_eq]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ ↑(↑contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r * b) =
    ↑(algebraMap R (CliffordAlgebra Q)) r * ↑(↑contractLeft d) b
[PROOFSTEP]
rw [← Algebra.smul_def, map_smul, Algebra.smul_def, Algebra.smul_def]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ ↑(↑contractLeft d) (a * ↑(algebraMap R (CliffordAlgebra Q)) r) =
    ↑(↑contractLeft d) a * ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes, Algebra.commutes]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ ↑(↑contractRight (↑(algebraMap R (CliffordAlgebra Q)) r * b)) d =
    ↑(algebraMap R (CliffordAlgebra Q)) r * ↑(↑contractRight b) d
[PROOFSTEP]
rw [← Algebra.smul_def, LinearMap.map_smul₂, Algebra.smul_def]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ ↑(↑contractRight (a * ↑(algebraMap R (CliffordAlgebra Q)) r)) d =
    ↑(↑contractRight a) d * ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
rw [← Algebra.commutes, contractRight_algebraMap_mul, Algebra.commutes]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : M
⊢ ↑(↑contractLeft d) (↑(ι Q) x) = ↑(algebraMap R (CliffordAlgebra Q)) (↑d x)
[PROOFSTEP]
refine
  (foldr'_ι _ _ ?_ _ _).trans <| by
    simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : M
⊢ ↑(↑(contractLeftAux Q d) x) (1, 0) = ↑(algebraMap R (CliffordAlgebra Q)) (↑d x)
[PROOFSTEP]
simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : M
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ↑(↑(contractLeftAux Q d) m) (↑(ι Q) m * x, ↑(↑(contractLeftAux Q d) m) (x, fx)) = ↑Q m • fx
[PROOFSTEP]
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : M
⊢ ↑(↑contractRight (↑(ι Q) x)) d = ↑(algebraMap R (CliffordAlgebra Q)) (↑d x)
[PROOFSTEP]
rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
⊢ ↑(↑contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r) = 0
[PROOFSTEP]
refine (foldr'_algebraMap _ _ ?_ _ _).trans <| smul_zero _
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ↑(↑(contractLeftAux Q d) m) (↑(ι Q) m * x, ↑(↑(contractLeftAux Q d) m) (x, fx)) = ↑Q m • fx
[PROOFSTEP]
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
⊢ ↑(↑contractRight (↑(algebraMap R (CliffordAlgebra Q)) r)) d = 0
[PROOFSTEP]
rw [contractRight_eq, reverse.commutes, contractLeft_algebraMap, map_zero]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
⊢ ↑(↑contractLeft d) 1 = 0
[PROOFSTEP]
simpa only [map_one] using contractLeft_algebraMap Q d 1
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
⊢ ↑(↑contractRight 1) d = 0
[PROOFSTEP]
simpa only [map_one] using contractRight_algebraMap Q d 1
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d) x) = 0
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r)) = 0
[PROOFSTEP]
simp_rw [contractLeft_algebraMap, map_zero]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x y : CliffordAlgebra Q
hx : ↑(↑contractLeft d) (↑(↑contractLeft d) x) = 0
hy : ↑(↑contractLeft d) (↑(↑contractLeft d) y) = 0
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d) (x + y)) = 0
[PROOFSTEP]
rw [map_add, map_add, hx, hy, add_zero]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx : ↑(↑contractLeft d) (↑(↑contractLeft d) m) = 0
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d) (↑(ι Q) x * m)) = 0
[PROOFSTEP]
rw [contractLeft_ι_mul, map_sub, contractLeft_ι_mul, hx, LinearMap.map_smul, mul_zero, sub_zero, sub_self]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(↑contractRight (↑(↑contractRight x) d)) d = 0
[PROOFSTEP]
rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d') x) = -↑(↑contractLeft d') (↑(↑contractLeft d) x)
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r : R
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d') (↑(algebraMap R (CliffordAlgebra Q)) r)) =
    -↑(↑contractLeft d') (↑(↑contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r))
[PROOFSTEP]
simp_rw [contractLeft_algebraMap, map_zero, neg_zero]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x y : CliffordAlgebra Q
hx : ↑(↑contractLeft d) (↑(↑contractLeft d') x) = -↑(↑contractLeft d') (↑(↑contractLeft d) x)
hy : ↑(↑contractLeft d) (↑(↑contractLeft d') y) = -↑(↑contractLeft d') (↑(↑contractLeft d) y)
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d') (x + y)) = -↑(↑contractLeft d') (↑(↑contractLeft d) (x + y))
[PROOFSTEP]
rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx : ↑(↑contractLeft d) (↑(↑contractLeft d') m) = -↑(↑contractLeft d') (↑(↑contractLeft d) m)
⊢ ↑(↑contractLeft d) (↑(↑contractLeft d') (↑(ι Q) x * m)) = -↑(↑contractLeft d') (↑(↑contractLeft d) (↑(ι Q) x * m))
[PROOFSTEP]
simp only [contractLeft_ι_mul, map_sub, LinearMap.map_smul]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx : ↑(↑contractLeft d) (↑(↑contractLeft d') m) = -↑(↑contractLeft d') (↑(↑contractLeft d) m)
⊢ ↑d' x • ↑(↑contractLeft d) m -
      (↑d x • ↑(↑contractLeft d') m - ↑(ι Q) x * ↑(↑contractLeft d) (↑(↑contractLeft d') m)) =
    -(↑d x • ↑(↑contractLeft d') m -
        (↑d' x • ↑(↑contractLeft d) m - ↑(ι Q) x * ↑(↑contractLeft d') (↑(↑contractLeft d) m)))
[PROOFSTEP]
rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(↑contractRight (↑(↑contractRight x) d)) d' = -↑(↑contractRight (↑(↑contractRight x) d')) d
[PROOFSTEP]
rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse, reverse_reverse,
  contractLeft_comm, map_neg]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ ↑(↑(changeFormAux Q B) v) (↑(↑(changeFormAux Q B) v) x) = (↑Q v - BilinForm.bilin B v v) • x
[PROOFSTEP]
simp only [changeFormAux_apply_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ ↑(ι Q) v * (↑(ι Q) v * x - ↑(↑contractLeft (↑(↑BilinForm.toLin B) v)) x) -
      ↑(↑contractLeft (↑(↑BilinForm.toLin B) v)) (↑(ι Q) v * x - ↑(↑contractLeft (↑(↑BilinForm.toLin B) v)) x) =
    (↑Q v - BilinForm.bilin B v v) • x
[PROOFSTEP]
rw [mul_sub, ← mul_assoc, ι_sq_scalar, map_sub, contractLeft_ι_mul, ← sub_add, sub_sub_sub_comm, ← Algebra.smul_def,
  BilinForm.toLin_apply, sub_self, sub_zero, contractLeft_contractLeft, add_zero, sub_smul]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h✝ : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
h : BilinForm.toQuadraticForm B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ (↑Q' m - BilinForm.bilin B m m) • x = ↑Q m • x
[PROOFSTEP]
dsimp only [← BilinForm.toQuadraticForm_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h✝ : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
h : BilinForm.toQuadraticForm B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ (↑Q' m - ↑(BilinForm.toQuadraticForm B) m) • x = ↑Q m • x
[PROOFSTEP]
rw [h, QuadraticForm.sub_apply, sub_sub_cancel]
[GOAL]
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
inst✝ : Invertible 2
⊢ BilinForm.toQuadraticForm (↑QuadraticForm.associated (-Q)) = 0 - Q
[PROOFSTEP]
simp [QuadraticForm.toQuadraticForm_associated]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
⊢ ↑(changeForm h) 1 = 1
[PROOFSTEP]
simpa using changeForm_algebraMap h (1 : R)
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m : M
⊢ ↑(ι Q') m = ↑(↑(changeFormAux Q' B) m) 1
[PROOFSTEP]
rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m : M
x : CliffordAlgebra Q
⊢ ↑(↑(foldr Q (changeFormAux Q' B)
              (_ :
                ∀ (m : M) (x : CliffordAlgebra Q'),
                  ↑(↑(changeFormAux Q' B) m) (↑(↑(changeFormAux Q' B) m) x) = ↑Q m • x))
          (↑(↑(foldr Q (changeFormAux Q' B)
                    (_ :
                      ∀ (m : M) (x : CliffordAlgebra Q'),
                        ↑(↑(changeFormAux Q' B) m) (↑(↑(changeFormAux Q' B) m) x) = ↑Q m • x))
                1)
            x))
      (↑(ι Q) m) =
    ↑(ι Q') m * ↑(changeForm h) x - ↑(↑contractLeft (↑(↑BilinForm.toLin B) m)) (↑(changeForm h) x)
[PROOFSTEP]
rw [foldr_ι]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m : M
x : CliffordAlgebra Q
⊢ ↑(↑(changeFormAux Q' B) m)
      (↑(↑(foldr Q (changeFormAux Q' B)
                (_ :
                  ∀ (m : M) (x : CliffordAlgebra Q'),
                    ↑(↑(changeFormAux Q' B) m) (↑(↑(changeFormAux Q' B) m) x) = ↑Q m • x))
            1)
        x) =
    ↑(ι Q') m * ↑(changeForm h) x - ↑(↑contractLeft (↑(↑BilinForm.toLin B) m)) (↑(changeForm h) x)
[PROOFSTEP]
rfl
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m₁ m₂ : M
⊢ ↑(changeForm h) (↑(ι Q) m₁ * ↑(ι Q) m₂) =
    ↑(ι Q') m₁ * ↑(ι Q') m₂ - ↑(algebraMap R (CliffordAlgebra Q')) (BilinForm.bilin B m₁ m₂)
[PROOFSTEP]
rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι, BilinForm.toLin_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ ↑(changeForm h) (↑(↑contractLeft d) x) = ↑(↑contractLeft d) (↑(changeForm h) x)
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
d : Module.Dual R M
r : R
⊢ ↑(changeForm h) (↑(↑contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r)) =
    ↑(↑contractLeft d) (↑(changeForm h) (↑(algebraMap R (CliffordAlgebra Q)) r))
[PROOFSTEP]
simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
d : Module.Dual R M
x y : CliffordAlgebra Q
hx : ↑(changeForm h) (↑(↑contractLeft d) x) = ↑(↑contractLeft d) (↑(changeForm h) x)
hy : ↑(changeForm h) (↑(↑contractLeft d) y) = ↑(↑contractLeft d) (↑(changeForm h) y)
⊢ ↑(changeForm h) (↑(↑contractLeft d) (x + y)) = ↑(↑contractLeft d) (↑(changeForm h) (x + y))
[PROOFSTEP]
rw [map_add, map_add, map_add, map_add, hx, hy]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
d : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx : ↑(changeForm h) (↑(↑contractLeft d) m) = ↑(↑contractLeft d) (↑(changeForm h) m)
⊢ ↑(changeForm h) (↑(↑contractLeft d) (↑(ι Q) x * m)) = ↑(↑contractLeft d) (↑(changeForm h) (↑(ι Q) x * m))
[PROOFSTEP]
simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, LinearMap.map_smul]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
d : Module.Dual R M
m : CliffordAlgebra Q
x : M
hx : ↑(changeForm h) (↑(↑contractLeft d) m) = ↑(↑contractLeft d) (↑(changeForm h) m)
⊢ ↑d x • ↑(changeForm h) m -
      (↑(ι Q') x * ↑(changeForm h) (↑(↑contractLeft d) m) -
        ↑(↑contractLeft (↑(↑BilinForm.toLin B) x)) (↑(changeForm h) (↑(↑contractLeft d) m))) =
    ↑d x • ↑(changeForm h) m - ↑(ι Q') x * ↑(↑contractLeft d) (↑(changeForm h) m) -
      ↑(↑contractLeft d) (↑(↑contractLeft (↑(↑BilinForm.toLin B) x)) (↑(changeForm h) m))
[PROOFSTEP]
rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) x = x
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
r : R
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) (↑(algebraMap R (CliffordAlgebra Q)) r) =
    ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
simp_rw [changeForm_algebraMap]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
x y : CliffordAlgebra Q
hx : ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) x = x
hy : ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) y = y
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) (x + y) = x + y
[PROOFSTEP]
rw [map_add, hx, hy]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m : CliffordAlgebra Q
x : M
hx : ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) m = m
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm 0 = Q - Q)) (↑(ι Q) x * m) = ↑(ι Q) x * m
[PROOFSTEP]
rw [changeForm_ι_mul, hx, map_zero, LinearMap.zero_apply, map_zero, LinearMap.zero_apply, sub_zero]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ ↑(changeForm h') (↑(changeForm h) x) = ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) x
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
r : R
⊢ ↑(changeForm h') (↑(changeForm h) (↑(algebraMap R (CliffordAlgebra Q)) r)) =
    ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) (↑(algebraMap R (CliffordAlgebra Q)) r)
[PROOFSTEP]
simp_rw [changeForm_algebraMap]
[GOAL]
case h_add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
x y : CliffordAlgebra Q
hx : ↑(changeForm h') (↑(changeForm h) x) = ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) x
hy : ↑(changeForm h') (↑(changeForm h) y) = ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) y
⊢ ↑(changeForm h') (↑(changeForm h) (x + y)) = ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) (x + y)
[PROOFSTEP]
rw [map_add, map_add, map_add, hx, hy]
[GOAL]
case h_mul_ι
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
m : CliffordAlgebra Q
x : M
hx : ↑(changeForm h') (↑(changeForm h) m) = ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) m
⊢ ↑(changeForm h') (↑(changeForm h) (↑(ι Q) x * m)) =
    ↑(changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) (↑(ι Q) x * m)
[PROOFSTEP]
rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub, map_add, LinearMap.add_apply, map_add,
  LinearMap.add_apply, changeForm_contractLeft, hx, add_comm (_ : CliffordAlgebra Q'')]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm (-B) = Q - Q'))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(changeForm h),
                map_add' :=
                  (_ :
                    ∀ (x y : CliffordAlgebra Q),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : CliffordAlgebra Q),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm (-B) = Q - Q')) (↑(changeForm h) x) = x
[PROOFSTEP]
exact (changeForm_changeForm _ _ x).trans <| by simp_rw [add_right_neg, changeForm_self_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm (B + -B) = Q - Q)) x = x
[PROOFSTEP]
simp_rw [add_right_neg, changeForm_self_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q'
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(changeForm h),
              map_add' :=
                (_ :
                  ∀ (x y : CliffordAlgebra Q),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : CliffordAlgebra Q),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(changeForm (_ : BilinForm.toQuadraticForm (-B) = Q - Q')) x) =
    x
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q'
⊢ ↑(changeForm h) (↑(changeForm (_ : BilinForm.toQuadraticForm (-B) = Q - Q')) x) = x
[PROOFSTEP]
exact (changeForm_changeForm _ _ x).trans <| by simp_rw [add_left_neg, changeForm_self_apply]
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinForm.toQuadraticForm B = Q' - Q
h' : BilinForm.toQuadraticForm B' = Q'' - Q'
src✝ : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' := changeForm h
x : CliffordAlgebra Q'
⊢ ↑(changeForm (_ : BilinForm.toQuadraticForm (-B + B) = Q' - Q')) x = x
[PROOFSTEP]
simp_rw [add_left_neg, changeForm_self_apply]


[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (nhds a)
[PROOFSTEP]
rw [nhds_discrete]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (pure a)
[PROOFSTEP]
exact isCountablyGenerated_pure
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
hd : DiscreteTopology α
inst✝ : Encodable α
i : α
⊢ instTopologicalSpaceSubtype = generateFrom {univ}
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
refine' (eq_bot_of_singletons_open fun a => _).symm
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ IsOpen {a}
[PROOFSTEP]
have h_singleton_eq_inter : { a } = Iio (succ a) ∩ Ioi (pred a) :=
  by
  suffices h_singleton_eq_inter' : { a } = Iic a ∩ Ici a
  · rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
  rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ {a} = Iio (succ a) ∩ Ioi (pred a)
[PROOFSTEP]
suffices h_singleton_eq_inter' : { a } = Iic a ∩ Ici a
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter' : {a} = Iic a ∩ Ici a
⊢ {a} = Iio (succ a) ∩ Ioi (pred a)
[PROOFSTEP]
rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
[GOAL]
case h_singleton_eq_inter'
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ {a} = Iic a ∩ Ici a
[PROOFSTEP]
rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
[PROOFSTEP]
apply @IsOpen.inter _ _ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case h₁
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ DiscreteTopology α ↔ OrderTopology α
[PROOFSTEP]
refine' ⟨fun h => ⟨_⟩, fun h => ⟨_⟩⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : DiscreteTopology α
⊢ inst✝⁵ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
rw [h.eq_bot]
[GOAL]
case refine'_1
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : DiscreteTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder
[GOAL]
case refine'_2
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : OrderTopology α
⊢ inst✝⁵ = ⊥
[PROOFSTEP]
rw [h.topology_eq_generate_intervals]
[GOAL]
case refine'_2
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : OrderTopology α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = ⊥
[PROOFSTEP]
exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder.symm
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
refine' (eq_bot_of_singletons_open fun a => _).symm
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ IsOpen {a}
[PROOFSTEP]
have h_singleton_eq_inter : { a } = Iic a ∩ Ici a := by rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ {a} = Iic a ∩ Ici a
[PROOFSTEP]
rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_top : IsTop a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_bot : IsBot a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_bot.Ici_eq] at h_singleton_eq_inter
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `isOpen_univ` explicitly to fix an error.
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen univ
[PROOFSTEP]
apply @isOpen_univ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isBot_iff_isMin] at ha_bot
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isTop_iff_isMax] at ha_top
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Iio_succ_of_not_isMax ha_top] at h_singleton_eq_inter
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_bot : IsBot a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isBot_iff_isMin] at ha_bot
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
[PROOFSTEP]
apply @IsOpen.inter _ _ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case neg.h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case neg.h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α
[PROOFSTEP]
refine' ⟨fun h => ⟨_⟩, fun h => ⟨_⟩⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
rw [h.eq_bot]
[GOAL]
case refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
exact LinearOrder.bot_topologicalSpace_eq_generateFrom
[GOAL]
case refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : OrderTopology α
⊢ inst✝³ = ⊥
[PROOFSTEP]
rw [h.topology_eq_generate_intervals]
[GOAL]
case refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : OrderTopology α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = ⊥
[PROOFSTEP]
exact LinearOrder.bot_topologicalSpace_eq_generateFrom.symm
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ MetrizableSpace α
[PROOFSTEP]
obtain rfl := DiscreteTopology.eq_bot (α := α)
[GOAL]
α : Type u_1
inst✝ : DiscreteTopology α
⊢ MetrizableSpace α
[PROOFSTEP]
exact @UniformSpace.metrizableSpace α ⊥ (isCountablyGenerated_principal _) _


[GOAL]
p q : ℚ
s t : Set ℚ
⊢ NeBot (cocompact ℚ ⊓ 𝓝 p)
[PROOFSTEP]
refine' (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 _
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ∀ {i : Set ℚ × Set ℚ}, IsCompact i.fst ∧ p ∈ i.snd ∧ IsOpen i.snd → Set.Nonempty (i.fstᶜ ∩ i.snd)
[PROOFSTEP]
rintro ⟨s, o⟩ ⟨hs, hpo, ho⟩
[GOAL]
case mk.intro.intro
p q : ℚ
s✝ t s o : Set ℚ
hs : IsCompact (s, o).fst
hpo : p ∈ (s, o).snd
ho : IsOpen (s, o).snd
⊢ Set.Nonempty ((s, o).fstᶜ ∩ (s, o).snd)
[PROOFSTEP]
rw [inter_comm]
[GOAL]
case mk.intro.intro
p q : ℚ
s✝ t s o : Set ℚ
hs : IsCompact (s, o).fst
hpo : p ∈ (s, o).snd
ho : IsOpen (s, o).snd
⊢ Set.Nonempty ((s, o).snd ∩ (s, o).fstᶜ)
[PROOFSTEP]
exact (dense_compl_compact hs).inter_open_nonempty _ ho ⟨p, hpo⟩
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬IsCountablyGenerated (cocompact ℚ)
[PROOFSTEP]
intro H
[GOAL]
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
⊢ False
[PROOFSTEP]
rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩
[GOAL]
case intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False
[PROOFSTEP]
rw [tendsto_inf] at hx
[GOAL]
case intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
[PROOFSTEP]
rcases hx with ⟨hxc, hx0⟩
[GOAL]
case intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x)
[GOAL]
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ ∃ n, ¬x n ∈ insert 0 (range x)
case intro.intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : ¬x n ∈ insert 0 (range x)
⊢ False
[PROOFSTEP]
exact (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists
[GOAL]
case intro.intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : ¬x n ∈ insert 0 (range x)
⊢ False
[PROOFSTEP]
exact hn (Or.inr ⟨n, rfl⟩)
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬IsCountablyGenerated (𝓝 ∞)
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ False
[PROOFSTEP]
have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
[PROOFSTEP]
infer_instance
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
⊢ False
[PROOFSTEP]
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (cocompact ℚ)
⊢ False
[PROOFSTEP]
exact not_countably_generated_cocompact this
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬FirstCountableTopology ℚ∞
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : FirstCountableTopology ℚ∞
⊢ False
[PROOFSTEP]
exact not_countably_generated_nhds_infty_opc inferInstance
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬SecondCountableTopology ℚ∞
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : SecondCountableTopology ℚ∞
⊢ False
[PROOFSTEP]
exact not_firstCountableTopology_opc inferInstance
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ TotallyDisconnectedSpace ℚ
[PROOFSTEP]
refine' ⟨fun s hsu hs x hx y hy => _⟩
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hsu : s ⊆ univ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
[PROOFSTEP]
clear hsu
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
[PROOFSTEP]
by_contra' H : x ≠ y
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
⊢ False
[PROOFSTEP]
wlog hlt : x < y
[GOAL]
case inr
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ False
[PROOFSTEP]
refine' this s hs y hy x hx H.symm <| H.lt_or_lt.resolve_left hlt
[GOAL]
case inr.refine'_1
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_2
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_3
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ Set ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_4
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ Set ℚ
[PROOFSTEP]
assumption
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False
[PROOFSTEP]
rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
⊢ False
[PROOFSTEP]
have := hs.image _ continuous_coe_real.continuousOn
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this : IsPreconnected (Rat.cast '' s)
⊢ False
[PROOFSTEP]
rw [isPreconnected_iff_ordConnected] at this
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this✝ : IsPreconnected (Rat.cast '' s)
this : OrdConnected (Rat.cast '' s)
⊢ False
[PROOFSTEP]
have : z ∈ Rat.cast '' s := this.out (mem_image_of_mem _ hx) (mem_image_of_mem _ hy) ⟨hxz.le, hzy.le⟩
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this✝¹ : IsPreconnected (Rat.cast '' s)
this✝ : OrdConnected (Rat.cast '' s)
this : z ∈ Rat.cast '' s
⊢ False
[PROOFSTEP]
exact hz (image_subset_range _ _ this)