mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝³ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝² : (comap (algebraMap S Sₘ) I).IsPrime
this✝¹ : (comap φ' I).IsPrime
this✝ : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this : (comap φ' I).IsMaximal
⊢ (comap (algebraMap S Sₘ) I).IsMaximal

Tactic:
have := ((IsLocalization.isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝⁴ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝³ : (comap (algebraMap S Sₘ) I).IsPrime
this✝² : (comap φ' I).IsPrime
this✝¹ : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this✝ : (comap φ' I).IsMaximal
this : (under R (comap φ' I)).IsMaximal
⊢ (comap (algebraMap S Sₘ) I).IsMaximal
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ v₁ x ≤ 1 ↔ v₂ x ≤ 1

Tactic:
rw [← v₁.map_one, h, map_one]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ 1 ≤ v₁ x ↔ 1 ≤ v₂ x

Tactic:
rw [← v₁.map_one, h, map_one]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i : ι
x : ↥(P.corootSpan S)
⊢ (algebraMap S R) ((P.root'In S i) x) = (P.root' i) ↑x

Tactic:
by
  rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hc' : P₁.coroot = P₂.coroot
⊢ P₁.reflectionPerm = P₂.reflectionPerm

Tactic:
ext i j

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hc' : P₁.coroot = P₂.coroot
i j : ι
⊢ (P₁.reflectionPerm i) j = (P₂.reflectionPerm i) j
Module: Mathlib.LinearAlgebra.RootSystem.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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
x✝ : M
⊢ (preReflection (sα β) (p.flip (sα' β'))) x✝ = (sα ∘ₗ sβ ∘ₗ sα) x✝

Tactic:
have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
x✝ : M
hpi : (p.flip (coroot i)) (root i) = 2
⊢ (preReflection (sα β) (p.flip (sα' β'))) x✝ = (sα ∘ₗ sβ ∘ₗ sα) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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✝ : Fintype ι
i : ι
⊢ (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i

Tactic:
LinearMap.smul_apply,

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✝ : Fintype ι
i : ι
⊢ 4 • (P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_2
ι : 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
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i = P.root j ∨ P.root i = -P.root j

Tactic:
rcases eq_or_ne i j with rfl | h'
    · tauto
    · exact Or.inr (h i j h' hLin)

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
⊢ finrank R (Dual R N) = finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator

Tactic:
← P.finrank_corootSpan_eq',

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
⊢ finrank R (Dual R N) = finrank R ↥(P.corootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
aux0 : finrank R ↥(P.corootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator = finrank R N
aux1 : finrank R ↥(P.rootSpan R) + finrank R ↥(LinearMap.ker P.RootForm) = finrank R M
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥(P.corootSpan R).dualAnnihilator

Tactic:
← P.finrank_corootSpan_eq',

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
aux0 : finrank R ↥(P.corootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator = finrank R N
aux1 : finrank R ↥(P.corootSpan R) + finrank R ↥(LinearMap.ker P.RootForm) = finrank R M
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥(P.corootSpan R).dualAnnihilator
Module: Mathlib.LinearAlgebra.RootSystem.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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
x✝ : M
⊢ (preReflection (sα β) (p.flip (sα' β'))) x✝ = (sα ∘ₗ sβ ∘ₗ sα) x✝

Tactic:
have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
x✝ : M
hpi : (p.flip (coroot i)) (root i) = 2
⊢ (preReflection (sα β) (p.flip (sα' β'))) x✝ = (sα ∘ₗ sβ ∘ₗ sα) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
h : P.corootSpan R = ⊤
⊢ finrank R ↥(P.rootSpan R) = finrank R M

Tactic:
← P.finrank_corootSpan_eq',

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
h : P.corootSpan R = ⊤
⊢ finrank R ↥(P.corootSpan R) = finrank R M
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert.inr.inl
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
hx : 0 ∈ p j
⊢ 0 ∈ ⋃ i ∈ s, ↑(p i)

pp: case insert.inr.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ x ∈ ⋃ i ∈ s, ↑(p i)

Tactic:
· simpa using! hs

Goal state after:
case insert.inr.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ x ∈ ⋃ i ∈ s, ↑(p i)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥

Tactic:
by
  by_cases hα : α.IsZero
  · simpa only [hα.eq, smul_zero, neg_zero, chainTop_zero, zero_add, ne_eq] using! β.2
  obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero
  obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα
  obtain rfl := isSl2.h_eq_coroot hα he hf
  have prim : isSl2.HasPrimitiveVectorWith x (chainLength α β : K) :=
    have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
    ⟨x_ne0, (chainLength_smul _ _ hx).symm, by rwa [genWeightSpace_add_chainTop _ _ hα] at this⟩
  simp only [← smul_neg, ne_eq, LieSubmodule.eq_bot_iff, not_forall]
  exact ⟨_, toEnd_pow_apply_mem hf hx n, prim.pow_toEnd_f_ne_zero_of_eq_nat rfl hn⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ (a • p.1) (a • p.2) = (a * a) • p.1 p.2

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a • p.1 (a • p.2) = (a * a) • p.1 p.2
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p + q).1 (p + q).2 = p.1 p.2 + q.1 q.2 + ((LinearMap.dualProd R M) p) q

Tactic:
LinearMap.dualProd_apply_apply,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p + q).1 (p + q).2 = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p.1 + q.1) (p + q).2 = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)

Tactic:
Prod.snd_add,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ (p.1 + q.1) (p.2 + q.2) = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
⊢ (g.weightMap ∘ₗ f.weightMap).dualMap ∘ₗ ↑P₂.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ f.coweightMap ∘ₗ g.coweightMap

Tactic:
ext φ x
    rw [← LinearMap.dualMap_comp_dualMap, ← LinearMap.comp_assoc _ f.coweightMap,
      ← f.weight_coweight_transpose, LinearMap.comp_assoc g.coweightMap,
      ← g.weight_coweight_transpose, ← LinearMap.comp_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
intro r f w

Goal state after:
case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r✝ : k[G]
m : RestrictScalars k k[G] M
r : k
f : k[G]
w :
  ((ofModule M).asAlgebraHom f) m = (RestrictScalars.addEquiv k k[G] M).symm (f • (RestrictScalars.addEquiv k k[G] M) m)
⊢ ((ofModule M).asAlgebraHom (r • f)) m =
    (RestrictScalars.addEquiv k k[G] M).symm ((r • f) • (RestrictScalars.addEquiv k k[G] M) m)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : ↑P.flip.toPerfPair ∘ₗ f.coweightMap = ↑P.flip.toPerfPair ∘ₗ g.coweightMap
⊢ f.weightMap x = g.weightMap x

Tactic:
rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h

Goal state after:
case weightMap
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.flip.toPerfPair = g.weightMap.dualMap ∘ₗ ↑P.flip.toPerfPair
⊢ f.weightMap x = g.weightMap x
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ P.root j ∈ ↑(ker (P.coroot' k))

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, P.root_coroot'_eq_pairing, P.pairing_eq_zero_iff',
        ← P.root_coroot'_eq_pairing]

Goal state after:
case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ (P.coroot' j) (P.root k) = 0
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
⊢ symm P P e * e = 1

Tactic:
by
    ext m
    · rw [← weightEquiv_apply]
      simp
    · rw [← coweightEquiv_apply]
      simp
    · simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
by
  refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp
    (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)
  simpa [← P.algebraMap_pairingIn ℤ] using P.pairing_eq_zero_iff' (i := i) (j := j)

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
i j : ↥b.support
hij : i ≠ j
⊢ LinearIndependent R ![P.root ↑i, P.root ↑j]

Tactic:
by
  have : ({(j : ι), (i : ι)} : Set ι) ⊆ b.support := by simp [pair_subset_iff]
  rw [← linearIndepOn_id_range_iff (by simp_all)]
  simpa [image_pair] using LinearIndepOn.id_image <| b.linearIndepOn_root.mono this

Goal state after: