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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
hM' : 0 ∉ M'
this : ⊥.IsMaximal
⊢ (comap (IsLocalization.map (Localization M') (quotientMap P C ⋯) ⋯) ⊥).IsMaximal

Tactic:
refine isMaximal_comap_of_isIntegral_of_isMaximal' _ ?_ ⊥

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
hM' : 0 ∉ M'
this : ⊥.IsMaximal
⊢ (IsLocalization.map (Localization M') (quotientMap P C ⋯) ⋯).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsJacobsonRing A
inst✝ : Algebra.FiniteType A B
⊢ IsJacobsonRing B

Tactic:
by
  obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
  exact isJacobsonRing_of_surjective ⟨f.toRingHom, hf⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ * s₂)

Tactic:
simpa using mul_mem (by simpa : _ ∈ NonUnitalSubsemiring.sumSq R) (by simpa)

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

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
B : P.InvariantForm
i j : ι
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ 2 * (B.form (P.root i)) (P.root j) = 0

Tactic:
simp [two_ne_zero]

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 < (B.posForm ri) rj ↔ 0 < 2 * (B.posForm ri) rj

Tactic:
by rw [mul_pos_iff_of_pos_left zero_lt_two]

Goal state after:
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 Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v x ≤ 1
hx' : v x < 1
⊢ v (1 + x) = v 1

Tactic:
apply map_add_eq_of_lt_left

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 Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v x ≤ 1
hx' : v x < 1
⊢ v x < v 1
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 Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v' x ≤ 1
hx' : v' x < 1
⊢ v' (1 + x) = v' 1

Tactic:
apply map_add_eq_of_lt_left

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 Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v' x ≤ 1
hx' : v' x < 1
⊢ v' x < v' 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v (x + -y) = v x

Tactic:
apply map_add_eq_of_lt_left

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v x < v (-y)
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
aux : finrank R M = finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R M ≤ finrank R ↥(P.rootSpan R) + finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
aux,

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
aux : finrank R M = finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator ≤
    finrank R ↥(P.rootSpan R) + finrank R ↥(LinearMap.ker P.RootForm)
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 : ι
c : R
hc : ∏ i, (P.RootForm (P.root i)) (P.root i) = (P.RootForm (P.root i)) (P.root i) * c
⊢ (∏ a, (P.RootForm (P.root a)) (P.root a)) • P.coroot i ∈ (P.Polarization.domRestrict (P.rootSpan R)).range

Tactic:
rw [hc, mul_comm, mul_smul, rootForm_self_smul_coroot]

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 : ι
c : R
hc : ∏ i, (P.RootForm (P.root i)) (P.root i) = (P.RootForm (P.root i)) (P.root i) * c
⊢ c • 2 • P.Polarization (P.root i) ∈ (P.Polarization.domRestrict (P.rootSpan R)).range
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case h
ι : 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✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
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 k (range ⇑root) = ⊤
i j : ι
⊢ coroot ((RootPairing.equiv_of_mapsTo p root coroot i hs hp) j) = (preReflection (coroot i) (p (root i))) (coroot j)

Tactic:
refine (coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)

Goal state after:
case h
ι : 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✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
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 k (range ⇑root) = ⊤
i j : ι
⊢ root ((RootPairing.equiv_of_mapsTo p root coroot i hs hp) j) = (preReflection (root i) (p.flip (coroot i))) (root j)
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : 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
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
this : Injective fun t ↦ x + t • y
aux : sxy = (fun t ↦ x + t • y) '' {t | t ≠ 0}
⊢ ENat.card K ≤ sxy.encard + 1

Tactic:
aux,

Goal state after:
ι : 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
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
this : Injective fun t ↦ x + t • y
aux : sxy = (fun t ↦ x + t • y) '' {t | t ≠ 0}
⊢ ENat.card K ≤ ((fun t ↦ x + t • y) '' {t | t ≠ 0}).encard + 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : (pi Q).Anisotropic
⊢ ∀ (i : ι), (Q i).Anisotropic

Tactic:
simp_rw [Anisotropic, pi_apply, funext_iff, Pi.zero_apply] at h

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
⊢ ∀ (i : ι), (Q i).Anisotropic
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inr
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
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
have hk : k = n + 2⁻¹ - chainTopCoeff α β := by simpa [sub_div, add_div] using H

Goal state after:
case inr.inr
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
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.inr.inl
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
hβ : β.IsNonZero
hα : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
cases hβ (by rwa [zero_smul] at h)

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
hβ : β.IsNonZero
⊢ (reflectRoot α β).IsNonZero

Tactic:
intro e
  have : β (coroot α) = 0 := by
    by_cases hα : α.IsZero
    · simp [coroot_eq_zero_iff.mpr hα]
    simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)
  have : reflectRoot α β = β := by ext; simp [reflectRoot, this]
  exact hβ (this ▸ e)

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
h' : H := g⁻¹ • h
⊢ (((ofMulAction k G H) g) f).coeff (g • h') = f.coeff h'

Tactic:
have hg : Function.Injective (g • · : H → H) := by
    intro h₁ h₂
    simp

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
h' : H := g⁻¹ • h
hg : Function.Injective fun x ↦ g • x
⊢ (((ofMulAction k G H) g) f).coeff (g • h') = f.coeff h'
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 : ι
this : P.root i ∈ span ℕ (⇑P.root '' ↑b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' ↑b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' ↑b.support)

Tactic:
rw [← span_span_of_tower (R := ℕ)]

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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' ↑b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' ↑b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' ↑b.support))
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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainTopCoeff i j = ⋯.choose.toNat
hp : ⋯.choose ≥ 0
h₂ : S = Icc ⋯.choose ⋯.choose
⊢ ↑n ∈ S ↔ n ≤ chainTopCoeff i j

Tactic:
aux,

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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainTopCoeff i j = ⋯.choose.toNat
hp : ⋯.choose ≥ 0
h₂ : S = Icc ⋯.choose ⋯.choose
⊢ ↑n ∈ S ↔ n ≤ ⋯.choose.toNat
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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainBotCoeff i j = (-⋯.choose).toNat
hq : ⋯.choose ≤ 0
p : ℤ
hp : p ≥ 0
h₂ : S = Icc ⋯.choose p
⊢ -↑n ∈ S ↔ n ≤ chainBotCoeff i j

Tactic:
aux,

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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainBotCoeff i j = (-⋯.choose).toNat
hq : ⋯.choose ≤ 0
p : ℤ
hp : p ≥ 0
h₂ : S = Icc ⋯.choose p
⊢ -↑n ∈ S ↔ n ≤ (-⋯.choose).toNat
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
b : Basis ↑(baseOf (⇑P.root) f) ℚ ↥(P.rootSpan ℚ) :=
  have this := ⋯;
  Basis.mk this ⋯
⊢ Nat.card ↑(baseOf (⇑P.root) f) = finrank ℚ ↥(P.rootSpan ℚ)

Tactic:
finrank_eq_nat_card_basis b

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
b : Basis ↑(baseOf (⇑P.root) f) ℚ ↥(P.rootSpan ℚ) :=
  have this := ⋯;
  Basis.mk this ⋯
⊢ Nat.card ↑(baseOf (⇑P.root) f) = Nat.card ↑(baseOf (⇑P.root) f)
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
inst✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ P.pairing i i = (algebraMap ℤ R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)

Tactic:
map_sum,

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R) (f x • P.pairingIn ℤ x i)
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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ (P.toLinearMap (∑ j ∈ b.support, f j • P.root j)) (P.coroot i) =
    ∑ x ∈ b.support, (algebraMap ℤ R) (f x • P.pairingIn ℤ x i)

Tactic:
map_sum,

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ (∑ x ∈ b.support, P.toLinearMap (f x • P.root x)) (P.coroot i) =
    ∑ x ∈ b.support, (algebraMap ℤ R) (f x • P.pairingIn ℤ x i)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a + b + c = a + (b + c)

Tactic:
apply ext_cauchy

Goal state after:
x a b c : ℝ
⊢ (a + b + c).cauchy = (a + (b + c)).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 0 + a = a

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (0 + a).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a + 0 = a

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (a + 0).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a + b = b + a

Tactic:
apply ext_cauchy

Goal state after:
x a b : ℝ
⊢ (a + b).cauchy = (b + a).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a * b * c = a * (b * c)

Tactic:
apply ext_cauchy

Goal state after:
x a b c : ℝ
⊢ (a * b * c).cauchy = (a * (b * c)).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 1 * a = a

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (1 * a).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a * 1 = a

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (a * 1).cauchy = a.cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 0 * a = 0

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (0 * a).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a * 0 = 0

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (a * 0).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a * (b + c) = a * b + a * c

Tactic:
apply ext_cauchy

Goal state after:
x a b c : ℝ
⊢ (a * (b + c)).cauchy = (a * b + a * c).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ (a + b) * c = a * c + b * c

Tactic:
apply ext_cauchy

Goal state after:
x a b c : ℝ
⊢ ((a + b) * c).cauchy = (a * c + b * c).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ { cauchy := ↑0 } = 0

Tactic:
apply ext_cauchy

Goal state after:
x : ℝ
⊢ { cauchy := ↑0 }.cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) } = { cauchy := ↑n } + 1

Tactic:
apply ext_cauchy

Goal state after:
x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) }.cauchy = ({ cauchy := ↑n } + 1).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ -a + a = 0

Tactic:
apply ext_cauchy

Goal state after:
x a : ℝ
⊢ (-a + a).cauchy = cauchy 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
z : ℕ
⊢ { cauchy := ↑(Int.negSucc z) } = -↑(z + 1)

Tactic:
apply ext_cauchy

Goal state after:
x : ℝ
z : ℕ
⊢ { cauchy := ↑(Int.negSucc z) }.cauchy = (-↑(z + 1)).cauchy