mathlib-initiative/mathlib-tactics huggingface dataset:
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 : K
⊢ Tendsto (⇑v.restrict) (𝓝 x) (𝓝 (v.restrict x))

Tactic:
exact Valued.continuous_valuation.continuousAt

Goal state after:
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)
⊢ extension (x * y) = extension x * extension y

Tactic:
apply Completion.induction_on₂ x y
      (p := fun x y => extension (x * y) = extension x * extension y)

Goal state after:
case hp
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)
⊢ IsClosed {x | extension (x.1 * x.2) = extension x.1 * extension x.2}

case ih
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)
⊢ ∀ (a b : K), extension (↑a * ↑b) = extension ↑a * extension ↑b
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 | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo (- ·) ?_).mono' ?_, fun h ↦ (h.mapsTo (- ·) ?_).mono' ?_⟩

Goal state after:
case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ MapsTo (fun x ↦ -x) {x | -g ≤ x} {x | x ≤ g}

case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | -g ≤ x}, ∀ b ∈ {x | -g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 > x2) (fun x ↦ -x) a b

case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ -x) {x | x ≤ g} {x | -g ≤ x}

case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ -x) a b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
by
    rw [this, LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete]
    refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
    · exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero
    · intro a b
      rcases eq_or_ne a 0 with rfl | ha
      · simp [WithZero.withZeroUnitsEquiv]
      rcases eq_or_ne b 0 with rfl | hb
      · simp [WithZero.withZeroUnitsEquiv]
      simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]
    · exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)
    · intros
      rw [← WithZero.coe_le_coe]
      simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b

Tactic:
simp only [mem_sdiff, mem_ofPred_eq, mem_singleton_iff, gt_iff_lt, Function.onFun, and_imp]
    intro a _ _ b _ hb0
    refine inv_strictAnti₀ ?_
    simp [zero_lt_iff, hb0]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = (coeff d) p

pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0

Tactic:
coeff_X_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ((coeff (d, n).1) p * if (d, n).2 = n then 1 else 0) = (coeff d) p

case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

Tactic:
rintro ⟨i, j⟩ h1 h2

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (coeff (i, j).1) p * (coeff (i, j).2) (X ^ n) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (coeff (i, j).1) p * (coeff (i, j).2) (X ^ n) = 0

Tactic:
coeff_X_pow,

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ((coeff (i, j).1) p * if (i, j).2 = n then 1 else 0) = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = (coeff d) p

pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0

Tactic:
coeff_X_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (if (n, d).1 = n then 1 else 0) * (coeff (n, d).2) p = (coeff d) p

case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

Tactic:
rintro ⟨i, j⟩ h1 h2

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ (coeff (i, j).1) (X ^ n) * (coeff (i, j).2) p = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ (coeff (i, j).1) (X ^ n) * (coeff (i, j).2) p = 0

Tactic:
coeff_X_pow,

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ (if (i, j).1 = n then 1 else 0) * (coeff (i, j).2) p = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff x.1) p * (coeff x.2) (X ^ n) = 0

Tactic:
coeff_X_pow,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ((coeff x.1) p * if x.2 = n then 1 else 0) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1

Tactic:
by
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff x.1) (X ^ n) * (coeff x.2) p = 0

Tactic:
coeff_X_pow,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (if x.1 = n then 1 else 0) * (coeff x.2) p = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff d) (X ^ n * p) = if n ≤ d then (coeff (d - n)) p else 0

Tactic:
split_ifs with h
  · rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]
    simp
  · refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, zero_mul]
    have := mem_antidiagonal.mp hx
    rw [add_comm] at this
    exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
⊢ Function.Injective ⇑C

Tactic:
intro a b h

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
h : C a = C b
⊢ a = b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (∀ (n : σ →₀ ℕ), (coeff n) ((map f) φ) = (coeff n) 0) ↔ ∀ (n : σ →₀ ℕ), (coeff n) φ = (coeff n) 0

Tactic:
congr! with n

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
n : σ →₀ ℕ
⊢ (coeff n) ((map f) φ) = (coeff n) 0 ↔ (coeff n) φ = (coeff n) 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (coeff (i, j).1) (X s ^ n) * (coeff (i, j).2) φ = 0

Tactic:
coeff_X_pow,

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) φ = 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:
by
    intros
    ext
    exact mul_add _ _ _

Goal state after:
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
⊢ (coeff m) φ =
    (coeff (single s n, m - single s n).1) (X s ^ n) *
      (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

Tactic:
coeff_X_pow,

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
⊢ (coeff m) φ =
    (if (single s n, m - single s n).1 = single s n then 1 else 0) *
      (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ
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
a✝ : σ
⊢ (⇑(single s n + (i, j).2 - single s n) + ⇑(single s n)) a✝ = (⇑(single s n) + ⇑(i, j).2) a✝

Tactic:
Pi.add_apply,

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) a✝ + (single s n) a✝ = (⇑(single s n) + ⇑(i, j).2) a✝
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
a✝ : σ
⊢ (single s n + (i, j).2 - single s n) a✝ + (single s n) a✝ = (⇑(single s n) + ⇑(i, j).2) a✝

Tactic:
Pi.add_apply,

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) a✝ + (single s n) a✝ = (single s n) a✝ + (i, j).2 a✝
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : x = 0
⊢ (if h : (ofClass extensionValuation) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass extensionValuation) x) h, ⋯⟩) <
      valueGroup₀_equiv_extensionValuation ↑γ ↔
    extension x < ↑γ

Tactic:
simp only [hx0]
          rw [dif_pos (map_zero _)]
          · simp only [valueGroup₀_equiv_extensionValuation, valueGroup₀_hom_extensionValuation,
              MulEquiv.ofBijective_apply, coe_mk, ZeroHom.coe_mk]
            rw [Valuation.restrict_def, restrict₀_apply, dif_neg]
            · have hext : hv.extension 0 = 0 := by rw [extension_eq_zero_iff]
              simp [hext]
            · simp [← v.restrict.zero_iff, v.restrict_def,
                (restrict₀_surjective (.ofClass hv.v) _).choose_spec]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ ⊥ ≠ ⊤

Tactic:
rw [Ne, SetLike.ext_iff, not_forall]

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) 0) = 0

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) 0) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
a : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) ↑a) = ↑a

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
a : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) ↑a) = ↑a
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
y : (ofClass Valued.v).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) 0) = 0

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
y : (ofClass Valued.v).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) 0) = 0
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x✝¹ : ℕ∞ × ℕ∞
a b x✝ : ℕ∞
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, x✝)

Tactic:
| =>

Goal state after:
x✝¹ : ℕ∞ × ℕ∞
a b x✝ : ℕ∞
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, x✝)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x✝ : ℕ∞ × ℕ∞
a✝ b : ℕ∞
a : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ⊤)

Tactic:
| =>

Goal state after:
x✝ : ℕ∞ × ℕ∞
a✝ b : ℕ∞
a : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ⊤)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
y : (ofClass Valued.v).ValueGroup₀
b : ↥(ofClass Valued.v).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) ↑b) = ↑b

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
y : (ofClass Valued.v).ValueGroup₀
b : ↥(ofClass Valued.v).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) ↑b) = ↑b
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x✝ : ℕ∞ × ℕ∞
a✝ b✝ : ℕ∞
a b : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ↑b)

Tactic:
| =>

Goal state after:
x✝ : ℕ∞ × ℕ∞
a✝ b✝ : ℕ∞
a b : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ↑b)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a✝ b✝ : ℕ∞
h : a✝ ≠ ⊤ ∨ b✝ ≠ ⊤
a b : ℕ
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ↑b)

Tactic:
| =>

Goal state after:
a✝ b✝ : ℕ∞
h : a✝ ≠ ⊤ ∨ b✝ ≠ ⊤
a b : ℕ
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ↑b)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ⊤)

Tactic:
| =>

Goal state after:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ⊤)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a b✝ : ℕ∞
h : a ≠ ⊤ ∨ b✝ ≠ ⊤
b : ℕ
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (⊤, ↑b)

Tactic:
| =>

Goal state after:
a b✝ : ℕ∞
h : a ≠ ⊤ ∨ b✝ ≠ ⊤
b : ℕ
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (⊤, ↑b)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ 0 ≤ 0

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ 0 ≤ 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) ↑val✝ ↔ 0 ≤ ↑val✝

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) ↑val✝ ↔ 0 ≤ ↑val✝
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑val✝ ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ ↑val✝ ≤ 0

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑val✝ ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ ↑val✝ ≤ 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a✝ b✝ : (ofClass (valuation K v)).ValueGroup₀
a b : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑a ≤ (map' ↑(valueGroupEquiv K v)) ↑b ↔ ↑a ≤ ↑b

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a✝ b✝ : (ofClass (valuation K v)).ValueGroup₀
a b : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑a ≤ (map' ↑(valueGroupEquiv K v)) ↑b ↔ ↑a ≤ ↑b
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
g : (ofClass (valuation K v)).ValueGroup₀
⊢ embedding ((valueGroupOrderIso K v) 0) = embedding 0

Tactic:
| =>

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
g : (ofClass (valuation K v)).ValueGroup₀
⊢ embedding ((valueGroupOrderIso K v) 0) = embedding 0