mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2.calc_1
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 : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i

Tactic:
[

Goal state after:
case mpr.refine_2.calc_1
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 : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
i : n
hi : v i ≠ 0 i
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)

Tactic:
[

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
i : n
hi : v i ≠ 0 i
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b

Tactic:
[

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case refine_1
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ Pairwise fun i j ↦ Aᵀ i j < 0

Tactic:
[

Goal state after:
case refine_1
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ Pairwise fun i j ↦ Aᵀ i j < 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ ∀ (j : n), 0 < ∑ i, Aᵀ i j

Tactic:
[

Goal state after:
case refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ ∀ (j : n), 0 < ∑ i, Aᵀ i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
⊢ Q₃ (g (f x)) = Q₁ x

Tactic:
by rw [← f.map_app, ← g.map_app]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), (((associatedHom K) Q) (v i)) (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
[

Goal state after:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), (((associatedHom K) Q) (v i)) (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (map (Int.castRingHom R)) g = (map (Int.castRingHom R)) h → g = h

Tactic:
[

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (map (Int.castRingHom R)) g = (map (Int.castRingHom R)) h → g = h
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ (↑A).adjugate i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Tactic:
this

Goal state after:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0] i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
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

Tactic:
fin_cases j

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, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
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:
fin_cases j

Goal state after:
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 h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
[

Goal state after:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a, b; 0, a⁻¹], ⋯⟩
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

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
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
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_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

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
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
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_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 «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

Tactic:
fin_cases j

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, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
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:
fin_cases j

Goal state after:
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.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)
⊢ ((lift Q) ⟨f, cond⟩).range = Algebra.adjoin R (Set.range ⇑f)

Tactic:
[

Goal state after:
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)
⊢ ((lift Q) ⟨f, cond⟩).range = Algebra.adjoin R (Set.range ⇑f)
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)
⊢ Algebra.adjoin R (Set.range fun x ↦ ((lift Q) ⟨f, cond⟩) ((ι Q) x)) = Algebra.adjoin R (Set.range ⇑f)

Tactic:
lift_ι_apply

Goal state after:
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_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
      LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)

Tactic:
[

Goal state after:
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_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
      LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ coeMonoidHom ⟨diagonal D, hD⟩ =
    {i | i ≠ i₀}.noncommProd (fun i ↦ coeMonoidHom (if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)) ⋯

Tactic:
[

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ coeMonoidHom ⟨diagonal D, hD⟩ =
    {i | i ≠ i₀}.noncommProd (fun i ↦ coeMonoidHom (if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)) ⋯
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ diagonal D = {i | i ≠ i₀}.noncommProd (fun x ↦ diagonal (g x)) ⋯

Tactic:
[

Goal state after:
case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ diagonal D = {i | i ≠ i₀}.noncommProd (fun x ↦ diagonal (g x)) ⋯
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ↑M =
    ↑((List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, ⋯⟩ *
        (List.map TransvectionStruct.toSpecialLinearGroup L').prod)

Tactic:
[

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ↑M =
    ↑((List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, ⋯⟩ *
        (List.map TransvectionStruct.toSpecialLinearGroup L').prod)
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = (List.map (fun a ↦ ⟨(f a).fst, (f a).snd⟩) l).prod

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = (List.map (fun a ↦ ⟨(f a).fst, (f a).snd⟩) l).prod
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
j : Fin 2
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
j : Fin 2
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((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
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
j : Fin 2
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
j : Fin 2
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
fin_cases j

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = 1

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
fin_cases j

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = 0

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = 0