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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 1 (E.a₂ + E'.a₂) (by simp) (by simp) one_ne_zero
  use ⟨1, 0, s, 0⟩
  ext
  · simp_rw [variableChange_a₁, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]
    linear_combination s * CharP.cast_eq_zero F 2
  · simp_rw [variableChange_a₂, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]
    linear_combination -hs + E.a₂ * CharP.cast_eq_zero F 2
  · simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]
    ring1
  · simp_rw [variableChange_a₄, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF,
      a₄_of_isCharTwoJNeZeroNF]
    ring1
  · simp_rw [variableChange_a₆, inv_one, Units.val_one, heq]
    ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₆ = 4 * W.a₆

Tactic:
rw [b₆, a₃_of_isCharTwoJNeZeroNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_ne_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
· have h := (C • E).j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
      rw [variableChange_j, heq, ← variableChange_j E' C',
        j_of_isCharTwoJEqZeroNF_of_char_two] at h
      exact False.elim (h rfl)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2
n✝ : ℕ
⊢ (W.ΨSq ↑n✝).coeff ((↑n✝).natAbs ^ 2 - 1) = ↑(↑n✝ ^ 2)

Tactic:
Int.cast_pow,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2
n✝ : ℕ
⊢ (W.ΨSq ↑n✝).coeff ((↑n✝).natAbs ^ 2 - 1) = ↑↑n✝ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

Tactic:
push_cast [hn, ΨSq_neg, ΨSq_one]

Goal state after:
case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0

Tactic:
push_cast [hn, ΨSq_neg, ΨSq_one]

Goal state after:
case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ 1 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : 0 = 0 ∧ 2 * 0 ≠ 0
⊢ False

Tactic:
eq_self,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : True ∧ 2 * 0 ≠ 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]

Tactic:
by
  have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n
  erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : n = 0
⊢ W.Φ n ≠ 0

pp: case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ W.Φ n ≠ 0

Tactic:
· simpa only [hn, Φ_zero] using one_ne_zero

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ W.Φ n ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.dblZ P ^ 2, W'.negAddY P (W'.neg P), addZ P (W'.neg P)] = -W'.dblZ P ^ 3

Tactic:
negAddY_neg hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.dblZ P ^ 2, W'.dblZ P ^ 3, addZ P (W'.neg P)] = -W'.dblZ P ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ toAffine W (W.add P Q) = 0

Tactic:
rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by_cases hs : 0 ∈ s

Goal state after:
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

case neg
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
have ht : 0 ∉ t := fun ht => disjoint_left.1 h₁ (subset_closure hs) ht

Goal state after:
case pos
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
ht : 0 ∉ t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
inst✝⁷ : ValuativeRel R
K : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : ValuativeRel K
Γ₀ : Type u_3
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝³ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝² : v.Compatible
inst✝¹ : TopologicalSpace K
inst✝ : IsValuativeTopology K
⊢ IsTopologicalRing R

Tactic:
convert! (ValuativeRel.nonarchimedeanRing R).toIsTopologicalRing

Goal state after:
R : Type u_1
inst✝⁸ : Ring R
inst✝⁷ : ValuativeRel R
K : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : ValuativeRel K
Γ₀ : Type u_3
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝³ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝² : v.Compatible
inst✝¹ : TopologicalSpace K
inst✝ : IsValuativeTopology K
⊢ _t = topologicalSpace R
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(inseparableSetoid α)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
by
    rw [inseparableSetoid_ring]; exact fun _ _ ↦ id

Goal state after:
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(inseparableSetoid α)) id id

Tactic:
by
    rw [inseparableSetoid_ring]; exact fun _ _ ↦ id

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
inst✝ : IsRankLeOne R
f : ValueGroupWithZero R →*₀ NNReal
hf : StrictMono ⇑f
⊢ MulArchimedean (ValueGroupWithZero R)

Tactic:
exact .comap f.toMonoidHom hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (- -((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z))) ^ 3

Tactic:
neg_neg,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q

Tactic:
simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_smul]
  ring1

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
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
⊢ ¬v ↑r = 0

Tactic:
zero_iff,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
⊢ ¬↑r = 0
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
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
have hvr : vr ∈ (valueGroup (.ofClass v)) := by
    apply mem_valueGroup
    rw [hvr_def, Units.val_mk0 hr₀]
    exact mem_range_self _

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
hvr : vr ∈ (MonoidWithZeroHom.ofClass v).valueGroup
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

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

Tactic:
simp [v]

Goal state after:
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 * π ^ n) / (algebraMap A K) (↑w * π ^ m)) ≤ 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:
mul_comm (w : A) _,

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 * π ^ n) / (algebraMap A K) (π ^ m * ↑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.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
⊢ UniformContinuous ⇑(RingHom.id R)

Tactic:
have h_val : ((Valued.mk' v).v).IsEquiv (Valued.mk' w).v := h

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
⊢ UniformContinuous ⇑(RingHom.id R)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
by
  suffices e 1 = 1 ∨ -e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]
  have he : ¬IsOfFinAddOrder (e 1) :=
    not_isOfFinAddOrder_of_isAddTorsionFree ((AddEquiv.map_ne_zero_iff e).mpr Int.one_ne_zero)
  rw [← AddSubgroup.zmultiples_eq_zmultiples_iff he]
  simpa [e.surjective, eq_comm] using (e : ℤ →+ ℤ).map_zmultiples 1

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 Γ₀
U : Set K
hU : IsClosed[hv.toTopologicalSpace] U
⊢ U.Nonempty → IsClosed (⇑v.restrict '' U)

Tactic:
hU'

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU : IsClosed[hv.toTopologicalSpace] U
hU' : U.Nonempty
⊢ IsClosed (⇑v.restrict '' U)
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
⊢ ∃ r, (algebraMap R K) r = W.Δ

Tactic:
by
  obtain ⟨W_int, hW_int⟩ : ∃ W_int : WeierstrassCurve R, W = W_int⁄K :=
    IsIntegral.integral
  use W_int.Δ
  rw [hW_int, baseChange, map_Δ]

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
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₁ : ↑y ∈ extension ⁻¹' {γ₀'}
hy₂ : ↑y ∈ s
⊢ v y = γ₀

Tactic:
simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₁

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : ↑y ∈ s
hy₁ : (restrict₀ (ofClass v)) y = γ₀'
⊢ v y = γ₀
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), (coeff n_1) (φ * (monomial n) a) = (coeff n_1) ((monomial n) a * φ)
m : σ →₀ ℕ
this : (coeff (m + n)) (φ * (monomial n) a) = (coeff (m + n)) ((monomial n) a * φ)
⊢ Commute ((coeff m) φ) a

Tactic:
coeff_add_mul_monomial,

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), (coeff n_1) (φ * (monomial n) a) = (coeff n_1) ((monomial n) a * φ)
m : σ →₀ ℕ
this : (coeff m) φ * a = (coeff (m + n)) ((monomial n) a * φ)
⊢ Commute ((coeff m) φ) a
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
  rw [← coeff_zero_C a, h, coeff_zero_C]

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

Goal state before:
pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ n + (single s n, j).2 s

Tactic:
exact Nat.le_add_right n _

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
a : R
σ : MvPowerSeries σ✝ A
⊢ a • σ = ((map (algebraMap R A)).comp C) a * σ

Tactic:
ext n
    simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ ((algebraMap A R) (a x) • MvPowerSeries.X x) ^ e x =
    (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x

Tactic:
MvPowerSeries.smul_eq_C_mul

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x =
    (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
⊢ (weightedHomogeneousComponent w p) f = 0

Tactic:
ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · rw [coeff_zero]
    apply coeff_eq_zero_of_lt_weightedOrder w
    rw [hd]
    exact hf
  · rw [map_zero]

Goal state after:
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
a : adicCompletion K v
ha : 1 < Valued.v a
hϖ : v.intValuation 0 = exp (-1)
this : Valued.v ((algebraMap R (adicCompletion K v)) 0) = (exp 1)⁻¹
⊢ False

Tactic:
simp [exp_ne_zero.symm] at hϖ

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
intro i hi
    rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

Tactic:
· rw [coeff_of_lt_order i hi, zero_mul]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i : Set (σ →₀ ℕ) × TwoSidedIdeal R),
    i.1.Finite ∧ ↑i.2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ i.1.pi fun x ↦ ↑i.2

Tactic:
intro ⟨D, I⟩ ⟨hD, hI⟩

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
⊢ ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x ↦ ↑(D, I).2
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
f : Polynomial R
⊢ MvPowerSeries.eval₂ φ (fun x ↦ a)
      ↑((MvPolynomial.uniqueAlgEquiv R Unit) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)) =
    MvPolynomial.eval₂ φ (fun x ↦ a) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)

Tactic:
rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]

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

Goal state before:
pp: case h
σ : Type u_1
R : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : UniformSpace R
S : Type u_3
inst✝¹⁵ : CommRing S
inst✝¹⁴ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (⇑ε ∘ eval₂ φ a) ↑p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p

Tactic:
intro p
    simp only [Function.comp_apply, eval₂_coe]
    rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]

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

Goal state before:
pp: case e'_8
σ : Type u_1
R : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : UniformSpace R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : UniformSpace S
a : σ → S
inst✝¹⁷ : IsTopologicalSemiring R
inst✝¹⁶ : IsUniformAddGroup R
inst✝¹⁵ : IsUniformAddGroup S
inst✝¹⁴ : CompleteSpace S
inst✝¹³ : T2Space S
inst✝¹² : IsTopologicalRing S
inst✝¹¹ : IsLinearTopology S S
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ (↑ε).comp (algebraMap R S) = algebraMap R T

Tactic:
simp only [AlgHom.comp_algebraMap_of_tower]

Goal state after: