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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : a ∣ b
⊢ (addVal R) a ≤ (addVal R) b

Tactic:
· rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply]
    exact emultiplicity_le_emultiplicity_of_dvd_right h

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ

Tactic:
set u := WithZero.unzero (Units.ne_zero γ) with hu_def

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ f (v r) ≤ f (v s) ↔ v r ≤ v s

Tactic:
H.le_iff_le

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ v r ≤ v s ↔ v r ≤ v s
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ v' r ≤ v' s ↔ f (v' r) ≤ f (v' s)

Tactic:
H.le_iff_le

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ v' r ≤ v' s ↔ v' r ≤ v' s
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, (algebraMap Aₘ (FractionRing A)) y = x

Tactic:
intro x

Goal state after:
case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
⊢ IsIntegral Aₘ x → ∃ y, (algebraMap Aₘ (FractionRing A)) y = x
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ ⊥.jacobson = ⊥

Tactic:
have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero]

Goal state after:
case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
⊢ ⊥.jacobson = ⊥
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
this : ⊥.IsMaximal
⊢ ⊥.IsMaximal

Tactic:
← IsLocalization.under_map_of_isPrime_disjoint M (Localization M) isPrime_bot
      (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))

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
this : ⊥.IsMaximal
⊢ (under (R ⧸ P') (Ideal.map (algebraMap (R ⧸ P') (Localization M)) ⊥)).IsMaximal
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case smul
ι : 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✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x✝ : M
i : ι
t : S
x : M
hx✝ : x ∈ span S (range ⇑P.root)
hx : (P.coroot' i) x ∈ ↑(Algebra.linearMap S R).range
⊢ (P.coroot' i) (t • x) ∈ ↑(Algebra.linearMap S R).range

Tactic:
simpa only [LinearMap.map_smul_of_tower] using! Submodule.smul_mem _ t hx

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
i : ι
⊢ span R (range ⇑P.root) ≤ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
intro x

Goal state after:
ι : 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
i : ι
x : M
⊢ x ∈ span R (range ⇑P.root) → x ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
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, LinearMap.ker (P.coroot' i) ≤ LinearMap.ker P.RootForm

Tactic:
intro x

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 ι
x : M
⊢ x ∈ ⨅ i, LinearMap.ker (P.coroot' i) → x ∈ 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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
⊢ (P.PolarizationIn S).range ≤ P.corootSpan S

Tactic:
intro x

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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : N
⊢ x ∈ (P.PolarizationIn S).range → x ∈ P.corootSpan S
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
⊢ v.IsEquiv v'

Tactic:
intro x

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
⊢ ∀ (s : K), v x ≤ v s ↔ v' x ≤ v' s
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr
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), v x ≤ 1 ↔ v' x ≤ 1

Tactic:
intro x

Goal state after:
case mpr
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
⊢ v x ≤ 1 ↔ v' x ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr.mp.inl
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
this : v' (1 + x) = 1
⊢ v' x ≤ 1

Tactic:
show x = -1 + (1 + x) by simp

Goal state after:
case mpr.mp.inl
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
this : v' (1 + x) = 1
⊢ v' (-1 + (1 + x)) ≤ 1
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✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((∑ i, LinearMap.smulRight (P.coroot'In S i) (P.coroot'In S i)) (P.rootSpanMem S i)) (P.rootSpanMem S i) •
        P.coroot i -
      ∑ x, P.pairingIn S i x • (P.toLinearMap (P.root i)) (P.coroot x) • P.coroot i =
    ∑ i_1, P.pairingIn S i i_1 • P.coroot i_1 + ∑ x, -(P.pairingIn S i x • P.coroot x)

Tactic:
simp only [LinearMap.coe_sum, LinearMap.coe_smulRight, Finset.sum_apply,
    coroot'In_rootSpanMem_eq_pairingIn, LinearMap.smul_apply, smul_eq_mul, Finset.sum_smul,
    root_coroot_eq_pairing, Finset.sum_neg_distrib, add_neg_cancel, sub_eq_zero]

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ∑ i_1, (P.pairingIn S i i_1 * P.pairingIn S i i_1) • P.coroot i = ∑ x, P.pairingIn S i x • P.pairing i x • P.coroot i
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr.mpr.inl
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
this : v (1 + x) = 1
⊢ v x ≤ 1

Tactic:
show x = -1 + (1 + x) by simp

Goal state after:
case mpr.mpr.inl
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
this : v (1 + x) = 1
⊢ v (-1 + (1 + x)) ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mpr
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 : ¬x = 0
⊢ v' x = 1 → v x = 1

Tactic:
· intro hh
      by_contra h_1
      cases ne_iff_lt_or_gt.1 h_1 with
      | inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
      | inr h_2 =>
        rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
        exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))

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✝¹² : 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:
intro x

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
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
x : ↥(P.rootSpan S)
⊢ x ≠ 0 → 0 < (LinearMap.BilinMap.toQuadraticMap (P.RootFormIn S)) x
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case left
ι : 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.SeparatingLeft (P.posRootForm S).posForm

Tactic:
intro x

Goal state after:
case left
ι : 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
x : ↥(span S (range ⇑P.root))
⊢ (∀ (y : ↥(span S (range ⇑P.root))), ((P.posRootForm S).posForm x) y = 0) → x = 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case right
ι : 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.SeparatingRight (P.posRootForm S).posForm

Tactic:
intro x

Goal state after:
case right
ι : 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
x : ↥(span S (range ⇑P.root))
⊢ (∀ (x_1 : ↥(span S (range ⇑P.root))), ((P.posRootForm S).posForm x_1) x = 0) → x = 0
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), v x ≤ v (x + y) ∨ v y ≤ v (x + y)

Tactic:
intro x

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x : R
⊢ ∀ (y : R), v x ≤ v (x + y) ∨ v y ≤ v (x + y)
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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hx' : x = 0
⊢ 0 • x = ⁅coroot α, x⁆

Tactic:
simp [hx']

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert.inr
ι : 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
⊢ ↑(p j) ⊆ ⋃ i ∈ s, ↑(p i)

Tactic:
intro x

Goal state after:
case insert.inr
ι : 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
⊢ x ∈ ↑(p j) → x ∈ ⋃ i ∈ s, ↑(p i)
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert.inr
ι : 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
⊢ x ∈ ↑(p j) → x ∈ ⋃ i ∈ s, ↑(p i)

Tactic:
(hx : x ∈ p j)

Goal state after:
case insert.inr
ι : 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
⊢ x ∈ ⋃ i ∈ s, ↑(p i)
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
inst✝¹ : Finite ι
inst✝ : Infinite K
p : ι → Submodule K M
h : ∀ (i : ι), p i ≠ ⊤
_i : Fintype ι := Fintype.ofFinite ι
this : ⋃ i, ↑(p i) ⊂ univ
⊢ ∃ x, ∀ (i : ι), x ∉ p i

Tactic:
by simpa [ssubset_univ_iff, iUnion_eq_univ_iff] using this

Goal state after:
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
inst✝¹ : Finite ι
inst✝ : Infinite K
f : ι → Dual K M
h : ∀ (i : ι), ∃ x, (f i) x ≠ 0
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
⊢ ∃ x, ∀ (i : ι), (f i) x ≠ 0

Tactic:
replace h i : p i ≠ ⊤ := by specialize h i; aesop

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
f : ι → Dual K M
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
⊢ ∃ x, ∀ (i : ι), (f i) x ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case left
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), Q₁ a + Q₂ b = 0 → a = 0 ∧ b = 0
⊢ Q₁.Anisotropic

Tactic:
intro x

Goal state after:
case left
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), Q₁ a + Q₂ b = 0 → a = 0 ∧ b = 0
x : M₁
⊢ Q₁ x = 0 → x = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case right
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), Q₁ a + Q₂ b = 0 → a = 0 ∧ b = 0
⊢ Q₂.Anisotropic

Tactic:
intro x

Goal state after:
case right
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
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), Q₁ a + Q₂ b = 0 → a = 0 ∧ b = 0
x : M₂
⊢ Q₂ x = 0 → x = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp.left
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✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b
⊢ ∀ (x : M₁), 0 ≤ Q₁ x

Tactic:
intro x

Goal state after:
case mp.left
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✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b
x : M₁
⊢ 0 ≤ Q₁ x