mathlib-initiative/mathlib-tactics huggingface dataset:
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 • ⊤
⊢ ↑x n = 0

pp: case refine_2
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 n = 0
⊢ ↑x m ∈ I ^ n • ⊤

Tactic:
· rw [← x.prop m_ge, transitionMap, Submodule.factorPow, Submodule.factor, mapQ,
      ← LinearMap.mem_ker]
    simpa [ker_liftQ]

Goal state after:
case refine_2
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 n = 0
⊢ ↑x m ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.Jacobson.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n = 0

Tactic:
suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n ∈ ⊥.jacobson
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
r : R
hr : r ∈ I
hr0 : ¬r = 0
⊢ r ∈ span {p ^ Nat.find ex}

Tactic:
obtain ⟨n, u, rfl⟩ := H hr0

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
n : ℕ
u : Rˣ
hr : p ^ n * ↑u ∈ I
hr0 : ¬p ^ n * ↑u = 0
⊢ p ^ n * ↑u ∈ span {p ^ Nat.find ex}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case mp
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
h : J.IsMaximal
hJ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
⊢ (under R J).IsMaximal

Tactic:
convert! hIm

Goal state after:
case e'_3
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
h : J.IsMaximal
hJ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
⊢ under R J = I
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:
rw [H.le_iff_le]

Goal state after:
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:
rw [H.le_iff_le]

Goal state after:
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
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
⊢ P = comap f (Ideal.map f P)

Tactic:
rw [comap_map_of_surjective _ hf]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
⊢ P = P ⊔ comap f ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective ⇑(g.comp (Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
RingHom.coe_comp

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).root) = ⊤

Tactic:
by
    rw [← span_setOfPred_mem_eq_top]
    congr
    ext ⟨x, hx⟩
    simp [restrictScalars']

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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ span K (range ⇑(P.restrictScalars' K).coroot) = ⊤

Tactic:
by
    rw [← span_setOfPred_mem_eq_top]
    congr
    ext ⟨x, hx⟩
    simp [restrictScalars']

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_6
inst✝³ : CommRing S
inst✝² : Module S M
inst✝¹ : Nonempty ι
inst✝ : NeZero 2
⊢ P.rootSpan S ≠ ⊥

Tactic:
simpa [rootSpan] using P.exists_ne_zero

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

Goal state before:
pp: case hg₁
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
⊢ (P₁.flip (P₂.coroot i)) (P₁.root i) = 2

Tactic:
exact hr ▸ he ▸ P₂.coroot_root_two i

Goal state after:
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
⊢ v x ≤ 1

Tactic:
have : v' (1 + x) = 1 := by
          rw [← v'.map_one]
          apply map_add_eq_of_lt_left
          simpa
        rw [← h] at this
        rw [show x = -1 + (1 + x) by simp]
        refine le_trans (v.map_add _ _) ?_
        simp [this]

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

Goal state before:
pp: case neg.mpr.inr
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
hh : v' x = 1
h_1 : ¬v x = 1
h_2 : 1 < v x
⊢ False

Tactic:
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.Basic

Goal state before:
pp: case h.hf₁
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ (P₁.flip.toPerfPair (P₂.coroot i)) ?m.306 = 2

Tactic:
exact hr ▸ he ▸ P₂.coroot_root_two i

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'⟩
  rw [LinearIndependent.pair_iff] at h
  contrapose! h
  rcases eq_or_ne i j with rfl | h'
  · exact ⟨1, -1, by simp⟩
  · rw [h h']
    exact ⟨1, 1, by simp⟩

Goal state after:
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
⊢ c • (P.RootForm (P.root i)) (P.root i) • P.coroot i ∈ (P.Polarization.domRestrict (P.rootSpan R)).range

Tactic:
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.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
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
h₁ : ∀ (y : M), y ∈ p j
x✝ : M
⊢ x✝ ∈ p j ↔ x✝ ∈ ⊤

Tactic:
simp [h₁]

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✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
⊢ P.coxeterWeight i j ≠ 4

Tactic:
by
  intro contra
  have := P.infinite_of_linearIndependent_coxeterWeight_four hl contra
  exact not_finite ι

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
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 ≤ {t | t ≠ 0}.encard + 1

Tactic:
encard_ne_add_one

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 ≤ ENat.card K
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: 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 : ∀ (x : M₁ × M₂), Q₁ x.1 + Q₂ x.2 = 0 → x = 0
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic

Tactic:
Prod.forall,

Goal state after:
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, b) = 0
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: 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
⊢ (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x

Tactic:
Prod.forall,

Goal state after:
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
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ (Q₁.prod Q₂) (a, b)) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp.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
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; simpa only [zero_add, map_zero] using h 0 x

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

Goal state before:
pp: case mp
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
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b) → (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x

Tactic:
intro h
    constructor
    · intro x; simpa only [add_zero, map_zero] using h x 0
    · intro x; simpa only [zero_add, map_zero] using h 0 x

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
n : ℤ
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) β)) ↑(chainTopCoeff (⇑α) β)

Tactic:
rootSpace_zsmul_add_ne_bot_iff α β hα n,

Goal state after:
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
n : ℤ
⊢ n ≤ ↑(chainTopCoeff (⇑α) β) ∧ -n ≤ ↑(chainBotCoeff (⇑α) β) ↔
    n ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) β)) ↑(chainTopCoeff (⇑α) β)
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mpr
ι : 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
h : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic
x : (i : ι) → Mᵢ i
hx : ∀ i ∈ Finset.univ, (Q i) (x i) = 0
i : ι
⊢ (Q i) (x i) = 0

Tactic:
exact hx _ (Finset.mem_univ _)

Goal state after:
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
hβ : β.IsNonZero
k : K
h : ⇑β = 0
hα : α.IsZero
⊢ β = -α ∨ β = α

Tactic:
cases hβ h

Goal state after:
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
hβ : β.IsNonZero
e : (reflectRoot α β).IsZero
hα : α.IsZero
⊢ β (coroot α) = 0

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β : β.IsNonZero
e : (reflectRoot α β).IsZero
hα : ¬α.IsZero
⊢ β (coroot α) = 0

Tactic:
· simp [coroot_eq_zero_iff.mpr hα]

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β : β.IsNonZero
e : (reflectRoot α β).IsZero
hα : ¬α.IsZero
⊢ β (coroot α) = 0
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
e : ∃ x, x • 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 ⟨u, hu⟩ := e

Goal state after:
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β⟩
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 ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp
    (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)
  simpa [← P.algebraMap_pairingIn ℤ] using P.pairing_eq_zero_iff' (i := i) (j := j)

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

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

Tactic:
← root_coroot'_eq_pairing,

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 : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ (P.coroot' i) (P.root k) = P.pairing j i + (algebraMap ℤ R) r * (algebraMap ℤ R) 2