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

Goal state before:
pp: case refine_1
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : F
⊢ ⟨v x, ⋯⟩ ∈ {x | x ≤ 1} → ↑⟨v x, ⋯⟩ ∈ Set.range (⇑v ∘ ⇑(algebraMap O F))

Tactic:
simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_ofPred_eq, Set.mem_range,
      Function.comp_apply]

Goal state after:
case refine_1
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : F
⊢ v x ≤ 1 → ∃ y, v ((algebraMap O F) y) = v x
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ v ((algebraMap O F) y) = v ((algebraMap O F) y)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : K →+* ℂ
⊢ conjugate (conjugate x✝) = x✝

Tactic:
simp

Goal state after:
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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: case mpr
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im ≠ 0 →
    ∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z

Tactic:
rintro ⟨hz1, hz2⟩

Goal state after:
case mpr
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im ≠ 0
⊢ ∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
x✝ : K
⊢ φ x✝ = ((φ.comp ↑f).comp f.symm.toRingHom) x✝

Tactic:
simp

Goal state after:
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
⊢ Rat.ofInt (-1) ∈ ratLt 0

Tactic:
simp

Goal state after:
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
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n + 1 ≠ 0

Tactic:
simp

Goal state after:
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
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
simp

Goal state after:
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
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n < n + 1

Tactic:
simp

Goal state after:
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 ℝ := ⋯
he : StrictMono ⇑e
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑1).log) ⋯) ⋯) = ↑↑1

Tactic:
simp

Goal state after:
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:
Finset.coe_sort_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
⊢ Fintype.card ↥(p.aroots ℂ).toFinset = p.natDegree
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h3.a
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 := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ?h3.n + ((galActionHom p ℂ) conj').support.card = ?h3.n + 2

pp: case h3.n
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 := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ℕ

Tactic:
rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]

Goal state after:
case h3.a
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.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) conj').support.card = (p.rootSet ℂ).toFinset.card
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = X ^ 2 - C ↑(2 * z.re) * X + C (↑‖z‖ ^ 2)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
⊢ (valueGroup₀_equiv_withZeroMulInt v) 0 = 0

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : ¬IsNontrivial R
⊢ IsRankLeOne R

Tactic:
· refine ⟨⟨{ emb := 1, strictMono := ?_ }⟩⟩
      intro a b
      contrapose! H
      obtain ⟨H, H'⟩ := H
      rcases eq_or_ne a 0 with rfl | ha
      · simp_all
      rcases eq_or_ne a 1 with rfl | ha'
      · exact ⟨⟨b, (H.trans' zero_lt_one).ne', H.ne'⟩⟩
      · exact ⟨⟨a, ha, ha'⟩⟩

Goal state after:
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)
⊢ n + 1 ≠ 0

Tactic:
simp

Goal state after:
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)
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
simp

Goal state after:
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)
⊢ n < n + 1

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) (x + y) = dist 0 (x + y)

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
⊢ ‖x ^ 0‖₊ ≤ ‖x‖₊

Tactic:
simp

Goal state after:
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
⊢ ‖∏ i ∈ ∅, f i‖₊ ≤ ∅.sup fun x ↦ ‖f x‖₊

Tactic:
simp

Goal state after:
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
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (∅.Nonempty → i ∈ ∅) ∧ ‖∏ j ∈ ∅, f j‖ ≤ ‖f i‖

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
⊢ ∃ i, (0 ≠ 0 → i ∈ 0) ∧ ‖(Multiset.map f 0).prod‖ ≤ ‖f i‖

Tactic:
simp

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

Goal state before:
pp: M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ a ::ₘ t ≠ 0 → a ∈ a ::ₘ t

Tactic:
simp

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

Goal state before:
pp: case pos
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))

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

Goal state before:
pp: M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : 0 ≠ 0 → M ∈ 0
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ a ::ₘ 0 ≠ 0 → a ∈ a ::ₘ 0

Tactic:
simp

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

Goal state before:
pp: M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : 0 ≠ 0 → M ∈ 0
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f a‖

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
⊢ valuation.restrict 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hs : (↑∅).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
⊢ ‖∏ i ∈ ∅, f i‖₊ = ∅.sup fun i ↦ ‖f i‖₊

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 : ((↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊) → ‖∏ 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
⊢ ↑s ⊆ ↑(Finset.cons a s ha)

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (p, q) ∈ Finset.antidiagonal (p + q)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K✝ : Type u_1
hK : NormedField K✝
inst✝² : IsUltrametricDist K✝
K : Type u_2
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
h : 1 < ‖x‖
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: case h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ (e, 0) ∉ antidiagonal e → (coeff (e, 0).1) x * (coeff (e, 0).2) φ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ (RankOne.hom v) 0 < (RankOne.hom v) ↑ε

Tactic:
exact hv.strictMono _ (Units.zero_lt ε)

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

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
ψ : MvPowerSeries σ R
⊢ (0 * ψ).lexOrder = lexOrder 0 + ψ.lexOrder

Tactic:
simp

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

Goal state before:
pp: case inr.inl
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ (φ * 0).lexOrder = φ.lexOrder + lexOrder 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
k : Type u_3
inst✝ : Field k
⊢ constantCoeff 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ (C 0)⁻¹ = C 0⁻¹

Tactic:
simp

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

Goal state before:
pp: case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
⊢ weightedOrder w (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, weightedOrder w (f i)

Tactic:
simp

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
⊢ f ≠ 0 → ∃ n, Associated (X ^ n) f

Tactic:
hf

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ∃ n, Associated (X ^ n) f
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : IsDedekindDomain R
inst✝¹ : IsFractionRing R K
v✝ : HeightOneSpectrum R
inst✝ : NumberField K
v : FinitePlace K
⊢ ∀ {a : K}, v a = 0 → a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
by
  by_cases h3 : (3 : F) = 0
  · exact ofJ_1728_of_three_eq_zero h3
  · rw [ofJ, show (1728 : F) = 2 ^ 6 * 3 ^ 3 by norm_num1,
      if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)), if_pos rfl]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).IsElliptic

pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic

Tactic:
· have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
      rw [h0, ofJ_0_of_three_eq_zero h3]
      infer_instance

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
i : J.L
x : c.pt
⊢ (ConcreteCategory.hom (c.ι i)) ((sectionsEquiv hc) ((sectionsEquiv hc).symm x)) = ((sectionsEquiv hc).symm x).val i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]

Tactic:
← negY_of_Z_ne_zero hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * W'.neg P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * W'.neg P z ^ 2 - W'.negY P ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * W'.neg P z ^ 2 -
                  W'.a₁ * P x * W'.negY P * P z ^ 2 -
                W'.a₂ * P x ^ 2 * W'.neg P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * W'.neg P z ^ 2 -
          W'.a₃ * W'.negY P * P z ^ 2 * W'.neg P z -
        W'.a₄ * P x * P z * W'.neg P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * W'.neg P z =
    0

Tactic:
neg_Z,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 - W'.negY P ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * W'.negY P * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * W'.negY P * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * W'.negY P ^ 2 * P z + P x * P y ^ 2 * W'.neg P z - 2 * P x * P y * W'.negY P * W'.neg P z +
                              2 * P x * P y * W'.negY P * P z -
                            W'.a₁ * P x ^ 2 * W'.negY P * W'.neg P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * W'.neg P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * W'.neg P z ^ 2 +
                  W'.a₃ * P x * W'.negY P * P z ^ 2 -
                2 * W'.a₃ * P x * W'.negY P * P z * W'.neg P z +
              2 * W'.a₃ * P x * P y * P z * W'.neg P z +
            W'.a₄ * P x ^ 2 * W'.neg P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * W'.neg P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * W'.neg P z =
    0

Tactic:
neg_Z,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * W'.negY P ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * W'.negY P * P z + 2 * P x * P y * W'.negY P * P z -
                            W'.a₁ * P x ^ 2 * W'.negY P * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * W'.negY P * P z ^ 2 -
                2 * W'.a₃ * P x * W'.negY P * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
x✝ : Fin 3
⊢ (⇑f ∘ (u • P)) x✝ = (f u • ⇑f ∘ P) x✝

Tactic:
simp

Goal state after: