mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
hxi : IsIntegral ℤ 0
hx : ∀ (φ : K →+* A), 0 = 1
⊢ False

Tactic:
zero_ne_one

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
hxi : IsIntegral ℤ 0
hx : ∀ (φ : K →+* A), False
⊢ False
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∃ x, x ≠ 0 ∧ (hom v) (v.restrict x) < γ

Tactic:
by
  have hγ_pos : 0 < γ := pos_iff_ne_zero.mpr hγ
  obtain ⟨x, h⟩ := NNReal.exists_lt_of_strictMono (RankOne.strictMono v.restrict) hγ_pos
  obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val
  refine ⟨k, ?_, ?_⟩
  · simp only [restrict₀_apply, MonoidWithZeroHom.coe_ofClass, restrict_def, map_eq_zero,
      dite_eq_left_iff, coe_ne_zero, imp_false, not_not] at hk
    by_contra h0
    rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk
    simp at hk
  · convert! h
    simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]
    congr 1
    exact (embedding_restrict₀ k).symm

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℚ
hx : x.num • 1 < ↑x.den • 1
⊢ x ≤ 1

Tactic:
simpa [Rat.le_iff] using ((smul_lt_smul_iff_of_pos_right zero_lt_one).mp hx).le

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

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

Tactic:
nnnorm_prod_eq_sup_of_pairwise_ne,

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ ↑(s.sup fun i ↦ ‖f i‖₊) = s.sup' hs' fun i ↦ ‖f i‖

M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
· simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]

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

Goal state before:
pp: case neg.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match a with
      | (a, b) => (single () a, single () b)) ∈
      antidiagonal (single () n)

pp: case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
· aesop

Goal state after:
case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
· aesop

Goal state after:
case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
· aesop

Goal state after:
case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
· aesop

Goal state after:
case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : n ≤ j
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

pp: case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

Tactic:
· aesop

Goal state after:
case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ mk v₁ = mk v₂ → v₁ = v₂

Tactic:
contrapose!

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ v₁ ≠ v₂ → mk v₁ ≠ mk v₂
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Tactic:
have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by
    by_contra! H
    exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x y : K
⊢ v (x + y) ≤ max (v x) (v y)

Tactic:
obtain ⟨w, hw⟩ := v.prop
  have H x : v x = NumberField.HeightOneSpectrum.adicAbv K w x := by
    rw [show v x = v.val x from rfl]
    grind only [place_apply, norm_embedding]
  simpa only [H] using adicAbv_add_le_max K w x y

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
| I

Tactic:
← finprod_heightOneSpectrum_pow_multiplicity hI

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
| ∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

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

Tactic:
ofJ_0_of_three_ne_zero h3

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ0 F).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
· simp only [neg_of_Z_eq_zero hP.left hPz, nonsingular_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      nonsingular_zero]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ (fun m ↦ m • W'.add P Q) (hu.unit ^ 4) = W'.add (u • P) (v • Q)

Tactic:
by convert! (add_smul_of_equiv h hu hv).symm

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective 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 = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ W.addXYZ P Q = addU P Q • ![0, 1, 0]

Tactic:
addXYZ_of_X_eq hP hQ hPz hQz hx

Goal state after:
F : Type u
inst✝ : Field F
W : Projective 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 = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ addU P Q • ![0, 1, 0] = addU P Q • ![0, 1, 0]
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
R : Presieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
exact E.isSheafFor_sieve_of_pullback hF h₁ h₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
by
  let E := PreZeroHypercover.mk _ _ f
  have : (E.sigmaOfIsColimit hc).HasPullbacks :=
    fun i j ↦ by dsimp [sigmaOfIsColimit]; infer_instance
  have (i : E.I₀) : HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit) := by
    dsimp [sigmaOfIsColimit_f]; infer_instance
  have : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F := by
    dsimp [E]; infer_instance
  have : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F := by
    convert! Functor.Initial.preservesLimit_of_comp (Discrete.equivalence <| .sigmaPUnit _).inverse
    · infer_instance
    · assumption
  let equiv := (E.isLimitSigmaOfIsColimitEquiv hc hc' F).nonempty_congr
  rwa [isLimit_toPreOneHypercover_type_iff, isLimit_toPreOneHypercover_type_iff,
    presieve₀_sigmaOfIsColimit] at equiv

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective 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 = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ toAffine W (W.add P Q) = 0

pp: case neg
F : Type u
inst✝¹ : Field F
W : Projective 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 = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ toAffine W (W.add P Q) = 0

Tactic:
· rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Projective 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 = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ toAffine W (W.add P Q) = 0
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
⊢ (uliftFunctor.mapCocone c).pt.str =
    ⨆ j,
      TopologicalSpace.coinduced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)))
        ((K ⋙ uliftFunctor).obj j).str

pp: case hc
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
⊢ IsColimit ((forget TopCat).mapCocone (uliftFunctor.mapCocone c))

Tactic:
· ext s
    rw [Homeomorph.ulift.symm.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp),
      isOpen_iff_of_isColimit _ hc, isOpen_iSup_iff]
    congr!
    rw [Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)]
    rfl

Goal state after:
case hc
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
⊢ IsColimit ((forget TopCat).mapCocone (uliftFunctor.mapCocone c))
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_1
X Y✝ : Scheme
𝓤 : Y✝.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y✝
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y✝ ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
⊢ 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯ = x (𝓤.f j) ⋯

Tactic:
𝓤.ι_glueMorphisms

Goal state after:
case refine_1
X Y✝ : Scheme
𝓤 : Y✝.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y✝
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y✝ ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
⊢ x (𝓤.f j) ⋯ = x (𝓤.f j) ⋯
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_2
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
e' : (yoneda.obj X).obj (op Y)
h : x.IsAmalgamation e'
j : 𝓤.I₀
⊢ 𝓤.f j ≫ e' = 𝓤.f j ≫ e

Tactic:
𝓤.ι_glueMorphisms

Goal state after:
case refine_2
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
e' : (yoneda.obj X).obj (op Y)
h : x.IsAmalgamation e'
j : 𝓤.I₀
⊢ 𝓤.f j ≫ e' = x (𝓤.f j) ⋯