mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / (P z * d) * (W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) - P x / P z ^ 2) + P y / P z ^ 3 =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) /
      (P z * d) ^ 3

Tactic:
toAffine_addX_of_eq hPz hd

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / (P z * d) *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2 - P x / P z ^ 2) +
      P y / P z ^ 3 =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) /
      (P z * d) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
· rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ x * ↑t * ↑v * ↑u ≤ᵥ 0 * (↑s * ↑v)

Tactic:
grw [veq_mul_right_comm x]

Goal state after:
case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ x * ↑v * ↑t * ↑u ≤ᵥ 0 * (↑s * ↑v)
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
⊢ {a | (valuation R) (a - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r)} ⊆ s

pp: case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
⊢ {z | v.restrict (z - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r)} ⊆ s

Tactic:
all_goals convert! hr; simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬ValueGroupWithZero.mk x y = ValueGroupWithZero.mk 0 1
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1

Tactic:
ValueGroupWithZero.mk_eq_mk

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬(x * ↑1 ≤ᵥ 0 * ↑y ∧ 0 * ↑y ≤ᵥ x * ↑1)
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : v r = 1
⊢ v.IsNontrivial

pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ v.IsNontrivial

Tactic:
· exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩

Goal state after:
case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ v.IsNontrivial
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑0)⁻¹ = ↑0⁻¹

Tactic:
inv_zero

Goal state after:
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑0)⁻¹ = ↑0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
a b : A
⊢ (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b

Tactic:
by
  rw [← not_vle, vle_iff_vle, not_vle]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ¬IsPrincipalIdealRing R
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
  rw [isPrincipalIdealRing_iff, not_forall]
  exact ⟨I, hI⟩

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
hval : v ((↑π₁)⁻¹ * ↑π₂) = 1
⊢ Associated π₁ π₂

Tactic:
set p : v.integer := ⟨(π₁.1 : K)⁻¹ * π₂.1, (v.mem_integer_iff _).mpr (le_of_eq hval)⟩ with hp

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
h2 : v.IsUniformizer ↑π₂
hval : v ((↑π₁)⁻¹ * ↑π₂) = 1
p : ↥v.integer := ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
hp : p = ⟨(↑π₁)⁻¹ * ↑π₂, ⋯⟩
⊢ Associated π₁ π₂
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A))
      ((algebraMap A K) ↑u * (algebraMap A K) (π ^ n) / ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
div_eq_mul_inv,

Goal state after:
case neg
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A))
      ((algebraMap A K) ↑u * (algebraMap A K) (π ^ n) * ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)⁻¹) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
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
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ ↑1
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n

Tactic:
div_eq_mul_inv,

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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n * ((maximalIdeal A).intValuation π ^ m)⁻¹ ≤ ↑1
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
have h_mn : m ≤ n := by
      have v_π_lt_one := (intValuation_lt_one_iff_dvd (maximalIdeal A) π).mpr
          (dvd_of_eq ((irreducible_iff_uniformizer _).mp hπ))
      have v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0 := intValuation_ne_zero _ _ hπ.ne_zero
      zify
      rw [← WithZero.coe_one, div_eq_mul_inv, ← zpow_natCast, ← zpow_natCast, ← ofAdd_zero,
        ← zpow_neg, ← zpow_add₀ v_π_ne_zero, ← sub_eq_add_neg] at H
      rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]

Goal state after:
case neg
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.e_a
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n / ((algebraMap A K) ↑w * (algebraMap A K) π ^ m)

Tactic:
div_eq_mul_inv,

Goal state after:
case h.e_a
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n * ((algebraMap A K) ↑w * (algebraMap A K) π ^ m)⁻¹
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

pp: case inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
ha' : a ≠ 0
⊢ ∃ n, a ^ n < ↑b

Tactic:
· use 1
    simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
ha' : a ≠ 0
⊢ ∃ n, a ^ n < ↑b
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
lift a to Gˣ using IsUnit.mk0 _ ha'
    simpa using! exists_pow_lt ha b

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₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ ∃ r, (algebraMap R K) r = W.Δ

Tactic:
use W_int.Δ

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K) W_int.Δ = W.Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
⊢ (valuation K (maximalIdeal R)) W.Δ ≤ 1

Tactic:
by
      choose r hr using Δ_integral_of_isIntegral R W
      rw [← hr]
      exact valuation_le_one (maximalIdeal R) r

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

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

Tactic:
· apply h
    simpa only [Finsupp.single_eq_same] using hm

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

Tactic:
Finsupp.single_eq_single_iff

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : s = t ∧ 1 = 1 ∨ 1 = 0 ∧ 1 = 0
h : 1 = 1
⊢ s = t
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
⊢ (coeff 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl

Goal state after:
case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
⊢ (coeff 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk v.asIdeal).factors)) = exp (-1)

Tactic:
Associates.count_self,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ exp (-↑1) = exp (-1)

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Irreducible (Associates.mk v.asIdeal)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ v.intValuation x = 1 ↔ x ∉ v.asIdeal

Tactic:
by
  refine ⟨fun h ↦ by simp [← (intValuation_lt_one_iff_mem _ _).not, h], fun h ↦ ?_⟩
  exact le_antisymm (v.intValuation_le_one x) <| by
    simp [← not_lt, (v.intValuation_lt_one_iff_mem _).not, h]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ n ∈ v.asIdeal.primeCompl

Tactic:
rw [← v.intValuation_eq_one_iff_mem_primeCompl]

Goal state after:
case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ v.intValuation n = 1
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) p) = (coeff x) p

Tactic:
simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset R s) p) = 0

Tactic:
simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
wlog H₁ : f.weightedOrder w < g.weightedOrder w

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
    weightedOrder w f ≠ weightedOrder w g →
      weightedOrder w f < weightedOrder w g → weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

σ✝ : Type u_1
R✝ : Type u_2
inst✝¹ : Semiring R✝
w✝ : σ✝ → ℕ
f✝ g✝ : MvPowerSeries σ✝ R✝
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n.succ) f = (trunc n) f + (Polynomial.monomial n) ((coeff n) f)

Tactic:
trunc_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m) ((coeff m) f) = (trunc n) f + (Polynomial.monomial n) ((coeff n) f)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    (trunc n) f + (Polynomial.monomial n) ((coeff n) f)

Tactic:
trunc_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    ∑ m ∈ Ico 0 n, (Polynomial.monomial m) ((coeff m) f) + (Polynomial.monomial n) ((coeff n) f)
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ = 𝔠

Tactic:
by
  apply le_antisymm
  · rw [← continuum_power_aleph0]
    exact power_le_power_right h₂
  · rw [← two_power_aleph0]
    exact power_le_power_right h₁

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case e'_3
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n ↦ f_max (n + 1)) = c / (1 - c)

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_3
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n ↦ f_max (n + 1)) = c * (1 - c)⁻¹
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s

Tactic:
term_of_ne_zero hn

Goal state after:
case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ f n / ↑n ^ s = f n / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
div_eq_mul_inv,

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n ↦ ‖↑C * (↑n ^ (s + (1 - ↑x)))⁻¹‖