mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ (conjugate φ) x = (φ.comp ↑σ.symm) x

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
x : K
⊢ (starRingEnd ℂ) (φ x) = φ (σ.symm x)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a✝ : K
⊢ (σ ^ 2) a✝ = 1 a✝

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a✝ : K
⊢ σ (σ a✝) = a✝
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
this : num • 1 < den • x → num ≤ ↑n * ↑den
⊢ { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ } ∈ {r | r.num • 1 < r.den • x} →
    { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ }.num * ↑(↑n).den ≤
      (↑n).num * ↑{ num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ }.den

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
this : num • 1 < den • x → num ≤ ↑n * ↑den
⊢ num • 1 < den • x → num ≤ ↑n * ↑den
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
h : num • 1 < den • x
⊢ x ≤ ↑n • 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
h : num • 1 < den • x
⊢ x ≤ n • 1
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
this : -(n • 1) < x
⊢ Rat.ofInt (-↑n) ∈ ratLt x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
this : -(n • 1) < x
⊢ -(n • 1) < x
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
⊢ -x < -x - x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
⊢ x < 0
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case h
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ { num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } ∈ ratLt x

Tactic:
simpa using

Goal state after:
case h
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ 1 < (n + 1) • x
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_1
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ m • 1 < k • a.den • x

Tactic:
simpa using

Goal state after:
case mp.refine_1
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ m • 1 < k • a.den • x
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Fintype.card ↥(p.aroots ℂ).toFinset = p.natDegree

Tactic:
Fintype.card_coe

Goal state after:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ (p.aroots ℂ).toFinset.card = p.natDegree
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
a b : (ofClass v).ValueGroup₀ˣ
h : a < b
⊢ (rf.comp e) a < (rf.comp e) b

Tactic:
simpa using

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
a b : (ofClass v).ValueGroup₀ˣ
h : a < b
⊢ e a < e b
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ m • 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ m • 1
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ p.natDegree ∣ Fintype.card ↥(galActionHom p ℂ).range

Tactic:
simpa using

Goal state after:
case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ p.natDegree ∣ Nat.card p.Gal
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
this : ∀ (y : ℚ), y.num • 1 < 0 → ↑y = x → x ≤ 0
⊢ x ∈ ⇑(Rat.castHom ℝ) '' {r | r.num • 1 < r.den • 0} → x ≤ 0

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
this : ∀ (y : ℚ), y.num • 1 < 0 → ↑y = x → x ≤ 0
⊢ ∀ (x_1 : ℚ), x_1.num • 1 < 0 → ↑x_1 = x → x ≤ 0
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
this : (∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x) → 0 ≤ x
⊢ (∀ x_1 ∈ ratLt' 0, x_1 ≤ x) → 0 ≤ x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
this : (∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x) → 0 ≤ x
⊢ (∀ (a : ℚ), a.num • 1 < 0 → ↑a ≤ x) → 0 ≤ x
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∃ x, x ≠ 0 ∧ (hom v) (v.restrict x) < γ

Tactic:
have hγ_pos : 0 < γ := pos_iff_ne_zero.mpr hγ
  obtain ⟨x, h⟩ := NNReal.exists_lt_of_strictMono (RankOne.strictMono v.restrict) hγ_pos
  obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val
  refine ⟨k, ?_, ?_⟩
  · simp only [restrict₀_apply, MonoidWithZeroHom.coe_ofClass, restrict_def, map_eq_zero,
      dite_eq_left_iff, coe_ne_zero, imp_false, not_not] at hk
    by_contra h0
    rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk
    simp at hk
  · convert! h
    simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]
    congr 1
    exact (embedding_restrict₀ k).symm

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ C p.leadingCoeff⁻¹ ≠ 0

Tactic:
simpa using

Goal state after:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ ¬p = 0
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
y : ℚ
hy : y < 0
⊢ y.num < 0

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
y : ℚ
hy : y < 0
⊢ y < 0
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
h' : x < 0
y : ℚ
hxy : x < ↑y
hy : ↑y < 0
⊢ y < 0

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
h' : x < 0
y : ℚ
hxy : x < ↑y
hy : ↑y < 0
⊢ y < 0
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: Γ₀ : Type u_2
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : MulArchimedean Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsRankLeOne R

Tactic:
rw [isRankLeOne_iff_mulArchimedean]
  exact MulArchimedean.comap (embedding.toMonoidHom.comp (ValueGroupWithZero.embed v).toMonoidHom)
    (embedding_strictMono.comp (ValueGroupWithZero.embed_strictMono v))

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
max_eq_right h.le

Goal state after:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y z ≤ dist x z
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ ¬dist y z ≤ dist y x

Tactic:
simpa using

Goal state after:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y x < dist y z
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ ¬dist y x ≤ dist y z

Tactic:
simpa using

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist y z < dist y x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
r s : ℝ
p : X → Prop
x✝² x✝¹ x✝ : Subtype p
⊢ dist x✝² x✝ ≤ max (dist x✝² x✝¹) (dist x✝¹ x✝)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
r s : ℝ
p : X → Prop
x✝² x✝¹ x✝ : Subtype p
⊢ dist ↑x✝² ↑x✝ ≤ dist ↑x✝² ↑x✝¹ ∨ dist ↑x✝² ↑x✝ ≤ dist ↑x✝¹ ↑x✝
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ ↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } ∈ ratLt' (y - x)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ 1 < (n + 1) • (y - x)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
this : ∀ (x : ℚ), x.num • 1 < ↑x.den • 1 → ↑x ≤ 1
⊢ ∀ b ∈ ratLt' 1, b ≤ 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
this : ∀ (x : ℚ), x.num • 1 < ↑x.den • 1 → ↑x ≤ 1
⊢ ∀ (a : ℚ), a.num • 1 < a.den • 1 → ↑a ≤ 1
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℚ
hx : x.num • 1 < ↑x.den • 1
⊢ x ≤ 1

Tactic:
simpa using

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℚ
hx : x.num • 1 < ↑x.den • 1
⊢ x.num ≤ ↑x.den
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
this : ∀ (x : ℝ), (∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x) → 1 ≤ x
⊢ ∀ (b : ℝ), (∀ x ∈ ratLt' 1, x ≤ b) → 1 ≤ b

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
this : ∀ (x : ℝ), (∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x) → 1 ≤ x
⊢ ∀ (b : ℝ), (∀ (a : ℚ), a.num • 1 < a.den • 1 → ↑a ≤ b) → 1 ≤ b
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
y : ℚ
hy : y < 1
⊢ y.num < ↑y.den

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
y : ℚ
hy : y < 1
⊢ y.num < ↑y.den
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
h' : x < 1
y : ℚ
hxy : x < ↑y
hy : ↑y < 1
⊢ ∃ y < 1, x < ↑y

Tactic:
exact ⟨y, (by norm_cast at hy), hxy⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
⊢ ‖x * y‖ ≤ max ‖x‖ ‖y‖

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
⊢ ‖x * y‖ ≤ ‖x‖ ∨ ‖x * y‖ ≤ ‖y‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S' : Type u_2
inst✝ : SeminormedGroup S'
h : ∀ (x y : S'), ‖x * y‖ ≤ max ‖x‖ ‖y‖
x y z : S'
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simpa using

Goal state after:
S' : Type u_2
inst✝ : SeminormedGroup S'
h : ∀ (x y : S'), ‖x * y‖ ≤ max ‖x‖ ‖y‖
x y z : S'
⊢ ‖x⁻¹ * z‖ ≤ ‖x⁻¹ * y‖ ∨ ‖x⁻¹ * z‖ ≤ ‖y⁻¹ * z‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
⊢ IsNonarchimedean fun x ↦ ↑‖x‖₊

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
⊢ IsNonarchimedean fun x ↦ ‖x‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y z : S
h : ‖x / y‖ ≠ ‖y / z‖
⊢ ‖x / z‖ = max ‖x / y‖ ‖y / z‖

Tactic:
simpa using

Goal state after:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y z : S
h : ‖x / y‖ ≠ ‖y / z‖
⊢ ‖x / z‖ = max ‖x / y‖ ‖y / z‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case succ
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
n : ℕ
hn : ‖x ^ n‖₊ ≤ ‖x‖₊
⊢ ‖x ^ (n + 1)‖₊ ≤ ‖x‖₊

Tactic:
simpa using

Goal state after:
case succ
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
n : ℕ
hn : ‖x ^ n‖₊ ≤ ‖x‖₊
⊢ ‖x ^ n * x‖₊ ≤ ‖x‖₊
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case ofNat
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.ofNat a✝‖₊ ≤ ‖x‖₊

Tactic:
simpa using

Goal state after:
case ofNat
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ a✝‖₊ ≤ ‖x‖₊
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case negSucc
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.negSucc a✝‖₊ ≤ ‖x‖₊

Tactic:
simpa using

Goal state after:
case negSucc
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ (a✝ + 1)‖₊ ≤ ‖x‖₊
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
⊢ ∀ U ∈ nhds 1, ∃ V, ↑V ⊆ U

Tactic:
simpa using

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
⊢ ∀ (U : Set M), (∃ ε > 0, ball 1 ε ⊆ U) → ∃ V, ↑V ⊆ U
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖∏ i ∈ t, f i‖ ≤ ‖f j‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

pp: case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖f j‖ ≤ ‖∏ i ∈ t, f i‖
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
· exact (norm_mul_le_max _ _).trans (max_eq_left h).le

Goal state after:
case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖f j‖ ≤ ‖∏ i ∈ t, f i‖
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖₊ ≤ ⨆ i, ‖f i‖₊

Tactic:
simpa using

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
simpa using

Goal state after:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : IsEmpty ι
⊢ 0 ≤ C
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
⊢ ∃ j ∈ s, ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊

Tactic:
simpa using

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
⊢ ∃ j ∈ s, (s.sup fun i ↦ ‖f i‖₊) = ‖f j‖₊