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

Goal state before:
pp: case h_option
R : Type u_1
inst✝ : Ring R
⊢ ∀ (α : Type u_5) [inst : Fintype α],
    (∀ (M : α → Type u_6) [inst_1 : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module R (M i)],
        length R ((i : α) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_1 : (i : Option α) → AddCommGroup (M i)]
        [inst_2 : (i : Option α) → Module R (M i)], length R ((i : Option α) → M i) = ∑ i, length R (M i)

Tactic:
intro ι

Goal state after:
case h_option
R : Type u_1
inst✝ : Ring R
ι : Type u_5
⊢ ∀ [inst : Fintype ι],
    (∀ (M : ι → Type u_6) [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)],
        length R ((i : ι) → M i) = ∑ i, length R (M i)) →
      ∀ (M : Option ι → Type u_6) [inst_1 : (i : Option ι) → AddCommGroup (M i)]
        [inst_2 : (i : Option ι) → Module R (M i)], length R ((i : Option ι) → M i) = ∑ i, length R (M i)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : b * c = a
⊢ b * c ∈ β

Tactic:
apply Ideal.mul_mem_right _ _ hb

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
by
  constructor
  · intro H x
    obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x
    have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
    obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
    · exact Or.inr
        ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩
    · exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩
  · intro H
    suffices PreValuationRing R from mk
    constructor
    intro a b
    by_cases ha : a = 0; · subst ha; exact ⟨0, Or.inr <| mul_zero b⟩
    by_cases hb : b = 0; · subst hb; exact ⟨0, Or.inl <| mul_zero a⟩
    replace ha := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr ha
    replace hb := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr hb
    obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)
    · rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
      exact ⟨c, Or.inr e⟩
    · rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e
      exact ⟨c, Or.inl e⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = ϖ * (ϖ * (a * b))
⊢ ϖ * (a * b) ≠ 1

Tactic:
exact fun hh => h2 (isUnit_of_dvd_one ⟨_, hh.symm⟩)

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
⊢ ValuationRing R

Tactic:
refine iff_dvd_total.mpr ⟨fun a b => ?_⟩

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
a b : R
⊢ a ∣ b ∨ b ∣ a
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
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n
⊢ F = lift I ha f ⋯

Tactic:
apply DFunLike.coe_injective
  apply IsHausdorff.StrictMono.funext I ha
  intro n m
  simp [← hF n]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
⊢ v y = v x

Tactic:
have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = max (v (y - x)) (v x)
⊢ v y = v x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
⊢ (addVal R) a = ⊤ ↔ a = 0

Tactic:
have hi := (Classical.choose_spec (exists_prime R)).irreducible
  constructor
  · contrapose
    intro h
    obtain ⟨n, ha⟩ := associated_pow_irreducible h hi
    obtain ⟨u, rfl⟩ := ha.symm
    rw [mul_comm, addVal_def' u hi n]
    nofun
  · rintro rfl
    exact addVal_zero

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ (IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegralElem p

Tactic:
refine (hp.symm ▸ this).of_mul_unit φ' p (algebraMap (R[X] ⧸ P) Sₘ (φ q')) q'' ?_

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ φ' q'' * (algebraMap (R[X] ⧸ P) Sₘ) (φ q') = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this = 0
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
have := Nat.find_spec this

Goal state after:
case neg.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = 0
this : maximalIdeal R ^ Nat.find this✝ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
⊢ IsIntegrallyClosed R

Tactic:
refine of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ Set.range MaximalSpectrum.toPrimeSpectrum → IsIntegrallyClosed (Localization.AtPrime x✝.asIdeal)

case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
⊢ ⨅ p ∈ Set.range MaximalSpectrum.toPrimeSpectrum, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯ = ⊥
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
⊢ ∀ {p : Ideal Rₘ}, p ≠ ⊥ → p.IsPrime → p.IsMaximal

Tactic:
by
  intro p hp0 hpp
  refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
  have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
  rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
  refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩
  exact IsLocalization.bot_lt_under_prime _ _ hM _ hp0

Goal state after:
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X), h (f x) = g x) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Surjective ⇑(lcomp R (CharacterModule M) f)

Tactic:
Surjective,

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X), h (f x) = g x) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f → ∀ (b : N →ₗ[R] CharacterModule M), ∃ a, (lcomp R (CharacterModule M) f) a = b
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩) ↔
    ∀ (I : Ideal R), Surjective ⇑(lcomp R (CharacterModule M) (Submodule.subtype I))

Tactic:
Surjective,

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩) ↔
    ∀ (I : Ideal R) (b : ↥I →ₗ[R] CharacterModule M), ∃ a, (lcomp R (CharacterModule M) (Submodule.subtype I)) a = b
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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y

Tactic:
obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
    · simp_all [valueGroup₀Fun_zero]
    obtain _ | ⟨r₂, s₂, hr₂, hs₂, rfl⟩ := y.zero_or_exists_mk
    · simp_all [valueGroup₀Fun_zero]
    simp [← WithZero.coe_mul, valueGroup.mk_mul, valueGroup₀Fun_spec h]

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✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ ((IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))).IsIntegral

Tactic:
refine RingHom.IsIntegral.trans (algebraMap (R ⧸ P') (Localization M))
        (IsLocalization.map (Localization M') φ M.le_comap_map) ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ (algebraMap (R ⧸ P') (Localization M)).IsIntegral

case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ (IsLocalization.map (Localization M') φ ⋯).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
⊢ (B.form ((P.reflection j) (P.root i))) ((P.reflection j) (P.root j)) =
    P.pairing i j * (B.form (P.root j)) (P.root j) - (B.form (P.root i)) (P.root j)

Tactic:
reflection_apply,

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
B : P.InvariantForm
i j : ι
⊢ (B.form (P.root i - (P.coroot' j) (P.root i) • P.root j)) ((P.reflection j) (P.root j)) =
    P.pairing i j * (B.form (P.root j)) (P.root j) - (B.form (P.root i)) (P.root j)
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 ι
y : N
hy : y ∈ (P.Polarization.domRestrict (P.rootSpan R)).range
⊢ y ∈ P.corootSpan R

Tactic:
obtain ⟨x, hx⟩ := hy

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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ y ∈ P.corootSpan R
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 : ι
c : S
hc :
  ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) =
    ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) * c
⊢ c • ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i ∈ (P.PolarizationIn S).range

Tactic:
rootFormIn_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
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 : ι
c : S
hc :
  ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) =
    ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) * c
⊢ c • 2 • (P.PolarizationIn S) (P.rootSpanMem S i) ∈ (P.PolarizationIn S).range
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R ↥(P.corootSpan R).dualAnnihilator ≤ finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
convert! Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
aux : finrank R M = finrank R ↥(P.rootSpan R) + finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R ↥(P.corootSpan R).dualAnnihilator =
    finrank R ↥(Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator)
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✝⁷ : 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
inst✝ : Fintype ι
x : ↥(span S (range ⇑P.root))
s : S
left✝ : s ≥ 0
hs : (algebraMap S R) s = (P.RootForm ↑x) ↑x
⊢ 0 ≤ ((P.posRootForm S).posForm x) x

Tactic:
have : s = (P.posRootForm S).posForm x x :=
    FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs

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✝⁷ : 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
inst✝ : Fintype ι
x : ↥(span S (range ⇑P.root))
s : S
left✝ : s ≥ 0
hs : (algebraMap S R) s = (P.RootForm ↑x) ↑x
this : s = ((P.posRootForm S).posForm x) x
⊢ 0 ≤ ((P.posRootForm S).posForm x) x
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α : α.IsZero
⊢ 0 = ↑(0 - 2 * 0)

Tactic:
mul_zero,

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
hα : α.IsZero
⊢ 0 = ↑(0 - 0)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_1
ι : 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
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ P.root j = 2 • P.root i

Tactic:
have : ¬ LinearIndependent R ![P.root i, P.root j] := by
      rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; simp

Goal state after:
case refine_1
ι : 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
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝¹ : IsAddTorsionFree M
this✝ : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root j = 2 • P.root i
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
S : Type u_5
i j : ι
inst✝⁷ : Finite ι
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R M
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeightIn S i j ≠ 4

Tactic:
rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]

Goal state after: