mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ LieSubalgebra K L

Tactic:
choose h e f t ht using exists_isSl2Triple_of_weight_isNonZero hα
  exact t.toLieSubalgebra K

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = ↑n.natAbs
⊢ C R ↑n.natAbs = C R n

pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R n

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = ↑n.natAbs
⊢ C R ↑n.natAbs = C R n

case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp (Polynomial.C (2 * ⅟2) * X) = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
mul_invOf_self',

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp (Polynomial.C 1 * X) = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅↑h, e⁆ = α h • e
hf_wt : ⁅↑h, f⁆ = (-α) h • f
⊢ ∃ c₁_1 c₂_1 c₃_1, c₁ • ⁅↑h, e⁆ + c₂ • ⁅↑h, f⁆ + c₃ • ⁅↑h, ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆

Tactic:
have hef_zero : ⁅(h : L), ⁅e, f⁆⁆ = 0 := by
      suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
        lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
      rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]
      exact (coroot α).property

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅↑h, e⁆ = α h • e
hf_wt : ⁅↑h, f⁆ = (-α) h • f
hef_zero : ⁅↑h, ⁅e, f⁆⁆ = 0
⊢ ∃ c₁_1 c₂_1 c₃_1, c₁ • ⁅↑h, e⁆ + c₂ • ⁅↑h, f⁆ + c₃ • ⁅↑h, ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ S R 2 = X ^ 2 - 1

Tactic:
by
  have := S_add_two R 0
  simp only [zero_add, S_one, S_zero] at this
  linear_combination this

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (Polynomial.C (2 * ⅟2) * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
mul_invOf_self',

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (Polynomial.C 1 * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α

Tactic:
conv_lhs => rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case e'_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ (fun m ↦ T R ↑m) '' Set.Ico 0 n = (fun m ↦ T R ↑m) '' Set.Icc 0 (n - 1)

pp: case e'_5
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Int.subNatNat n 1 = ↑(n - 1)

Tactic:
<;>

Goal state after:
case e'_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ (fun m ↦ T R ↑m) '' Set.Ico 0 n = (fun m ↦ T R ↑m) '' Set.Icc 0 (n - 1)

case e'_5
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Int.subNatNat n 1 = ↑(n - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (T R n) -
      ((⇑derivative)^[0 + 2] (T R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (T R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (T R n)) =
    (⇑derivative)^[0 + 1] (T R n) * X + 0 • (⇑derivative)^[0] (T R n) - ↑(n ^ 2) * (⇑derivative)^[0] (T R n)
⊢ (⇑derivative)^[0] (T R n) * ↑0 + (⇑derivative)^[0] (T R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (T R n) * ↑0 ^ 2 = 0

pp: case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (T R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (T R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (T R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (T R n)) =
    (⇑derivative)^[n✝ + 1 + 1] (T R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (T R n) -
      ↑(n ^ 2) * (⇑derivative)^[n✝ + 1] (T R n)
⊢ (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) ^ 2 =
    0

Tactic:
<;>

Goal state after:
case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (T R n) -
      ((⇑derivative)^[0 + 2] (T R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (T R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (T R n)) =
    (⇑derivative)^[0 + 1] (T R n) * X + 0 • (⇑derivative)^[0] (T R n) - ↑(n ^ 2) * (⇑derivative)^[0] (T R n)
⊢ (⇑derivative)^[0] (T R n) * ↑0 + (⇑derivative)^[0] (T R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (T R n) * ↑0 ^ 2 = 0

case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (T R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (T R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (T R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (T R n)) =
    (⇑derivative)^[n✝ + 1 + 1] (T R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (T R n) -
      ↑(n ^ 2) * (⇑derivative)^[n✝ + 1] (T R n)
⊢ (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (T R n) * ↑(n✝ + 1) ^ 2 =
    0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (U R n) -
      ((⇑derivative)^[0 + 2] (U R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (U R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (U R n)) =
    ↑3 * ((⇑derivative)^[0 + 1] (U R n) * X + 0 • (⇑derivative)^[0] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[0] (U R n)
⊢ (⇑derivative)^[0] (U R n) * ↑0 + (⇑derivative)^[0] (U R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (U R n) * ↑0 ^ 2 = 0

pp: case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (U R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (U R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (U R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (U R n)) =
    ↑3 * ((⇑derivative)^[n✝ + 1 + 1] (U R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[n✝ + 1] (U R n)
⊢ (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) ^ 2 =
    0

Tactic:
<;>

Goal state after:
case a.zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (⇑derivative)^[0 + 2] (U R n) -
      ((⇑derivative)^[0 + 2] (U R n) * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] (U R n) * X +
        (0 * (0 - 1)) • (⇑derivative)^[0] (U R n)) =
    ↑3 * ((⇑derivative)^[0 + 1] (U R n) * X + 0 • (⇑derivative)^[0] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[0] (U R n)
⊢ (⇑derivative)^[0] (U R n) * ↑0 + (⇑derivative)^[0] (U R n) * ↑0 * ↑(0 - 1) - (⇑derivative)^[0] (U R n) * ↑0 ^ 2 = 0

case a.succ
R : Type u_1
inst✝ : CommRing R
n : ℤ
n✝ : ℕ
h :
  (⇑derivative)^[n✝ + 1 + 2] (U R n) -
      ((⇑derivative)^[n✝ + 1 + 2] (U R n) * X ^ 2 + (2 * (n✝ + 1)) • (⇑derivative)^[n✝ + 1 + 1] (U R n) * X +
        ((n✝ + 1) * (n✝ + 1 - 1)) • (⇑derivative)^[n✝ + 1] (U R n)) =
    ↑3 * ((⇑derivative)^[n✝ + 1 + 1] (U R n) * X + (n✝ + 1) • (⇑derivative)^[n✝ + 1] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[n✝ + 1] (U R n)
⊢ (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) + (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) * ↑(n✝ + 1 - 1) -
      (⇑derivative)^[n✝ + 1] (U R n) * ↑(n✝ + 1) ^ 2 =
    0
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
⊢ (aeval ((algebraMap A S) r)) (p.scaleRoots ↑s) = 0

Tactic:
convert! scaleRoots_eval₂_eq_zero (algebraMap A S) hr
  funext
  rw [aeval_def, mk'_spec' _ r s]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
⊢ 0 < b → withZeroUnitsEquiv 0 < withZeroUnitsEquiv b

pp: case coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a✝ : αˣ
⊢ ↑a✝ < b → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv b

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
⊢ 0 < b → withZeroUnitsEquiv 0 < withZeroUnitsEquiv b

case coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a✝ : αˣ
⊢ ↑a✝ < b → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv b
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: case zero.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ 0 < 0 → withZeroUnitsEquiv 0 < withZeroUnitsEquiv 0

pp: case zero.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ 0 < ↑a✝ → withZeroUnitsEquiv 0 < withZeroUnitsEquiv ↑a✝

pp: case coe.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ ↑a✝ < 0 → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv 0

pp: case coe.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝¹ a✝ : αˣ
⊢ ↑a✝¹ < ↑a✝ → withZeroUnitsEquiv ↑a✝¹ < withZeroUnitsEquiv ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ 0 < 0 → withZeroUnitsEquiv 0 < withZeroUnitsEquiv 0

case zero.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ 0 < ↑a✝ → withZeroUnitsEquiv 0 < withZeroUnitsEquiv ↑a✝

case coe.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ ↑a✝ < 0 → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv 0

case coe.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝¹ a✝ : αˣ
⊢ ↑a✝¹ < ↑a✝ → withZeroUnitsEquiv ↑a✝¹ < withZeroUnitsEquiv ↑a✝
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
⊢ length R M = length R N + length R P

Tactic:
by_cases hP : IsFiniteLength R P
  · by_cases hN : IsFiniteLength R N
    · obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP
      obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN
      let s' : CompositionSeries (Submodule R M) :=
        s.map ⟨Submodule.comap g, Submodule.comap_covBy_of_surjective hg⟩
      let t' : CompositionSeries (Submodule R M) :=
        t.map ⟨Submodule.map f, Submodule.map_covBy_of_injective hf⟩
      have hfg : Submodule.map f ⊤ = Submodule.comap g ⊥ := by
        rw [Submodule.map_top, Submodule.comap_bot, LinearMap.exact_iff.mp H]
      let r := t'.smash s' (by simpa [s', t', hs₁, ht₂] using hfg)
      rw [← Module.length_compositionSeries s hs₁ hs₂,
        ← Module.length_compositionSeries t ht₁ ht₂,
        ← Module.length_compositionSeries r
          (by simpa [r, t', ht₁, -Submodule.map_bot] using Submodule.map_bot f)
          (by simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g)]
      simp_rw [r, RelSeries.smash_length, Nat.cast_add, s', t', RelSeries.map_length]
    · have := mt (IsFiniteLength.of_injective · hf) hN
      rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
      rw [hN, this, top_add]
  · have := mt (IsFiniteLength.of_surjective · hg) hP
    rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
    rw [hP, this, add_top]

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : x ∈ {x | v x ≤ 1}
⊢ -x ∈ {x | v x ≤ 1}

Tactic:
simp only [Set.mem_ofPred_eq] at hx; simpa only [Set.mem_ofPred_eq, map_neg]

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

Goal state before:
pp: case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial O → Nontrivial R

pp: case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial R → Nontrivial O

Tactic:
<;>

Goal state after:
case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial O → Nontrivial R

case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial R → Nontrivial O
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inl
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x ≤ 1
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

pp: case inr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x⁻¹ ≤ 1
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Tactic:
<;>

Goal state after:
case inl
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x ≤ 1
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

case inr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x⁻¹ ≤ 1
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ Submodule.IsPrincipal I → ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

pp: case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → Submodule.IsPrincipal I

Tactic:
<;>

Goal state after:
case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ Submodule.IsPrincipal I → ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → Submodule.IsPrincipal I
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
inst✝ : IsHausdorff I M
x y : M
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]

Tactic:
refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
  rw [← sub_eq_zero]
  apply IsHausdorff.haus' (I := I) (x - y)
  simpa [SModEq.sub_mem] using h

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

Goal state before:
pp: case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

pp: case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}) → ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Tactic:
<;>

Goal state after:
case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}) → ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I → v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

pp: case mp.mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a) → b ∈ I

Tactic:
<;>

Goal state after:
case mp.mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I → v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

case mp.mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a) → b ∈ I
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_1.inl
R : Type u_1
inst✝ : Semigroup R
H : PreValuationRing R
a c : R
⊢ a ∣ a * c ∨ a * c ∣ a

pp: case refine_1.inr
R : Type u_1
inst✝ : Semigroup R
H : PreValuationRing R
b c : R
⊢ b * c ∣ b ∨ b ∣ b * c

Tactic:
<;>

Goal state after:
case refine_1.inl
R : Type u_1
inst✝ : Semigroup R
H : PreValuationRing R
a c : R
⊢ a ∣ a * c ∨ a * c ∣ a

case refine_1.inr
R : Type u_1
inst✝ : Semigroup R
H : PreValuationRing R
b c : R
⊢ b * c ∣ b ∨ b ∣ b * c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a c : R
⊢ ∃ c_1, a * c_1 = a * c ∨ a * c * c_1 = a

pp: case refine_2.inr
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
b c : R
⊢ ∃ c_1, b * c * c_1 = b ∨ b * c_1 = b * c

Tactic:
<;>

Goal state after:
case refine_2.inl
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a c : R
⊢ ∃ c_1, a * c_1 = a * c ∨ a * c * c_1 = a

case refine_2.inr
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
b c : R
⊢ ∃ c_1, b * c * c_1 = b ∨ b * c_1 = b * c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a c : R
⊢ a * c = a * c ∨ a * c * c = a

pp: case h
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
b c : R
⊢ b * c * c = b ∨ b * c = b * c

Tactic:
<;>

Goal state after:
case h
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
a c : R
⊢ a * c = a * c ∨ a * c * c = a

case h
R : Type u_1
inst✝ : Semigroup R
H : Std.Total fun x1 x2 ↦ x1 ∣ x2
b c : R
⊢ b * c * c = b ∨ b * c = b * c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ValuationRing R

Tactic:
suffices PreValuationRing R from mk

Goal state after:
case mpr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ PreValuationRing R