mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
by_cases h : x = 0

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * ↑u ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n ∈ maximalIdeal R ^ n

Tactic:
apply Ideal.pow_mem_pow

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * ↑u ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ∈ maximalIdeal R
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 y : R
⊢ v₁ x < v₁ y ↔ v₂ x < v₂ y

Tactic:
by
  rw [← le_iff_le_iff_lt_iff_lt, h]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ (algebraMap A (FractionRing A)) z = (algebraMap A (FractionRing A)) ↑⟨y, y_mem⟩ * x

Tactic:
rw [hz, ← Algebra.smul_def]

Goal state after:
case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inl
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : (ofClass v).ValueGroup₀
h✝ : x = 0
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x

pp: case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)) =
    ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)

Tactic:
· simp_all [valueGroup₀Fun_zero]

Goal state after:
case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)) =
    ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inl
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : (ofClass w).ValueGroup₀
h✝ : x = 0
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x

pp: case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass w) r₁ ≠ 0
hs₁ : (ofClass w) s₁ ≠ 0
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun ↑(valueGroup.mk (ofClass w) r₁ s₁ hr₁ hs₁)) =
    ↑(valueGroup.mk (ofClass w) r₁ s₁ hr₁ hs₁)

Tactic:
· simp_all [valueGroup₀Fun_zero]

Goal state after:
case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass w) r₁ ≠ 0
hs₁ : (ofClass w) s₁ ≠ 0
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun ↑(valueGroup.mk (ofClass w) r₁ s₁ hr₁ hs₁)) =
    ↑(valueGroup.mk (ofClass w) r₁ s₁ hr₁ hs₁)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inl
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
h✝ : x = 0
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y

pp: case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
y : (ofClass v).ValueGroup₀
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
⊢ h.valueGroup₀Fun (↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * y) =
    h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * h.valueGroup₀Fun y

Tactic:
· simp_all [valueGroup₀Fun_zero]

Goal state after:
case inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
y : (ofClass v).ValueGroup₀
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
⊢ h.valueGroup₀Fun (↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * y) =
    h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * h.valueGroup₀Fun y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr.inl
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
y : (ofClass v).ValueGroup₀
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
h✝ : y = 0
⊢ h.valueGroup₀Fun (↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * y) =
    h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * h.valueGroup₀Fun y

pp: case inr.inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
r₂ s₂ : R
hr₂ : (ofClass v) r₂ ≠ 0
hs₂ : (ofClass v) s₂ ≠ 0
⊢ h.valueGroup₀Fun (↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * ↑(valueGroup.mk (ofClass v) r₂ s₂ hr₂ hs₂)) =
    h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) *
      h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₂ s₂ hr₂ hs₂)

Tactic:
· simp_all [valueGroup₀Fun_zero]

Goal state after:
case inr.inr
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : (ofClass v) r₁ ≠ 0
hs₁ : (ofClass v) s₁ ≠ 0
r₂ s₂ : R
hr₂ : (ofClass v) r₂ ≠ 0
hs₂ : (ofClass v) s₂ ≠ 0
⊢ h.valueGroup₀Fun (↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) * ↑(valueGroup.mk (ofClass v) r₂ s₂ hr₂ hs₂)) =
    h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₁ s₁ hr₁ hs₁) *
      h.valueGroup₀Fun ↑(valueGroup.mk (ofClass v) r₂ s₂ hr₂ hs₂)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
⊢ I.jacobson = I

Tactic:
let i : R →+* R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
⊢ I.jacobson = I
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : R
hs : IsSumSq s
⊢ 0 ≤ s

Tactic:
induction hs using IsSumSq.rec' with
  | zero          => simp
  | sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h

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

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : v.restrict a = 0
⊢ h.orderMonoidIso (v.restrict a) = w.restrict a

Tactic:
ha,

Goal state after:
case pos
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : v.restrict a = 0
⊢ h.orderMonoidIso 0 = w.restrict a
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α β
⊢ coroot k = (preReflection α' (p α)) β'

Tactic:
set sβ := preReflection β (p.flip β')

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 β')
⊢ coroot k = (preReflection α' (p α)) β'
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

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
⊢ P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j

Tactic:
by
  rw [isReduced_iff]
  refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin  ↦ ?_⟩
  · specialize h i j hLin
    simp_all
  · 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.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α β
⊢ coroot k = (preReflection α' (p α)) β'

Tactic:
set sβ := preReflection β (p.flip β')

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 β')
⊢ coroot k = (preReflection α' (p α)) β'
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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : LinearOrder S
inst✝⁶ : IsStrictOrderedRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i✝ j✝ i j : ι
⊢ (algebraMap S R) (∑ k, P.pairingIn S i k * P.pairingIn S j k) = (P.RootForm (P.root i)) (P.root j)

Tactic:
by simp [rootForm_apply_apply]

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∑ i ∈ s with 0 < c i, c i • v i = -∑ x ∈ s with 0 < -c x, c x • v x

Tactic:
← add_eq_zero_iff_eq_neg

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∑ i ∈ s with 0 < c i, c i • v i + ∑ x ∈ s with 0 < -c x, c x • v x = 0
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddAbove x✝
⊢ IsLUB x✝ (if h : x✝.Nonempty ∧ BddAbove x✝ then ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) else 0)

Tactic:
dif_pos ⟨hn, hb⟩

Goal state after:
x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddAbove x✝
⊢ IsLUB x✝ ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯)
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddBelow x✝
⊢ IsGLB x✝ (if h : x✝.Nonempty ∧ BddBelow x✝ then ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) else 0)

Tactic:
dif_pos ⟨hn, hb⟩

Goal state after:
x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddBelow x✝
⊢ IsGLB x✝ ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯)
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 ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
set lj := (P.posRootForm S).rootLength 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
P : RootPairing ι R M N
inst✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
⊢ P.coxeterWeightIn S i j ≤ 4
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i

Tactic:
hij'

Goal state after:
case inl.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl.inr.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i

Tactic:
hij'

Goal state after:
case inl.inr.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl.inr.inr.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i

Tactic:
hij'

Goal state after:
case inl.inr.inr.inl
ι : 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
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i