mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ (⇑i ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑i

Tactic:
ext

Goal state after:
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
x✝ : ↥K
⊢ (⇑i ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑i) x✝
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False

Tactic:
inf_eq_right.mpr hx

Goal state after:
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x✝ : α
⊢ (⇑f ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑f) x✝
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ Units.mk0 (v π) ⋯ ∈ (MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))).valueGroup ∧ Units.mk0 (v π) ⋯ ≠ 1

Tactic:
constructor

Goal state after:
case h.left
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ Units.mk0 (v π) ⋯ ∈ (MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))).valueGroup

case h.right
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ Units.mk0 (v π) ⋯ ≠ 1
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ DenselyOrdered ↑(some ⁻¹' s)

Tactic:
constructor

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ ∀ (a₁ a₂ : ↑(some ⁻¹' s)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Subring.map (algebraMap A K) ⊤ = (valuation K (maximalIdeal A)).valuationSubring.toSubring

Tactic:
ext

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ Subring.map (algebraMap A K) ⊤ ↔ x✝ ∈ (valuation K (maximalIdeal A)).valuationSubring.toSubring
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
b : Gˣ
ha : 0 < 1
⊢ ∃ n, 0 ^ n < ↑b

Tactic:
use 1
    simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) ↔ ∃! k, a ^ k = b

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) → ∃! k, a ^ k = b

case mpr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃! k, a ^ k = b) → ∃ n, a ^ n = b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁) ∈ map (fun x ↦ x⁻¹) F ∧
    ∀ x ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), ∀ y ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), v.restrict (y - x) < ↑γ

Tactic:
constructor

Goal state after:
case h.left
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁) ∈ map (fun x ↦ x⁻¹) F

case h.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ ∀ x ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), ∀ y ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), v.restrict (y - x) < ↑γ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b → b = |a|ₘ ∧ 1 < b

case mpr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
⊢ b = |a|ₘ ∧ 1 < b → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W = { a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K

Tactic:
ext

Goal state after:
case h.a₁
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₁ = ({ a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K).a₁

case h.a₂
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₂ = ({ a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K).a₂

case h.a₃
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₃ = ({ a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K).a₃

case h.a₄
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₄ = ({ a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K).a₄

case h.a₆
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₆ = ({ a₁ := h₁.choose, a₂ := h₂.choose, a₃ := h₃.choose, a₄ := h₄.choose, a₆ := h₆.choose }⁄K).a₆
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
by
    rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h
    · simpa [this h] using ⟨h⟩
    · simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
      exact ⟨fun H ↦ (this H) h⟩

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
constructor

Goal state after:
case mp
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) → Nonempty (G ≃+o ℤ)

case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (⇑embedding ∘ extension) (x + y) ≤ max ((⇑embedding ∘ extension) x) ((⇑embedding ∘ extension) y)

Tactic:
le_max_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (⇑embedding ∘ extension) (x + y) ≤ (⇑embedding ∘ extension) x ∨
    (⇑embedding ∘ extension) (x + y) ≤ (⇑embedding ∘ extension) y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
⊢ {b | ∃ r, v.restrict r = extension b} = extension ⁻¹' range ⇑v.restrict

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h✝ : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
x✝ : hat K
⊢ x✝ ∈ {b | ∃ r, v.restrict r = extension b} ↔ x✝ ∈ extension ⁻¹' range ⇑v.restrict
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ G₀ → G₀ˣ

Tactic:
exact fun x ↦ if h : x = 0 then 1 else Units.mk0 x h

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ MulArchimedean β

Tactic:
constructor

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ ∀ (x : β) {y : β}, 1 < y → ∃ n, x ≤ y ^ n
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ 1 < e.symm y

Tactic:
simp [← map_lt_map_iff e, hxy]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean (WithZero α) ↔ MulArchimedean α

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean (WithZero α) → MulArchimedean α

case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean α → MulArchimedean (WithZero α)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ˣ ↔ MulArchimedean G₀

Tactic:
constructor

Goal state after:
case mp
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ˣ → MulArchimedean G₀

case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ → MulArchimedean G₀ˣ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
⊢ a • f = C a * f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
n✝ : ℕ
⊢ (coeff n✝) (a • f) = (coeff n✝) (C a * f)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ Units.mk0 (v xy) ⋯ = Units.mk0 (v x * v y) ?neg.hxy✝

Tactic:
ext

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯
hx_def : x = ⋯.choose
y : K := ⋯
hy_def : y = ⋯.choose
xy : K := ⋯
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ↑(Units.mk0 (v xy) ⋯) = ↑(Units.mk0 (v x * v y) ?neg.hxy✝)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (map f) (C r) = C (f r)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
r : R
n✝ : ℕ
⊢ (coeff n✝) ((map f) (C r)) = (coeff n✝) (C (f r))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
⊢ (map f) X = X

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
n✝ : ℕ
⊢ (coeff n✝) ((map f) X) = (coeff n✝) X
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0

Tactic:
constructor

Goal state after:
case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) → ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0

case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0) → ∀ m < n, (coeff m) φ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: a b c : ℕ
⊢ ofAdd (-↑c) ≤ max (ofAdd (-↑a)) (ofAdd (-↑b)) ↔ min a b ≤ c

Tactic:
le_max_iff,

Goal state after:
a b c : ℕ
⊢ ofAdd (-↑c) ≤ ofAdd (-↑a) ∨ ofAdd (-↑c) ≤ ofAdd (-↑b) ↔ min a b ≤ c
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff m) φ = 0) ↔ (coeff 0) φ = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff m) φ = 0) → (coeff 0) φ = 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) φ = 0 → ∀ m < 1, (coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
⊢ a • f = C a * f

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (a • f) = (coeff n✝) (C a * f)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
⊢ (mk fun n ↦ a ^ n * (coeff n) (f * g)) = (mk fun n ↦ a ^ n * (coeff n) f) * mk fun n ↦ a ^ n * (coeff n) g

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (mk fun n ↦ a ^ n * (coeff n) (f * g)) =
    (coeff n✝) ((mk fun n ↦ a ^ n * (coeff n) f) * mk fun n ↦ a ^ n * (coeff n) g)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ → ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0) → X s ^ n ∣ φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (mk fun n ↦ a ^ n * (coeff n) 0) = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
⊢ (coeff n✝) (mk fun n ↦ a ^ n * (coeff n) 0) = (coeff n✝) 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
x✝ y✝ : R⟦X⟧
⊢ (mk fun n ↦ a ^ n * (coeff n) (x✝ + y✝)) = (mk fun n ↦ a ^ n * (coeff n) x✝) + mk fun n ↦ a ^ n * (coeff n) y✝

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
x✝ y✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (mk fun n ↦ a ^ n * (coeff n) (x✝ + y✝)) =
    (coeff n✝) ((mk fun n ↦ a ^ n * (coeff n) x✝) + mk fun n ↦ a ^ n * (coeff n) y✝)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ rescale 1 = RingHom.id R⟦X⟧

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) ((rescale 1) x✝) = (coeff n✝) ((RingHom.id R⟦X⟧) x✝)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
⊢ (rescale a) (mk f) = mk fun n ↦ a ^ n * f n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ (coeff n✝) ((rescale a) (mk f)) = (coeff n✝) (mk fun n ↦ a ^ n * f n)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b : R
⊢ rescale (a * b) = (rescale b).comp (rescale a)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) ((rescale (a * b)) x✝) = (coeff n✝) (((rescale b).comp (rescale a)) x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2

Tactic:
ext

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (single s n + (i, j).2 - single s n + single s n) a✝ = (single s n + (i, j).2) a✝
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.intValuation r ≤ exp (-↑n) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
by_cases hr : r = 0
  · simp_rw [hr, Valuation.map_zero, Ideal.dvd_span_singleton, zero_le, Submodule.zero_mem]
  · rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]

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

Goal state before:
pp: case h
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤

Tactic:
constructor

Goal state after:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X}

case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
a : A
⊢ (rescale a) X = C a * X

Tactic:
ext

Goal state after:
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (coeff n✝) ((rescale a) X) = (coeff n✝) (C a * X)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑((monomial n) a) = (PowerSeries.monomial n) a

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑((monomial n) a) = (PowerSeries.coeff n✝) ((PowerSeries.monomial n) a)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R[X]
⊢ ↑(φ + ψ) = ↑φ + ↑ψ

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R[X]
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑(φ + ψ) = (PowerSeries.coeff n✝) (↑φ + ↑ψ)