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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m₁ m₂ : M
⊢ (changeForm h) ((ι Q) m₁ * (ι Q) m₂) = (ι Q') m₁ * (ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)

Tactic:
changeForm_ι_mul,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m₁ m₂ : M
⊢ (ι Q') m₁ * (changeForm h) ((ι Q) m₂) - (contractLeft (B m₁)) ((changeForm h) ((ι Q) m₂)) =
    (ι Q') m₁ * (ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm ⋯) x✝ = x✝
⊢ (changeForm ⋯) ((ι Q) m✝ * x✝) = (ι Q) m✝ * x✝

Tactic:
changeForm_ι_mul,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm ⋯) x✝ = x✝
⊢ (ι Q) m✝ * (changeForm ⋯) x✝ - (contractLeft (0 m✝)) ((changeForm ⋯) x✝) = (ι Q) m✝ * x✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
have : IsDomain S := inferInstance

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (changeForm h') ((changeForm h) ((ι Q) m✝ * x✝)) = (changeForm ⋯) ((ι Q) m✝ * x✝)

Tactic:
changeForm_ι_mul,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (changeForm h') ((ι Q') m✝ * (changeForm h) x✝ - (contractLeft (B m✝)) ((changeForm h) x✝)) =
    (changeForm ⋯) ((ι Q) m✝ * x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (changeForm h') ((ι Q') m✝ * (changeForm h) x✝) - (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (changeForm ⋯) ((ι Q) m✝ * x✝)

Tactic:
changeForm_ι_mul,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm h') ((changeForm h) x✝) - (contractLeft (B' m✝)) ((changeForm h') ((changeForm h) x✝)) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (changeForm ⋯) ((ι Q) m✝ * x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm h') ((changeForm h) x✝) - (contractLeft (B' m✝)) ((changeForm h') ((changeForm h) x✝)) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (changeForm ⋯) ((ι Q) m✝ * x✝)

Tactic:
changeForm_ι_mul,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm h') ((changeForm h) x✝) - (contractLeft (B' m✝)) ((changeForm h') ((changeForm h) x✝)) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft ((B + B') m✝)) ((changeForm ⋯) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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
x : CliffordAlgebra Q
hx : x ∈ pinGroup Q
⊢ star x ∈ pinGroup Q

Tactic:
rw [mem_iff] at hx ⊢
  refine ⟨?_, Unitary.star_mem hx.2⟩
  rcases hx with ⟨⟨y, hy₁, hy₂⟩, _hx₂, hx₃⟩
  simp only [Subgroup.coe_toSubmonoid, SetLike.mem_coe] at hy₁
  simp only [Units.coeHom_apply] at hy₂
  simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]
  refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩
  rw [← hy₂] at hx₃
  have hy₃ : y * star y = 1 := by
    rw [← Units.val_inj]
    simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]
  apply_fun fun x => y⁻¹ * x at hy₃
  simp only [inv_mul_cancel_left, mul_one] at hy₃
  simp only [hy₃, hy₁, inv_mem_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ toDirectSum ((tprod R M n) x) = (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
tprod_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ toDirectSum (List.ofFn fun i ↦ (ι R) (x i)).prod = (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
h_inj : Injective v'
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ LinearIndependent L (⇑(Pi.algebraMap ι' R L) ∘ v)

Tactic:
have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' K L ∘ Pi.algebraMap ι' R K ∘ v := by
    ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
aux : ⇑(Pi.algebraMap ι' R L) ∘ v = ⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v
⊢ LinearIndependent L (⇑(Pi.algebraMap ι' R L) ∘ v)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).charpoly = M.charpoly

Tactic:
have h := FiniteField.Matrix.charpoly_pow_card M
  rwa [ZMod.card] at h

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ {x | ¬∃ j, f j = x}.card = Fintype.card ι - n

Tactic:
convert! Finset.card_compl {x | ∃ j, f j = x} using 2
    · exact (Finset.compl_filter _).symm
    · convert! (Finset.card_image_of_injective Finset.univ f.injective).symm <;> simp

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

Goal state before:
pp: α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0ᵀ D).IsDiag

Tactic:
exact ha.fromBlocks hd

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ swap R i j * swap R i j = 1

Tactic:
simp only [swap]
  rw [← Equiv.swap_inv, Equiv.Perm.inv_def]
  simp [← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_trans]

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

Goal state before:
pp: n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix n n R
⊢ A.Nonsingular ↔ A.det ≠ 0

Tactic:
nonsingular_iff_det_mem_nonZeroDivisors,

Goal state after:
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix n n R
⊢ A.det ∈ nonZeroDivisors R ↔ A.det ≠ 0
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Set (ℙ K V)
⊢ E ∈ SetLike.coe '' s → x ∈ E

Tactic:
rintro ⟨E, hE, rfl⟩

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ ↑E
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span ↑W ⊔ span S

Tactic:
span_coe

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = W ⊔ span S
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span S ⊔ span ↑W

Tactic:
span_coe

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span S ⊔ W
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier

Tactic:
mem_carrier_iff,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ span S ↔ x ∈ sInf {W | S ⊆ ↑W}
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
v✝ : V
h✝ : v✝ ≠ 0
⊢ v✝ ∈ s ↔ K ∙ v✝ ≤ s

Tactic:
Submodule.span_singleton_le_iff_mem

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
v✝ : V
h✝ : v✝ ≠ 0
⊢ v✝ ∈ s ↔ v✝ ∈ s
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD✝ : D ≠ D'
hE✝ : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet : LinearEquiv.det h = (LinearEquiv.det g)⁻¹
hD : h • D = D
hE : h • D' = D'
⊢ LinearEquiv.det (g * h) = 1

Tactic:
simp [hdet]

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ r • v = m • v

Tactic:
change _ = m.1 • v

Goal state after:
case h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ r • v = ↑m • v
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))).ker = Subgroup.center (Matrix.SpecialLinearGroup ι K)

Tactic:
by
  ext m
  simp only [MonoidHom.mem_ker, toPermHom_apply, Equiv.Perm.one_def, DFunLike.ext_iff, toPerm_apply,
    Equiv.refl_apply, Matrix.SpecialLinearGroup.mem_center_iff]
  refine ⟨fun hm ↦ ?_, fun ⟨r, hr1, hr2⟩ l ↦ ?_⟩
  · set f : (ι → K) →ₗ[K] ι → K := (Matrix.SpecialLinearGroup.toLin' m).toLinearMap with hf
    obtain ⟨a, ha⟩ := f.exists_eq_smul_id_of_forall_notLinearIndependent fun (v : ι → K) ↦ by
      by_cases hv : v = 0
      · simp [hv, linearIndependent_fin2]
      · simpa [LinearIndependent.pair_iff' hv, mk_eq_mk_iff'] using! hm (.mk K v hv)
    have hscalar : m.1 = Matrix.scalar ι a := calc
      m.1 = LinearMap.toMatrix' f := by
        rw [hf, Matrix.SpecialLinearGroup.toLin'_to_linearMap, LinearMap.toMatrix'_toLin']
      _ = (algebraMap K (Module.End K (ι → K)) a).toMatrix' := congrArg LinearMap.toMatrix' ha
      _ = Matrix.scalar ι a := LinearMap.toMatrix'_algebraMap a
    exact ⟨a, by simpa [hscalar] using m.2, hscalar.symm⟩
  · induction l using Projectivization.ind with | _ v hv =>
    simp only [smul_mk, mk_eq_mk_iff']
    use r
    change _ = m.1 • v
    simp [← hr2]

Goal state after:
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
⊢ ∀ (x : M), polar (⇑Q) n x = 0 x

Tactic:
← polarBilin_apply_apply,

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
⊢ ∀ (x : M), (Q.polarBilin n) x = 0 x
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
⊢ LinearIndependent R h

Tactic:
have : Matrix.diagLinearMap (b.support ⊕ ι) R R ∘ h =
      Sum.elimZeroLeft ∘ fun i : b.support ↦ algebraMap ℤ R ∘ (P.pairingIn ℤ · i) := by
    ext; rw [comp_apply, h_def]; aesop

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ LinearIndependent R h
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ ⟨⟨x, property✝⟩, hx⟩ ∈ span R (range h')

Tactic:
← SetLike.mem_coe,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
this : x ∈ map g (span R (range h'))
⊢ ⟨⟨x, property✝⟩, hx⟩ ∈ ↑(span R (range h'))
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
n✝ : ℕ
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
n : ℕ
⊢ (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)

Tactic:
pow_succ',

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
n✝ : ℕ
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
n : ℕ
⊢ (e i * e i ^ n).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * (x * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)

Tactic:
nth_rw 1 [← mul_one x]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * (x * 1 * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i

Tactic:
by
  classical
  suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this
  calc ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
                      _ = -(h j * e i - e i * h j) * ω b := ?_
                      _ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
                      _ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
                      _ = ω b * (-b.cartanMatrix i j • f i) := ?_
  · rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
    abel
  · rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]

Goal state after: