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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a

Tactic:
exact this.symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2

Tactic:
classical
  refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := H.total (Ideal.span {a}) (Ideal.span {b})
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm

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

Goal state before:
pp: case mpr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ min 1 γ
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
rcases min_cases 1 γ with ⟨h, h'⟩ | ⟨h, h'⟩

Goal state after:
case mpr.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ min 1 γ
h : min 1 γ = 1
h' : 1 ≤ γ
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ min 1 γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ (Ideal.map (algebraMap R S) I).IsMaximal

Tactic:
by
  rw [isMaximal_iff_isMaximal_disjoint S y, under_map_of_isPrime_disjoint (powers y) S hI.isPrime]
  · exact ⟨hI, hy⟩
  · rwa [disjoint_powers_iff_notMem_of_isPrime]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ∀ (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
r

Goal state after:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
⊢ C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
    C r * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})
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✝³ : 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.valueGroup₀Fun x ≤ h.valueGroup₀Fun y ↔ x ≤ y

Tactic:
simp only [valueGroup₀Fun, ne_eq]

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✝³ : 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₀
⊢ ((if h : x = 0 then 0 else ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯)) ≤
      if h : y = 0 then 0 else ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯)) ↔
    x ≤ y
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ Flat R M

Tactic:
by
  rw [IsDedekindDomain.flat_iff_torsion_eq_bot, ← Submodule.isTorsionFree_iff_torsion_eq_bot]
  infer_instance

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✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S R N
x : M
hx : x ∈ P.rootSpan S
y : N
hy : y ∈ P.corootSpan S
⊢ ∀ x ∈ range ⇑P.root,
    ∀ y ∈ range ⇑P.coroot,
      ((LinearMap.restrictScalarsₗ S R N R S ∘ₗ ↑S P.toLinearMap) x) y ∈ (Algebra.linearMap S R).range

Tactic:
simpa using RootPairing.exists_value

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < P.pairingIn S i j * (B.posForm rj) rj ↔ 0 < P.pairingIn S i j

Tactic:
mul_pos_iff_of_pos_right (B.zero_lt_posForm_apply_root j)

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S i 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✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
⊢ (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i) • P.coroot k =
    m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j

Tactic:
let lsq (i) : R := B.form (P.root i) (P.root i)

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✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
⊢ (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i) • P.coroot k =
    m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j
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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ (P.Polarization.domRestrict (P.rootSpan R)) x ∈ P.corootSpan R

Tactic:
LinearMap.domRestrict_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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ P.Polarization ↑x ∈ P.corootSpan R
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 ι
x : ↥(span S (range ⇑P.root))
⊢ 0 ≤ ((P.posRootForm S).posForm x) x

Tactic:
obtain ⟨s, _, hs⟩ := P.exists_ge_zero_eq_rootForm S x.1 x.2
  have : s = (P.posRootForm S).posForm x x :=
    FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs
  rwa [← this]

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✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan R
hx' : (P.RootForm x) x = 0
this : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm
⊢ x = 0

Tactic:
simpa [P.disjoint_rootSpan_ker_rootForm.eq_bot] using this

Goal state after:
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 α β
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ genWeightSpace L (⇑α + ⇑(chainTop (⇑α) β))
⊢ ⁅e, x⁆ = 0

Tactic:
rwa [genWeightSpace_add_chainTop _ _ hα] at this

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

Goal state before:
pp: case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic

Tactic:
rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩

Goal state after:
case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic
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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
this : ⁅e, x⁆ ∈ genWeightSpace L (⇑α + ⇑(chainTop (⇑α) 0))
⊢ ⁅e, x⁆ = 0

Tactic:
rwa [genWeightSpace_add_chainTop _ _ hα] at this

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
g : G
x : H
r : k
⊢ ((ofMulAction k G H) g) (MonoidAlgebra.single x r) = MonoidAlgebra.single (g • x) r

Tactic:
by simp [ofMulAction_def]

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

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✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p

Tactic:
have hS₀ : 0 ∈ S := by simp [S]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case 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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : ↑1 * t = 1
ht : ↑1 • P.coroot i ∈ range ⇑P.coroot
hw : ↑w * ↑1 = 1
this : ↑1 * ↑w = 1
⊢ t = 1 ∨ t = -1

Tactic:
left; simpa using hz

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

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✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2

Tactic:
apply algebraMap_injective ℤ R

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := ⋯
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ (algebraMap ℤ R) (P.pairingIn ℤ k i) = (algebraMap ℤ R) (P.pairingIn ℤ j i + r * 2)
Module: Mathlib.LinearAlgebra.RootSystem.Chain

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✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2

Tactic:
apply algebraMap_injective ℤ R

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := ⋯
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ (algebraMap ℤ R) (P.pairingIn ℤ l i) = (algebraMap ℤ R) (P.pairingIn ℤ j i + s * 2)
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))

Tactic:
have h' : ¬ LinearIndependent R ![P.root i, P.root (-j)] := by simpa
    simp only [chainTopCoeff_of_not_linearIndependent h, chainTopCoeff_of_not_linearIndependent h',
      chainBotCoeff_of_not_linearIndependent h, chainBotCoeff_of_not_linearIndependent h']

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
⊢ span ℤ (P.rootSpanMem ℤ '' ↑b.support) = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun ⟨x, hx⟩ ↦ ?_
  rw [← SetLike.mem_coe, ← (injective_subtype (P.rootSpan ℤ)).mem_set_image, ← Submodule.map_coe]
  simpa [Submodule.map_span, ← image_comp]

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

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✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
⊢ chainTopCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ range ⇑P.root

Tactic:
by
  rw [← chainBotCoeff_reflectionPerm_left]
  simp [-chainBotCoeff_reflectionPerm_left, chainBotCoeff_eq_zero_iff]

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root (chainBotIdx i j) = P.root j - chainBotCoeff i j • P.root i

Tactic:
· simp only [chainBotIdx, chainBotCoeff, h, reduceDIte, zero_smul, sub_zero]

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
inst✝ : CharZero R
i : ι
hi : i ∈ b.support
⊢ b.height i = 1

Tactic:
have : P.root i = ∑ j ∈ b.support, (Pi.single i 1 : ι → ℤ) j • P.root j := by
    rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]; simp

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
b : P.Base
inst✝ : CharZero R
i : ι
hi : i ∈ b.support
this : P.root i = ∑ j ∈ b.support, Pi.single i 1 j • P.root j
⊢ b.height i = 1
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
inst✝ : CharZero R
i j k : ι
hi : b.IsPos i
hj : j ∈ b.support
hk : P.root k = P.root i - P.root j
⊢ b.IsPos k

Tactic:
by
  rw [isPos_iff] at hi
  rw [isPos_iff', b.height_sub hk, height_one_of_mem_support hj]
  lia

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

Goal state before:
pp: A : Type u_5
inst✝³ : CommRing A
inst✝² : IsDomain A
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι A
⊢ (toBilin' M).Nondegenerate ↔ M.det ≠ 0

Tactic:
rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]

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
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
contra : i = -j
⊢ False

Tactic:
rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi

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
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
hi : 0 < -1
contra : i = -j
⊢ False
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
⊢ 0 < mk f ↔ f.Pos

Tactic:
rw [← mk_zero, mk_lt]

Goal state after:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
A : Matrix n n α
d e : n → α
⊢ diagonal d ⊙ A = diagonal e ↔ d * A.diag = e

Tactic:
simp [diagonal_hadamard, diagonal_eq_diagonal_iff, funext_iff]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹

Tactic:
inv_pow'

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ n)⁻¹ = (A ^ n)⁻¹