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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂);
  y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)

Tactic:
simp_rw [addY, negY, eq_div_iff (sub_ne_zero.mpr hx.symm)]
  linear_combination (norm := ring1) 2 * cyclic_sum_Y_mul_X_sub_X y₁ y₂ hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
⊢ c.π.app k ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ U

Tactic:
rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
J : Type u_1
U : J → c.pt.Opens
hU✝ : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
this : CompactSpace ↥c.pt
s : Finset J
hs : Set.univ ⊆ ⋃ i ∈ s, ↑(U i)
hU : IsOpenCover fun j ↦ U ↑j
i : I
V : ↥s → (D.obj i).Opens
hV : IsOpenCover V
heq : ∀ (j : ↥s), IsAffineOpen (V j) ∧ U ↑j = c.π.app i ⁻¹ᵁ V j
⊢ ∃ i s V, IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U ↑j = c.π.app i ⁻¹ᵁ V j

Tactic:
use i, s, V, hV

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.coeff W.Ψ₂Sq.natDegree = 4

Tactic:
W.natDegree_Ψ₂Sq h,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.coeff 3 = 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ (W.toCharNeTwoNF • W).a₂ = W.b₂

Tactic:
toCharNeTwoNF,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ ({ u := 1, r := 0, s := 2 * -W.a₁, t := 2 * -W.a₃ } • W).a₂ = W.b₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      (W.preΨ' (m + 1) * W.preΨ' (m + 3)).coeff (expDegree (m + 1) + expDegree (m + 3)) *
        (W.preΨ' (m + 4) ^ 2).coeff (2 * expDegree (m + 4)) =
    ↑(expCoeff (2 * (m + 3)))

Tactic:
cm h₁.1 h₃.1,

Goal state after:
case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) * (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) *
        (W.preΨ' (m + 4) ^ 2).coeff (2 * expDegree (m + 4)) =
    ↑(expCoeff (2 * (m + 3)))
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.IsShortNF
inst✝ : E'.IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
have ha₄ := E.Δ'.ne_zero
  rw [E.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_ne_zero] at ha₄
  have ha₄' := E'.Δ'.ne_zero
  rw [E'.coe_Δ', Δ_of_isShortNF_of_char_three, neg_ne_zero, pow_ne_zero_iff three_ne_zero] at ha₄'
  have : NeZero (4 : F) := NeZero.mk <| by
    rw [show (4 : F) = 1 by linear_combination CharP.cast_eq_zero F 3]
    exact one_ne_zero
  obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₄ / E'.a₄) 4
  obtain ⟨r, hr⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 3 3
    1 _ (E.a₆ - u ^ 6 * E'.a₆) (by simp) (by simp) ha₄
  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, r, 0, 0⟩
  ext
  · simp_rw [variableChange_a₁, a₁_of_isShortNF]
    ring1
  · simp_rw [variableChange_a₂, a₁_of_isShortNF, a₂_of_isShortNF,
      show (3 : F) = 0 from CharP.cast_eq_zero F 3]
    ring1
  · simp_rw [variableChange_a₃, a₁_of_isShortNF, a₃_of_isShortNF]
    ring1
  · 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,
      show (3 : F) = 0 from CharP.cast_eq_zero F 3]
    simp [field]
  · 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]
    simp [field]
    linear_combination hr

Goal state after:
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
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 :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
⊢ 47775744 ≠ 0

Tactic:
have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)

Goal state after:
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 :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : 2 ^ 16 * 3 ^ 6 ≠ 0
⊢ 47775744 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : Even n
⊢ 2 ≤ n ^ 2 - 4

Tactic:
exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
h✝ : ¬Even n
⊢ 2 ≤ n ^ 2 - 1

Tactic:
exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
this :
  ∀ (j₁ j₂ : ↥s),
    ∃ l flk,
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
⊢ ∃ l flk,
    ∀ (j₁ j₂ : ↥s),
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂

Tactic:
choose l flk hflk using this

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
⊢ ∃ l flk,
    ∀ (j₁ j₂ : ↥s),
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
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
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P x ≠ 0

Tactic:
by
  intro hPx
  simp only [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPx, mul_zero, zero_mul,
    zero_pow <| OfNat.ofNat_ne_zero _, ne_self_iff_false, or_false, false_or] at hP
  rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
⊢ Nonempty (IsColimit ((yoneda.obj X).mapCocone c))

Tactic:
rw [Limits.Types.isColimit_iff_coconeTypesIsColimit]

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
⊢ ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).IsColimit
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case coe.zero
e : ℝ≥0
he : 1 < e
a✝ : Multiplicative ℤ
⊢ 0 < ↑a✝ → (toNNReal ⋯) 0 < (toNNReal ⋯) ↑a✝

pp: case coe.coe
e : ℝ≥0
he : 1 < e
a✝¹ a✝ : Multiplicative ℤ
⊢ ↑a✝ < ↑a✝¹ → (toNNReal ⋯) ↑a✝ < (toNNReal ⋯) ↑a✝¹

Tactic:
· simpa using! zpow_pos he.pos _

Goal state after:
case coe.coe
e : ℝ≥0
he : 1 < e
a✝¹ a✝ : Multiplicative ℤ
⊢ ↑a✝ < ↑a✝¹ → (toNNReal ⋯) ↑a✝ < (toNNReal ⋯) ↑a✝¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
simp only [negDblY, dblU_smul, dblX_smul, negY_smul, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.dblU P) * ((u ^ 4) ^ 2 * W'.dblX P - u ^ 2 * P x * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2) +
      u ^ 3 * P y * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)
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
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u ^ 4 • W'.dblXYZ P = u ^ 4 • W'.add P Q

Tactic:
add_of_equiv h

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u ^ 4 • W'.dblXYZ P = u ^ 4 • W'.dblXYZ P
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z ∈ {U | ∃ i, U = ↑(B i)}, z ⊆ ↑(B i) ∩ ↑(B j)

Tactic:
use B k

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V * V ⊆ ↑(B i)

Tactic:
use B k

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) * ↑(B k) ⊆ ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)
⊢ ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)

Tactic:
use B k

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)
⊢ ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)

Tactic:
use B k

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z ∈ {U | ∃ i, U = ↑(B i)}, z ⊆ ↑(B i) ∩ ↑(B j)

Tactic:
use B k

Goal state after:
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
⊢ 0 ≤ᵥ x

Tactic:
by
  simpa using mul_vle_mul_left ((vle_total 0 1).resolve_right not_vle_one_zero) x

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : (ofClass v).ValueGroup₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : v.restrict r < ↑γ₀
s : R
s_in : v.restrict s < ↑γ₀
⊢ v.restrict r * v.restrict s < ↑γ₀ * ↑γ₀

Tactic:
by gcongr <;> exact zero_le

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

Goal state before:
pp: case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 ((0, 0).1 * (0, 0).2))

Tactic:
rw [zero_mul]

Goal state after:
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Tactic:
rw [addX_eq' hP hQ, addZ_of_X_eq hx]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
          W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
        P x * Q z ^ 2 * 0 ^ 2 -
      Q x * P z ^ 2 * 0 ^ 2 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : IsUniformAddGroup β
⊢ completion 0 ⋯ = 0

Tactic:
ext x
  refine Completion.induction_on x ?_ ?_
  · apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
    exact continuous_const
  · simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
⊢ Continuous fun p ↦ p.1 * p.2

Tactic:
by
    let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
    have : Continuous fun p : α × α => m p.1 p.2 := (continuous_coe α).comp continuous_mul
    have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
    exact (di.extend_Z_bilin di this :)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑a * (↑b + ↑c) = ↑a * ↑b + ↑a * ↑c

Tactic:
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
have hx' : x ≠ 0 := by
      rintro rfl
      rw [inf_eq_right.mpr hx] at hF
      exact cau_F.1.ne hF

Goal state after:
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (map (fun x ↦ x⁻¹) F)
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
⊢ CompletableTopField α

Tactic:
by
  refine CompletableTopField.mk (fun F F_cau inf_F => ?_)
  rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢
  have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
    ext; simp only [Function.comp_apply, map_inv₀]
  rw [Filter.map_comm h_comm]
  apply CompletableTopField.nice _ F_cau
  rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

Goal state after: