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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v 1 ≤ 1

Tactic:
v.map_one

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ 1 ≤ 1
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
⊢ ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Tactic:
simp_rw [← funext (incl_apply _ _ _), map_sum]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, Irreducible ϖ

Tactic:
irreducible_iff_uniformizer

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, maximalIdeal R = span {ϖ}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hq : q ≠ 0
hQ2 : Irreducible q
⊢ R ∙ q = maximalIdeal R

Tactic:
irreducible_iff_uniformizer

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hq : q ≠ 0
hQ2 : maximalIdeal R = span {q}
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b

Tactic:
irreducible_iff_uniformizer

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ Associated a b
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m

Tactic:
simp only [mkQ_apply]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) (Submodule.Quotient.mk (↑f n)) = Submodule.Quotient.mk (↑f m)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x✝ y✝ : 𝒪
hab : (algebraMap 𝒪 K) x✝ = (algebraMap 𝒪 K) y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
simpa using hab

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ x m✝ ≡ x n✝ [SMOD I ^ m✝ • ⊤]

Tactic:
by rw [SModEq, hx, ← u.2 hmn, ← hx]; simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : ↑x m ∈ I ^ n • ⊤
⊢ (Submodule.factorPow I M m_ge) (↑x m) = 0

Tactic:
Submodule.factorPow,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : ↑x m ∈ I ^ n • ⊤
⊢ (Submodule.factor ⋯) (↑x m) = 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
⊢ Injective toMonoidWithZeroHom

Tactic:
rintro ⟨f, _⟩ g hfg; congr!

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ (under R J).IsMaximal ∧ y ∉ under R J → J.IsMaximal

Tactic:
simp only [Ideal.mem_comap, and_imp]
    exact (fun _ _ ↦ IsMaximal.of_isLocalization_of_disjoint (powers y))

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal
tfae_4_to_2 : (nilradical R).IsMaximal → ∃! I, I.IsPrime
⊢ (∃! I, I.IsPrime) → KrullDimLE 0 R ∧ IsLocalRing R

Tactic:
rintro ⟨P, hP₁, hP₂⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal
tfae_4_to_2 : (nilradical R).IsMaximal → ∃! I, I.IsPrime
P : Ideal R
hP₁ : P.IsPrime
hP₂ : ∀ (y : Ideal R), (fun I ↦ I.IsPrime) y → y = P
⊢ KrullDimLE 0 R ∧ IsLocalRing R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v

Tactic:
rcases h with h | h

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0
⊢ u = v

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ y * quotient x y + remainder x y = x

Tactic:
by
    rw [remainder, quotient]
    split_ifs with h₁ h₂ h₂
    · rw [h₁, zero_dvd_iff] at h₂; rw [h₁, h₂]; ring
    · rw [h₁]; ring
    · rw [← h₂.choose_spec]; ring
    · ring

Goal state after:
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 Γ₀
x y : R
hxy : v (x * y) = 0
⊢ v x = 0 ∨ v y = 0

Tactic:
v.map_mul x y

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 Γ₀
x y : R
hxy : v x * v y = 0
⊢ v x = 0 ∨ v y = 0
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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ by simp [h]⟩
  have : ¬ LinearIndependent R ![P.root i, P.root j] := by
    rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; norm_num
  replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
  exact P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ 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
⊢ chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β = chainLength α β

Tactic:
by
  rw [add_comm, chainBotCoeff_add_chainTopCoeff]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Q ((LinearMap.proj i).toFun m) = (pi (Pi.single i Q)) m

Tactic:
by
    dsimp
    rw [pi_apply, Fintype.sum_eq_single i (fun j hij => ?_), Pi.single_eq_same]
    rw [Pi.single_eq_of_ne hij, zero_apply]

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

Goal state before:
pp: case pos
ι : 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 : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : j = i
⊢ (Q j) (Pi.single i x j) = 0

pp: case neg
ι : 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 : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
· subst hji; rw [Pi.single_eq_same, hx]

Goal state after:
case neg
ι : 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 : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ (Q j) (Pi.single i x j) = 0
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
H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
n : ℕ
hn : chainLength α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
apply_fun (· / 2) at H
    rw [hn, smul_eq_mul] at H
    have hk : k = n + 2⁻¹ - chainTopCoeff α β := by simpa [sub_div, add_div] using H
    have := (rootSpace_zsmul_add_ne_bot_iff α β hα (chainTopCoeff α β - n)).mpr ?_
    swap
    · simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg, neg_sub, true_and]
      rw [← Nat.cast_add, chainBotCoeff_add_chainTopCoeff, hn]
      lia
    rw [h, hk, ← Int.cast_smul_eq_zsmul K, ← add_smul] at this
    simp only [Int.cast_sub, Int.cast_natCast,
      sub_add_sub_cancel', add_sub_cancel_left, ne_eq] at this
    cases this (rootSpace_one_div_two_smul α hα)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g h : P.End
⊢ MulOpposite.op (g * h).coweightMap = MulOpposite.op g.coweightMap * MulOpposite.op h.coweightMap

Tactic:
simp only [← MulOpposite.op_mul, coweightMap_mul, Module.End.mul_eq_comp]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
⊢ (↑e).weightMap ((weightEquiv P Q e).symm m) = m

Tactic:
rw [← weightEquiv_apply]
  exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
A : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module k A
G : Type u_4
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
⊢ (ofDistribMulAction k G A).norm x = ∑ g, g • x

Tactic:
by
  simp [norm]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: G M : Type
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : Additive M
⊢ Additive.toMul ((ofMulDistribMulAction G M).norm x) = ∏ g, g • Additive.toMul x

Tactic:
by
  simp [norm]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
i j : ↥b.support
hij : i ≠ j
⊢ LinearIndependent R ![P.root ↑i, P.root ↑j]

Tactic:
have : ({(j : ι), (i : ι)} : Set ι) ⊆ b.support := by simp [pair_subset_iff]

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 j : ↥b.support
hij : i ≠ j
this : {↑j, ↑i} ⊆ ↑b.support
⊢ LinearIndependent R ![P.root ↑i, P.root ↑j]
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]
⊢ ↑(chainTopCoeff i j) = sSup {k | P.root j + k • P.root i ∈ range ⇑P.root}

Tactic:
by
  rw [setOfPred_root_add_zsmul_mem_eq_Icc h]
  simp

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairingIn ℤ j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : 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]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
⊢ chainBotCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ range ⇑P.root

Tactic:
simp only [h, not_true_eq_false, false_or, this, Iic_chainBotCoeff_eq h, Set.ext_iff,
    mem_ofPred_eq, mem_singleton_iff]

Goal state after:
case pos
ι : 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]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
⊢ (∀ (x : ℕ), P.root j - x • P.root i ∈ range ⇑P.root ↔ x = 0) ↔ P.root j - P.root i ∉ range ⇑P.root
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
⊢ P.root i = ∑ j ∈ b.support, Pi.single i 1 j • P.root j

Tactic:
rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]

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
⊢ P.root i = Pi.single i 1 i • P.root i
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
⊢ mk (if h : f.LimZero then 0 else f.inv h) = mk (if h : g.LimZero then 0 else g.inv h)

Tactic:
simp only [hf, dite_false, hg]

Goal state after:
case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
⊢ mk (f.inv ⋯) = mk (g.inv ⋯)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |min (↑a j - ↑b j) (↑b j - ↑b j)| < ε✝

Tactic:
rwa [sub_self, min_eq_right, abs_zero]

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑a j - ↑b j
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (0 + 1) ^ b * a + (a * ↑b + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b

Tactic:
gcongr
        · norm_num
        · exact hb ha'

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec

Tactic:
by
  ext ⟨k, l⟩
  simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]

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
n : ℕ
⊢ 1⁻¹ = 1

Tactic:
inv_one

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 = 1
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
u : Mˣ
n : ℕ
⊢ ↑(u ^ n) = ↑u ^ n

Tactic:
Units.val_pow_eq_pow_val

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
n : ℕ
⊢ ↑u ^ n = ↑u ^ n
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]

Goal state after:
case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
d : ↥b.flip.support → ℤ
hd : ∀ (i : ↥b.flip.support), 0 < d i
hd' : (b.flip.cartanMatrix * Matrix.diagonal d).PosDef
⊢ (Matrix.diagonal d * b.cartanMatrix).PosDef

Tactic:
← PosDef.transpose_iff

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
d : ↥b.flip.support → ℤ
hd : ∀ (i : ↥b.flip.support), 0 < d i
hd' : (b.flip.cartanMatrix * Matrix.diagonal d)ᵀ.PosDef
⊢ (Matrix.diagonal d * b.cartanMatrix).PosDef