mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case left
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤

pp: case right
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
<;>

Goal state after:
case left
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤

case right
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
<;>

Goal state after:
case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
<;>

Goal state after:
case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case pos
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

pp: case neg
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

case neg
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m

Tactic:
by
  obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)
  rw [← restrictRootsOfUnity_coe_apply, hm, ← zpow_mod_orderOf, ← Int.toNat_of_nonneg
      (m.emod_nonneg (Int.natCast_ne_zero.mpr (pos_iff_ne_zero.mp (orderOf_pos ζ)))),
    zpow_natCast, rootsOfUnity.coe_pow]
  exact ⟨(m % orderOf ζ).toNat, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mp
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

pp: case mpr
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
<;>

Goal state after:
case mp
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

case mpr
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r else 1) * diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) = 1

pp: case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) * diagonal fun j ↦ if j = i then ↑r else 1) = 1

Tactic:
<;>

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r else 1) * diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) = 1

case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ((diagonal fun j ↦ if j = i then ↑r⁻¹ else 1) * diagonal fun j ↦ if j = i then ↑r else 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then 1 else ↑r⁻¹ else if i_1 = i then ↑r else 1) = 1

pp: case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then ↑r⁻¹ * ↑r else ↑r else if i_1 = i then ↑r⁻¹ else 1) = 1

Tactic:
<;>

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then 1 else ↑r⁻¹ else if i_1 = i then ↑r else 1) = 1

case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then ↑r⁻¹ * ↑r else ↑r else if i_1 = i then ↑r⁻¹ else 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then 1 else ↑r⁻¹ else if j = i then ↑r else 1) = 1 j

pp: case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then ↑r⁻¹ * ↑r else ↑r else if j = i then ↑r⁻¹ else 1) = 1 j

Tactic:
<;>

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then 1 else ↑r⁻¹ else if j = i then ↑r else 1) = 1 j

case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then ↑r⁻¹ * ↑r else ↑r else if j = i then ↑r⁻¹ else 1) = 1 j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case pos
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : j = i
⊢ 1 = 1 j

pp: case neg
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : ¬j = i
⊢ 1 = 1 j

pp: case pos
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : j = i
⊢ ↑r⁻¹ * ↑r = 1 j

pp: case neg
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : ¬j = i
⊢ 1 = 1 j

Tactic:
<;>

Goal state after:
case pos
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : j = i
⊢ 1 = 1 j

case neg
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : ¬j = i
⊢ 1 = 1 j

case pos
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : j = i
⊢ ↑r⁻¹ * ↑r = 1 j

case neg
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
h✝ : ¬j = i
⊢ 1 = 1 j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case isTrue
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f ↑u = f ↑u

pp: case isFalse
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0

Tactic:
<;>

Goal state after:
case isTrue
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f ↑u = f ↑u

case isFalse
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) j = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) j = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) j = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) j = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0».«0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![m 0 0, m 0 1; m 1 0, m 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 1 0 * ↑A 0 1 = 1

pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
<;>

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 1 0 * ↑A 0 1 = 1

case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 0 1 * ↑A 1 0 = 1

pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
<;>

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 0 1 * ↑A 1 0 = 1

case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, -v; b, u].det = 1

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, a; -u, b].det = 1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, -v; b, u].det = 1

case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, a; -u, b].det = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, b; -v, u].det = 1

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, -u; a, b].det = 1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, b; -v, u].det = 1

case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, -u; a, b].det = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ v ((fun i ↦ i) ⟨0, ⋯⟩) = ↑g 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ v ((fun i ↦ i) ⟨1, ⋯⟩) = ↑g 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ v ((fun i ↦ i) ⟨0, ⋯⟩) = ↑g 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ v ((fun i ↦ i) ⟨1, ⋯⟩) = ↑g 0 ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) j = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) j = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) j = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) j = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ g = (lift Q) ⟨f, cond⟩

Tactic:
by
  convert! (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq
  rw [lift_symm_apply, Subtype.mk_eq_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
x : CliffordAlgebra Q₁
⊢ (equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁)) x = AlgEquiv.refl x

Tactic:
exact AlgHom.congr_fun (map_id Q₁) x

Goal state after: