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✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
h : ↑E.Δ' ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
rw [E.coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff, neg_ne_zero,
    pow_ne_zero_iff three_ne_zero] at h

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
h : E.a₂ ≠ 0 ∧ E.a₆ ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
h : E'.a₂ ≠ 0 ∧ E'.a₆ ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨ha₂', ha₆'⟩ := h

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Equation P ↔ W'.Equation Q

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m ↦ m • Q) u) ↔ W'.Equation Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
⊢ ∃ C, C • E = E'

pp: case neg
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
⊢ ∃ C, C • E = E'

Tactic:
· have ha₄ := E.Δ'.ne_zero
    rw [coe_Δ', Δ_of_isShortNF, ha₆, zero_pow two_ne_zero, mul_zero, add_zero, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff three_ne_zero] at ha₄
    replace ha₄ := ha₄.2
    have ha₆' : E'.a₆ = 0 := by
      rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq
      exact (pow_eq_zero_iff two_ne_zero).1 <| heq.resolve_left <| pow_ne_zero 3 ha₄
    have ha₄' := E'.Δ'.ne_zero
    rw [coe_Δ', Δ_of_isShortNF, ha₆', zero_pow two_ne_zero, mul_zero, add_zero, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff three_ne_zero] at ha₄'
    replace ha₄' := ha₄'.2
    obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₄ / E'.a₄) 4
    have hu0 : u ≠ 0 := by
      rw [← pow_ne_zero_iff four_ne_zero, hu, div_ne_zero_iff]
      exact ⟨ha₄, ha₄'⟩
    use ⟨Units.mk0 u hu0, 0, 0, 0⟩
    ext
    · simp [variableChange_a₁]
    · simp [variableChange_a₂]
    · simp [variableChange_a₃]
    · simp_rw [variableChange_a₄, a₁_of_isShortNF, a₂_of_isShortNF, a₃_of_isShortNF,
        Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu]
      simp [field]
    · simp [ha₆, ha₆', variableChange_a₆]

Goal state after:
case neg
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Nonsingular ((fun m ↦ m • Q) u) ↔ W'.Nonsingular Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
case refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
Q : Fin 3 → F
hQ : W.Nonsingular Q
u : Fˣ
hP : W.Nonsingular ((fun m ↦ m • Q) u)
⊢ ⇑f ∘ (fun m ↦ m • Q) u ≈ ⇑f ∘ Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Equation (⇑f ∘ P) ↔ (W'⁄A).Equation P

Tactic:
← RingHom.coe_coe,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Equation (⇑↑f ∘ P) ↔ (W'⁄A).Equation P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
← RingHom.coe_coe,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑↑f ∘ P) ↔ (W'⁄A).Nonsingular P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.neg ((fun m ↦ m • Q) u) ≈ W'.neg Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
          2 * P x * (P y - W'.negY P) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0

Tactic:
dblU_of_Z_eq_zero hPz,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
          2 * P x * (P y - W'.negY P) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0

Tactic:
dblU_of_Z_eq_zero hPz,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : A
y : ↥S
⊢ ↑v.toMonoidWithZeroHom x * ↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom).domRestrict S) ⋯) y)⁻¹ = v x * (v ↑y)⁻¹

Tactic:
by simp [IsUnit.coe_liftRight]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} ⊆ s

Tactic:
suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i) by
        rw [h]
        assumption

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun y ↦ a + y) '' ↑(B i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
Q : Fin 3 → F
u : Fˣ
⊢ toAffine W ((fun m ↦ m • Q) u) = toAffine W Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]

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

Goal state before:
pp: case pos
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)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W
      (W.dblZ P •
        ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
            (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
          W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
            (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
          1]) =
    toAffine W P + toAffine W Q

Tactic:
toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx

Goal state after:
case pos
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)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑f ∘ P) = ⇑f ∘ (W'⁄A).neg P

Tactic:
← RingHom.coe_coe,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑↑f ∘ P) = ⇑↑f ∘ (W'⁄A).neg P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'⁄F).add P Q

Tactic:
← RingHom.coe_coe,

Goal state after:
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add (⇑↑f ∘ P) (⇑↑f ∘ Q) = ⇑↑f ∘ (W'⁄F).add P Q
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
toUniformSpace_eq,

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
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 : R
h : 1 ≤ ValueGroupWithZero.mk 0 1
⊢ False

Tactic:
← ValueGroupWithZero.mk_one_one,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
h : ValueGroupWithZero.mk 1 1 ≤ ValueGroupWithZero.mk 0 1
⊢ False
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 : ¬x ≤ᵥ 0
⊢ ValueGroupWithZero.mk x y * ValueGroupWithZero.mk ↑y ⟨x, h⟩ = 1

Tactic:
← ValueGroupWithZero.mk_one_one,

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 ≤ᵥ 0
⊢ ValueGroupWithZero.mk x y * ValueGroupWithZero.mk ↑y ⟨x, h⟩ = ValueGroupWithZero.mk 1 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x y : R
⊢ x ≤ᵥ y ∧ y ≤ᵥ x ↔ v x = v y

Tactic:
vle_iff_le v,

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x y : R
⊢ v x ≤ v y ∧ v y ≤ v x ↔ v x = v y
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClosed[_t] {x | v.restrict x < r}

Tactic:
exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _)

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ ∀ (x y : β), ⋯.extend (⇑f) (x * y) = ⋯.extend (⇑f) x * ⋯.extend (⇑f) y

Tactic:
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous

Goal state after:
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
⊢ ∀ (x y : β), ⋯.extend (⇑f) (x * y) = ⋯.extend (⇑f) x * ⋯.extend (⇑f) y
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ ∀ (x y : β), ⋯.extend (⇑f) (x + y) = ⋯.extend (⇑f) x + ⋯.extend (⇑f) y

Tactic:
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous

Goal state after:
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
⊢ ∀ (x y : β), ⋯.extend (⇑f) (x + y) = ⋯.extend (⇑f) x + ⋯.extend (⇑f) y
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
⊢ ∀ ⦃x : hat K⦄, x ≠ 0 → ContinuousAt Inv.inv x

Tactic:
intro x x_ne
      have : { y | hatInv y = y⁻¹ } ∈ 𝓝 x :=
        haveI : {(0 : hat K)}ᶜ ⊆ { y : hat K | hatInv y = y⁻¹ } := by
          intro y y_ne
          rw [mem_compl_singleton_iff] at y_ne
          dsimp [Inv.inv]
          rw [if_neg y_ne]
        mem_of_superset (compl_singleton_mem_nhds x_ne) this
      exact ContinuousAt.congr (continuous_hatInv x_ne) this

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

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
⊢ False

Tactic:
have hvalueGroup : valueGroup (.ofClass v) = ⊥ := by
    simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]
    intro y x
    specialize h1 x
    aesop

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
hvalueGroup : (MonoidWithZeroHom.ofClass v).valueGroup = ⊥
⊢ False
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 ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v.IsUniformizer ↑π₂

Tactic:
rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]

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 Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
⊢ v.IsUniformizer ↑r

Tactic:
have hr₀ : r ≠ 0 := by
    intro h
    rw [h, Set.singleton_zero, span_zero] at hr
    exact Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
⊢ v.IsUniformizer ↑r
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negY (⇑f ∘ P) = f ((W'⁄A).negY P)

Tactic:
← RingHom.coe_coe,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).negY (⇑↑f ∘ P) = ↑f ((W'⁄A).negY P)