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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) •
          { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))

Tactic:
;

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } j))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) •
          { toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
          { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))

Tactic:
;

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
          { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
⊢ f.Finite

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
⊢ f.Finite
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : DivisionRing L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
⊢ Module.Finite K L

Tactic:
by
  obtain ⟨m, hm⟩ := Ideal.exists_maximal A
  let := Ideal.Quotient.field m
  have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
  exact Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap
    (RingHom.injective _)

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✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i j k l : ι
x y : S
h : P.root k = (algebraMap S R) x • P.root i + (algebraMap S R) y • P.root l
⊢ (algebraMap S R) (P.pairingIn S k j) = (algebraMap S R) (x • P.pairingIn S i j + y • P.pairingIn S l j)

Tactic:
simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using
    pairing_eq_add_of_root_eq_smul_add_smul h

Goal state after:
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w✝ : R
⊢ IsSumSq (w✝ * w✝ + s)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w✝ : R
⊢ IsSumSq (w✝ * w✝ + s)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : NonUnitalCommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}

Tactic:
;

Goal state after:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : CommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}

Tactic:
;

Goal state after:
T : Type u_2
inst✝ : CommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
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 M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
x✝ : R
⊢ x✝ ∈ range ⇑(algebraMap S R) ↔ x✝ ∈ ↑(Algebra.linearMap S R).range

Tactic:
;

Goal state after:
ι : 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 M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
x✝ : R
⊢ x✝ ∈ range ⇑(algebraMap S R) ↔ x✝ ∈ ↑(Algebra.linearMap S R).range
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 M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
⊢ (P.coroot' i) x ∈ ↑(Algebra.linearMap S R).range

Tactic:
induction hx using Submodule.span_induction with

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✝ : Module S M
i : ι
⊢ ↑(P.rootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.rootSpanMem S i)

Tactic:
;

Goal state after:
ι : 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✝ : Module S M
i : ι
⊢ ↑(P.rootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.rootSpanMem S i)
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✝ : Module S N
i : ι
⊢ ↑(P.corootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.corootSpanMem S i)

Tactic:
;

Goal state after:
ι : 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✝ : Module S N
i : ι
⊢ ↑(P.corootSpanMem S ((P.reflectionPerm i) i)) = ↑(-P.corootSpanMem S i)
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
i : ι
x : M
hx : x ∈ span R (range ⇑P.root)
⊢ x ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
induction hx using Submodule.span_induction with

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
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(⨅ i, LinearMap.ker (P.root' i))

Tactic:
;

Goal state after:
ι : 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
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(⨅ i, LinearMap.ker (P.root' i))
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
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(span R (range P.root')).dualCoannihilator

Tactic:
;

Goal state after:
ι : 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
x✝ : N
⊢ x✝ ∈ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) ↔
    x✝ ∈ ↑(span R (range P.root')).dualCoannihilator
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_7
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
i j : ι
⊢ (algebraMap S R) (P.coxeterWeightIn S i j) = P.coxeterWeight i j

Tactic:
simp [coxeterWeightIn, coxeterWeight]

Goal state after:
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 ι
x✝¹ x✝ : M
⊢ ((P.flip.toLinearMap ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) x✝

Tactic:
;

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 ι
x✝¹ x✝ : M
⊢ ((P.flip.toLinearMap ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) 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 ι
x✝ : M
⊢ x✝ ∈ P.Polarization.ker ↔ x✝ ∈ LinearMap.ker P.RootForm

Tactic:
;

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 ι
x✝ : M
⊢ x✝ ∈ P.Polarization.ker ↔ x✝ ∈ LinearMap.ker P.RootForm
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 := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
this✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.flip ∘ ⇑coroot))
⊢ (span R (range ⇑root)).subtype.dualMap ((⇑p.flip ∘ ⇑coroot) k) =
    (span R (range ⇑root)).subtype.dualMap ((⇑p.flip ∘ ⇑coroot) l)

Tactic:
refine Dual.eq_of_preReflection_mapsTo' (finite_range root)
    (Submodule.subset_span <| mem_range_self k) (hp k) (hr k) hkl ?_

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 α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
this✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.flip ∘ ⇑coroot))
⊢ MapsTo (⇑(preReflection (root k) ((⇑p.flip ∘ ⇑coroot) l))) (range ⇑root) (range ⇑root)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE

Tactic:
tfae_have 1 ↔ 3 := isEquiv_iff_val_le_one

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
tfae_1_iff_3 : v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
tfae_1_iff_3 : v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
tfae_1_iff_4 : v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
tfae_1_iff_5 : v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE

Tactic:
tfae_have 1 ↔ 6 := isEquiv_iff_val_sub_one_lt_one

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
tfae_1_iff_3 : v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
tfae_1_iff_4 : v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
tfae_1_iff_5 : v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1
tfae_1_iff_6 : v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ 1 ∈ ⊤

Tactic:
;

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ 1 ∈ ⊤
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 j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ 4 • (P.RootForm (P.root i)) (P.root j) * (P.RootForm (P.root i)) (P.root j) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
hij,

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 j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i)) * (P.RootForm (P.root i)) (P.root j) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
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
x✝ : M
⊢ x✝ ∈ P.RootForm.orthogonal ⊤ → x✝ ∈ P.RootForm.orthogonal (P.rootSpan R)

Tactic:
;

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
x✝ : M
⊢ x✝ ∈ P.RootForm.orthogonal ⊤ → x✝ ∈ P.RootForm.orthogonal (P.rootSpan R)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_1
ι : 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✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : P.root i + P.root j ∈ range ⇑P.root
hij : i = j
⊢ False

Tactic:
hij,

Goal state after:
case refine_1
ι : 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✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : P.root j + P.root j ∈ range ⇑P.root
hij : i = j
⊢ False
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
inst✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : P.root i + P.root j ∈ range ⇑P.root
hij : P.root i = -P.root j
⊢ 0 ∈ range ⇑P.root

Tactic:
hij,

Goal state after:
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
inst✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : -P.root j + P.root j ∈ range ⇑P.root
hij : P.root i = -P.root j
⊢ 0 ∈ range ⇑P.root
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
x y : M
hx : ∀ n ∈ P.rootSpan R, (P.RootForm n) x = 0
⊢ y ∈ ⊤

Tactic:
;

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
x y : M
hx : ∀ n ∈ P.rootSpan R, (P.RootForm n) x = 0
⊢ y ∈ ⊤