-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q)
    [Invertible (2 : R)] :
    ConjAct.toConjAct x • LinearMap.range (ι Q) = LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ LinearMap.range (ι Q) ≤
    Submodule.comap (DistribMulAction.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (LinearMap.range (ι Q))

Tactic:
rintro _ ⟨m, rfl⟩

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
m : M
⊢ (ι Q) m ∈
    Submodule.comap (DistribMulAction.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (LinearMap.range (ι Q))

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
⊢ ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)

Tactic:
intro x hx

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this✝ : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
this : ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)

Tactic:
refine Eq.trans_le ?_ this

Result:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this✝ : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
this : ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) = ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
⊢ ConjAct.toConjAct x • LinearMap.range (ι Q) = LinearMap.range (ι Q)

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
⊢ ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)

case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
m : M
⊢ (ι Q) m ∈
    Submodule.comap (DistribMulAction.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (LinearMap.range (ι Q))

Tactic:
exact conjAct_smul_ι_mem_range_ι hx _

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
⊢ ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)

Tactic:
exact this _ hx

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)

Tactic:
have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)

Result:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this✝ : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
this : ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)

Tactic:
erw [Submodule.map_le_iff_le_comap]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
hx✝ : x✝ ∈ lipschitzGroup Q
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
⊢ LinearMap.range (ι Q) ≤
    Submodule.comap (DistribMulAction.toLinearMap R (CliffordAlgebra Q) (ConjAct.toConjAct x)) (LinearMap.range (ι Q))

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
inst✝ : Invertible 2
this✝ : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
this : ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q) ≤ ConjAct.toConjAct x • LinearMap.range (ι Q)
⊢ LinearMap.range (ι Q) = ConjAct.toConjAct x • ConjAct.toConjAct x⁻¹ • LinearMap.range (ι Q)

Tactic:
simp only [map_inv, smul_inv_smul]

Result:
no goals