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
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
tfae_1_iff_3 : v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
tfae_1_iff_4 : v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE

Tactic:
tfae_have 1 ↔ 5 := isEquiv_iff_val_lt_one

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' : R
⊢ ∀ (s : R), v s = 0 → v (a' + s) ≤ v a'

Tactic:
s'

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
⊢ v s' = 0 → v (a' + s') ≤ v a'
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
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
⊢ (LinearMap.BilinMap.toQuadraticMap (P.RootFormIn S)).PosDef

Tactic:
by
  intro x hx
  simpa using P.posRootForm_posForm_pos_of_ne_zero S hx

Goal state after:
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✝¹ : Nontrivial R
inst✝ : P.IsReduced
⊢ LinearIndependent R ![P.root i, P.root j] ↔ i ≠ j ∧ P.root i ≠ -P.root j

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h, h'⟩ ↦ linearIndependent P h h'⟩

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
i j : ι
inst✝¹ : Nontrivial R
inst✝ : P.IsReduced
h : LinearIndependent R ![P.root i, P.root j]
⊢ i ≠ j ∧ P.root i ≠ -P.root j
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : α.IsZero
⊢ 0 • x = ⁅0, x⁆

Tactic:
zero_smul,

Goal state after:
case pos
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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : α.IsZero
⊢ 0 = ⁅0, x⁆
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)
k : ι
hk : k ∈ s
t₁ t₂ : K
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
⊢ x ∈ p k

Tactic:
convert sub_mem ht₁ ((p k).smul_mem t₁ ht)

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)
k : ι
hk : k ∈ s
t₁ t₂ : K
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
ht : y ∈ p k
⊢ x = x + t₁ • y - t₁ • y
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
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α : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β
⊢ genWeightSpace L (↑(chainTopCoeff (⇑α) β - (chainLength α β).succ) • ⇑α + ⇑β) = ⊥

Tactic:
Nat.cast_sub e,

Goal state after:
case neg
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α : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β
⊢ genWeightSpace L ((↑(chainTopCoeff (⇑α) β) - ↑(chainLength α β).succ) • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ i, (Q i) (x i)) → ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Tactic:
intro h i x
    classical
    convert! h (Pi.single i x) using 1
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]
    rw [Pi.single_eq_of_ne hji, map_zero]

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
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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R), ∑ i ∈ s with 0 < c i, c i • v i = 0 → ∀ i ∈ s, c i ≤ 0
⊢ ∀ i ∈ s, c i = 0

Tactic:
replace hx (i : ι) (hi : i ∈ s) : c i ≤ 0 := H _ (by grind) i hi

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
x : M := ∑ 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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R), ∑ i ∈ s with 0 < c i, c i • v i = 0 → ∀ i ∈ s, c i ≤ 0
hx : ∀ i ∈ s, c i ≤ 0
⊢ ∀ i ∈ s, c i = 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

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

Tactic:
have := (rootSpace_zsmul_add_ne_bot_iff_mem α 0 hα (n - chainTopCoeff α β)).mp
      (by rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, FunLike.coe_zero, add_zero]; exact β.2)

Goal state after:
case 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
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
this : ↑n - ↑(chainTopCoeff (⇑α) β) ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) 0)) ↑(chainTopCoeff (⇑α) 0)
⊢ k = -1 ∨ k = 0 ∨ k = 1
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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩ ∨ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩

Tactic:
obtain (h | h) := eq_neg_or_eq_of_eq_smul α β (by simpa using hβ) u
      (by ext x; exact DFunLike.congr_fun hu.symm x)

Goal state after:
case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩ ∨ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩

case 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α : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩ ∨ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩
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
⊢ Injective ⇑(weightHom P)

Tactic:
refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_
  let h : (weightHom P g).toLinearMap = (weightHom P g').toLinearMap := hgg' --`have` gets lint
  rw [weightHom_toLinearMap, weightHom_toLinearMap] at h
  suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')
  exact Hom.weightHom_injective P hgg'

Goal state after:
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
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
hsi' : (algebraMap S R) si = ((P.posRootForm S).form (P.root i)) (P.root i)
sj : S
hsj : sj > 0
hsj' : (algebraMap S R) sj = ((P.posRootForm S).form (P.root j)) (P.root j)
⊢ (algebraMap S R) si = (algebraMap S R) li

Tactic:
by simpa [li] using hsi'

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
⊢ P.root l - P.root i ∉ range ⇑P.root

Tactic:
replace hl : P.root l - P.root i = P.root j + (s - 1) • P.root i := by rw [hl]; module

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
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 : ι
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hl : P.root l - P.root i = P.root j + (s - 1) • P.root i
⊢ P.root l - 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root

Tactic:
by rwa [hf]

Goal state after:
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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
this : s ⊆ baseOf (⇑P.root) f
⊢ (baseOf (⇑P.root) f).ncard ≤ s.ncard

Tactic:
h_card

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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
this : s ⊆ baseOf (⇑P.root) f
⊢ s.ncard ≤ s.ncard
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ toBilin (Pi.basisFun R₁ n) = toBilin'

Tactic:
by
  ext M
  simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr,
    toBilin'_apply]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
G : Type u_3
inst✝¹ : SMul G β
inst✝ : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2

Tactic:
simpa [const_smul, smul_one_mul _ _] using
    mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
obtain ⟨h₁, h₂⟩ := h j ij

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
⊢ F / 2 ≤ ↑(f + g) j
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : (const abv x).LimZero then 0 else (const abv x).inv h

Tactic:
by split_ifs with h <;>
    [simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
a✝ : Nontrivial R
⊢ (0 < fun i ↦ star (v i) * v i) ↔ v ≠ 0

Tactic:
simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]

Goal state after:
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
a✝ : Nontrivial R
⊢ ((0 ≤ fun i ↦ star (v i) * v i) ∧ ∃ i, 0 < star (v i) * v i) ↔ ∃ a, v a ≠ 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr
a : ℝ
ha : 0 ≤ a
b : ℕ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
clear ha

Goal state after:
case inr
a : ℝ
b : ℕ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝⁵ : CommRing α
inst✝⁴ : StarRing α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) =
    star ((D⁻¹ * Bᴴ) *ᵥ x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) + star x ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x

Tactic:
simp [Function.star_sumElim, vecMul_fromBlocks, add_vecMul,
    dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, hD.eq,
    conjTranspose_nonsing_inv, star_mulVec]

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝⁵ : CommRing α
inst✝⁴ : StarRing α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
by
  have := Fintype.ofFinite m
  refine of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_mul B hA.1) fun x ↦ ?_
  simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using
      hA.dotProduct_mulVec_nonneg (B *ᵥ x)

Goal state after:
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
hg : (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix
⊢ Injective fun v ↦ v ᵥ* b.cartanMatrix

Tactic:
rw [Matrix.vecMul_injective_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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
hg : (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix
⊢ LinearIndependent ℤ b.cartanMatrix.row
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
r : R
⊢ 1 = eval (r - ↑0 + 1) 1

Tactic:
eval_one

Goal state after:
case zero
R : Type u
inst✝ : Ring R
r : R
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : k ≤ n
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Tactic:
rw [Nat.cast_mul, Nat.cast_sub h]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
⊢ ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0

Tactic:
intro y ⟨f, hf⟩

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : L₂
f : ι₁ →₀ R
hf : (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) f = (0, y)
⊢ y = 0