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

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r

pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r

Tactic:
·

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r

Tactic:
·

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2

Tactic:
·

Goal state after:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ 1 = 1

pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = 1

pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = ⟨⋯.unit * ⋯.unit, ⋯⟩

Tactic:
·

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = 1

pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = ⟨⋯.unit * ⋯.unit, ⋯⟩

Tactic:
·

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
·

Goal state after:
case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ ↑↑↑g = LinearMap.id

pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑↑g = LinearMap.id

pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id

Tactic:
·

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ ↑↑↑g = LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑↑g = LinearMap.id

pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id

Tactic:
·

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑↑g = LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id

Tactic:
·

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

Tactic:
·

Goal state after:
case pos
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case e'_2
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = 1

Tactic:
·

Goal state after:
case e'_2
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = 1
Module: Mathlib.LinearAlgebra.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (a : M), 0 a = 0 (Submodule.Quotient.mk a)

Tactic:
LinearMap.zero_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (a : M), True
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case e'_3
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(center_equiv_rootsOfUnity g) = 1

Tactic:
·

Goal state after:
case e'_3
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(center_equiv_rootsOfUnity g) = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

Tactic:
·

Goal state after:
case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))

pp: case neg
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))

Tactic:
·

Goal state after:
case pos
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))

Tactic:
·

Goal state after:
case neg
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (x y : M ⧸ N),
    Quotient.lift ⇑Q ⋯ (x + y) =
      Quotient.lift ⇑Q ⋯ x + Quotient.lift ⇑Q ⋯ y + ((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯) x) y

pp: case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker

Tactic:
·

Goal state after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (x y : M ⧸ N),
    Quotient.lift ⇑Q ⋯ (x + y) =
      Quotient.lift ⇑Q ⋯ x + Quotient.lift ⇑Q ⋯ y + ((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯) x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker

Tactic:
·

Goal state after:
case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ N ≤ Q.radical → ∃ Q', Q'.comp N.mkQ = Q

pp: case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical

Tactic:
·

Goal state after:
case mp
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ N ≤ Q.radical → ∃ Q', Q'.comp N.mkQ = Q
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical

Tactic:
·

Goal state after:
case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical