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
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
⊢ x ∈
    ⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset

Tactic:
;

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
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
⊢ x ∈
    ⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔
    Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
←
    LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero,

Goal state after:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔ {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
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
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
by
  apply pow_eq_one_of_norm_le_one K A _ hxi fun φ ↦ le_of_eq <| hx φ
  intro rfl
  simp_rw [map_zero, norm_zero, zero_ne_one] at hx
  exact hx (IsAlgClosed.lift (R := ℚ)).toRingHom

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : K →+* ℂ
⊢ conjugate (conjugate x✝) = x✝

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
x✝ : K →+* ℂ
⊢ conjugate (conjugate x✝) = x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ (place (conjugate φ)) x✝ = (place φ) x✝

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ (place (conjugate φ)) x✝ = (place φ) x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ φ = (φ.comp ↑f).comp f.symm.toRingHom

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
⊢ φ = (φ.comp ↑f).comp f.symm.toRingHom
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
x✝ : K
⊢ φ x✝ = ((φ.comp ↑f).comp f.symm.toRingHom) x✝

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp ↑f)
x✝ : K
⊢ φ x✝ = ((φ.comp ↑f).comp f.symm.toRingHom) x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a✝ : K
⊢ (σ ^ 2) a✝ = 1 a✝

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
hσ : IsConj φ σ
hσ' : σ ≠ 1
a✝ : K
⊢ (σ ^ 2) a✝ = 1 a✝
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ a.card = (b ∪ c).card

Tactic:
apply congr_arg Finset.card
    simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]
    tauto

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := ⋯
he : StrictMono ⇑e
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑1).log) ⋯) ⋯) = ↑↑1

Tactic:
;

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := ⋯
he : StrictMono ⇑e
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑1).log) ⋯) ⋯) = ↑↑1
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := ⋯
he : StrictMono ⇑e
x✝¹ x✝ : Multiplicative ℝ
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑(x✝¹ * x✝)).log) ⋯) ⋯) =
    ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑x✝¹).log) ⋯) ⋯ * Units.mk0 (NNReal.mk (2 ^ (↑x✝).log) ⋯) ⋯)

Tactic:
;

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := ⋯
he : StrictMono ⇑e
x✝¹ x✝ : Multiplicative ℝ
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑(x✝¹ * x✝)).log) ⋯) ⋯) =
    ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑x✝¹).log) ⋯) ⋯ * Units.mk0 (NNReal.mk (2 ^ (↑x✝).log) ⋯) ⋯)
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mp
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
⊢ IsRankLeOne R → MulArchimedean (ValueGroupWithZero R)

Tactic:
rintro ⟨⟨f, hf⟩⟩
    exact .comap f.toMonoidHom hf

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

Goal state before:
pp: case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

pp: case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
;

Goal state after:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
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 φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ (coeff (u, snd✝).1) x * (coeff (u, snd✝).2) φ = 0

Tactic:
suffices u < e by simp only [he u this, zero_mul, map_zero]

Goal state after:
case h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u < e
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (x - y))) = ↑((RankOne.hom v) (v.restrict (y - x)))

Tactic:
;

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (x - y))) = ↑((RankOne.hom v) (v.restrict (y - x)))
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ (monomial (n + 0)) (r * s) = 0

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ (monomial (n + 0)) (r * s) = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((monomial (n + 0)) (r * s)) = (coeff n✝) 0

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((monomial (n + 0)) (r * s)) = (coeff n✝) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ (monomial (0 + n)) (s * r) = 0

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ (monomial (0 + n)) (s * r) = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((monomial (0 + n)) (s * r)) = (coeff n✝) 0

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((monomial (0 + n)) (s * r)) = (coeff n✝) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0 ∨ (weightedHomogeneousComponent w q) g = 0
⊢ False

Tactic:
rcases H with H | H <;>
        · refine weightedHomogeneousComponent_of_weightedOrder ?_ H
          simp only [ENat.natCast_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
          rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]
          exact ENat.natCast_toNat (ne_top_of_lt (by simpa))

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

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ ≠ 0
⊢ φ⁻¹ * φ = 1

Tactic:
rw [mul_comm, φ.mul_inv_cancel h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : n = 0
⊢ a = a

pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (-a *
      ∑ x ∈ antidiagonal (single () n),
        if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : n = 0
⊢ a = a

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f.divXPowOrder

Tactic:
;

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f.divXPowOrder
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyConnected x✝ ↔ geometrically (fun x ↦ ConnectedSpace ↥x) x✝

Tactic:
;

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyConnected x✝ ↔ geometrically (fun x ↦ ConnectedSpace ↥x) x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n

Tactic:
;

Goal state after:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
⊢ (ConcreteCategory.hom (F.map gi.op)) (s.val i) = (ConcreteCategory.hom (F.map gj.op)) (s.val j)

Tactic:
by
      have heq := s.property ⟨(i, j), ⟨⟩⟩
      dsimp at heq
      rw [← pullback.lift_fst _ _ hgij]
      conv_rhs => rw [← pullback.lift_snd _ _ hgij]
      rw [op_comp, Functor.map_comp, op_comp, Functor.map_comp]
      simp [heq]

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

Tactic:
rw [← Sieve.generate_le_iff, Sieve.generate_sieve, Sieve.generate_le_iff,
      Presieve.ofArrows_le_iff]
    intro i
    rw [← f.w₀]
    exact ⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
x✝ : E.multicospanShape.L
⊢ ((E.multifork F).toSections (h.amalgamate s.val ⋯)).val x✝ = s.val x✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
x✝ : E.multicospanShape.L
⊢ ((E.multifork F).toSections (h.amalgamate s.val ⋯)).val x✝ = s.val x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (P y ^ 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W.a₂ * P x ^ 2 * P z + W.a₄ * P x * P z ^ 2 + W.a₆ * P z ^ 3)) /
          P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + W.toAffine.a₂ * (P x / P z) ^ 2 + W.toAffine.a₄ * (P x / P z) + W.toAffine.a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (P y ^ 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W.a₂ * P x ^ 2 * P z + W.a₄ * P x * P z ^ 2 + W.a₆ * P z ^ 3)) /
          P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + W.toAffine.a₂ * (P x / P z) ^ 2 + W.toAffine.a₄ * (P x / P z) + W.toAffine.a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
    0
⊢ (u * P y) ^ 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) + W'.a₃ * (u * P y) * (u * P z) ^ 2 -
          ((u * P x) ^ 3 + W'.a₂ * (u * P x) ^ 2 * (u * P z) + W'.a₄ * (u * P x) * (u * P z) ^ 2 +
            W'.a₆ * (u * P z) ^ 3) +
        u ^ 3 * 0 -
      (0 +
        u ^ 3 *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0

Tactic:
;

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
    0
⊢ (u * P y) ^ 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) + W'.a₃ * (u * P y) * (u * P z) ^ 2 -
          ((u * P x) ^ 3 + W'.a₂ * (u * P x) ^ 2 * (u * P z) + W'.a₄ * (u * P x) * (u * P z) ^ 2 +
            W'.a₆ * (u * P z) ^ 3) +
        u ^ 3 * 0 -
      (0 +
        u ^ 3 *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = ↑hu.unit⁻¹ • u • P

Tactic:
;

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = ↑hu.unit⁻¹ • u • P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧ =
    ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧

Tactic:
smul_eq _ <| Ne.isUnit hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧ =
    ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

Tactic:
;

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      (W.toAffine.a₁ * (P y / P z) - (3 * (P x / P z) ^ 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0