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

Goal state before:
pp: case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = 1
⊢ (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j

pp: case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = -1
⊢ (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = 1
⊢ (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j

case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = -1
⊢ (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = 1
⊢ (1 + A s j) * (1 + A t j) = 1 + A s j + A t j + A s j * A t j

pp: case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = -1
⊢ (1 + -A s j) * (1 + -A t j) = 1 + -A s j + -A t j + A s j * A t j

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = 1
⊢ (1 + A s j) * (1 + A t j) = 1 + A s j + A t j + A s j * A t j

case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = -1
⊢ (1 + -A s j) * (1 + -A t j) = 1 + -A s j + -A t j + A s j * A t j
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
j : n
hs : A s j = 1
⊢ 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)

pp: case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
j : n
hs : A s j = -1
⊢ 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)

Tactic:
<;>

Goal state after:
case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
j : n
hs : A s j = 1
⊢ 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)

case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
j : n
hs : A s j = -1
⊢ 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
⊢ single i j r i j • v j = Pi.single i (r • v j) i

pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' : ι
hi : i ≠ i'
⊢ single i j r i' j • v j = Pi.single i (r • v j) i'

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
⊢ single i j r i j • v j = Pi.single i (r • v j) i

case inr
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' : ι
hi : i ≠ i'
⊢ single i j r i' j • v j = Pi.single i (r • v j) i'
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: case e_M.inl
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k = i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i

pp: case e_M.inr
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k ≠ i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i

Tactic:
<;>

Goal state after:
case e_M.inl
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k = i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i

case e_M.inr
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k ≠ i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 0
⊢ (star f).ofConv i j = f.ofConv i j

pp: case inr
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 1
⊢ (star f).ofConv i j = f.ofConv i j

Tactic:
<;>

Goal state after:
case inl
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 0
⊢ (star f).ofConv i j = f.ofConv i j

case inr
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 1
⊢ (star f).ofConv i j = f.ofConv i j
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y : (i : ι) → A i
⊢ (mul ((tprod R) x)) ((tprod R) y) = (tprod R) (x * y)

Tactic:
by
  simp only [mul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply', Pi.mul_def]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : MultilinearMap R M N
h : ∀ (j : (i : ι) → γ i), (φ fun i ↦ g (j i)) = φ' fun i ↦ g (j i)
⊢ lift φ = lift φ'

Tactic:
exact PiTensorProduct.ext_of_span_eq_top hg (fun j ↦ by simpa using h j)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬¬Independent f

Tactic:
Classical.not_not

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ Independent f
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
hS' : S = ∅
⊢ IsCollinear S

pp: case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
x : ℙ K V
hx : S = {x}
⊢ IsCollinear S

Tactic:
<;>

Goal state after:
case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
hS' : S = ∅
⊢ IsCollinear S

case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
x : ℙ K V
hx : S = {x}
⊢ IsCollinear S
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x = u → x ∈ ↑p

pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x ∈ {v} → x ∈ ↑p

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x = u → x ∈ ↑p

case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x ∈ {v} → x ∈ ↑p
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «0»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «1»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
<;>

Goal state after:
case «0»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «1»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «0».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «1».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
<;>

Goal state after:
case «0».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «1».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 0 1) ≤ ⨆ p, lineStab p.submodule

pp: case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 1 1) ≤ ⨆ p, lineStab p.submodule

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 0 1) ≤ ⨆ p, lineStab p.submodule

case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 1 1) ≤ ⨆ p, lineStab p.submodule
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 0 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule

pp: case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 1 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 0 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule

case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 1 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : w i = 0
⊢ 0 * ↑1 ^ 2 = w i

pp: case neg
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ 1 * ↑(Units.mk0 ⋯.choose ⋯) ^ 2 = w i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : w i = 0
⊢ 0 * ↑1 ^ 2 = w i

case neg
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ 1 * ↑(Units.mk0 ⋯.choose ⋯) ^ 2 = w i
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_1
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
w : V
hw : w ∈ R ∙ v
⊢ w ∈ Submodule.comap A (R ∙ v)

pp: case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
w : V
hw : w ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨w, hw⟩ = (c • id) ⟨w, hw⟩

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
w : V
hw : w ∈ R ∙ v
⊢ w ∈ Submodule.comap A (R ∙ v)

case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
w : V
hw : w ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨w, hw⟩ = (c • id) ⟨w, hw⟩
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: 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 : SpecialLinearGroup R V
hg : g ∈ Subgroup.center (SpecialLinearGroup R V)
x : V
⊢ ↑↑g x = ⋯.choose • x

Tactic:
let H := (mem_center_iff.mp hg).choose_spec.2
  rw [LinearMap.ext_iff] at H
  simp [H]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ Q ((linearCombination R g) l) =
    (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (linearCombination R (⇑Q ∘ g)) (l * l)

Tactic:
by
  simp_rw [linearCombination_apply, map_finsuppSum', Q.map_smul, mul_smul]
  rw [(l * l).sum_of_support_subset support_mul_subset_left _ <| by simp,
    l.sym2Mul.sum_of_support_subset support_sym2Mul_subset _ <| by simp]
  simp [Finsupp.sum, ← polarSym2_map_smul, mul_smul]

Goal state after:
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

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'_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

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.QuadraticForm.Real

Goal state before:
pp: ι : 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
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
⊢ (weightedSumSquares ℝ fun i ↦ ↑(sign (w i))) v =
    ((weightedSumSquares ℝ w).basisRepr ((Pi.basisFun ℝ ι).unitsSMul fun i ↦ Units.mk0 (1 / √|↑(u i)|) ⋯)) v

Tactic:
suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]

Goal state after:
ι : 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
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
⊢ ∑ i, w i / |↑(u i)| * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |↑(u i)|⁻¹)
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: case zero
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = zero
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

pp: case neg
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = neg
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

pp: case pos
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = pos
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
<;>

Goal state after:
case zero
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = zero
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

case neg
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = neg
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1

case pos
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
hi : w i = pos
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 1