mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
hp : Irreducible p
⊢ MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

Tactic:
refine ⟨fun x y ↦ ?_⟩
  have hx := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm x).2).2
  have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2
  obtain ⟨g, hg⟩ := (Normal.minpoly_eq_iff_mem_orbit p.SplittingField).mp (hy.symm.trans hx)
  exact ⟨g, (rootsEquivRoots p E).eq_symm_apply.mp (Subtype.ext hg)⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ✝ : Type u_1
τ : Type u_2
R✝ : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha : a✝ ∈ Set.ofPred IsSymmetric
hb : b✝ ∈ Set.ofPred IsSymmetric
e : Perm σ
⊢ (rename ⇑e) (a✝ + b✝) = a✝ + b✝

Tactic:
map_add,

Goal state after:
σ✝ : Type u_1
τ : Type u_2
R✝ : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha : a✝ ∈ Set.ofPred IsSymmetric
hb : b✝ ∈ Set.ofPred IsSymmetric
e : Perm σ
⊢ (rename ⇑e) a✝ + (rename ⇑e) b✝ = a✝ + b✝
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
x✝ : Finset σ
⊢ (Finsupp.single (∑ i ∈ x✝, Finsupp.single i 1) 1).support = {∑ i ∈ x✝, Finsupp.single i 1}

Tactic:
exact Finsupp.support_single _ one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map (fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) s.antidiagonal).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)

Tactic:
antidiagonal_eq_map_powerset,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map (fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) (map (fun t ↦ (s - t, t)) s.powerset)).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
n : ℕ
⊢ IsClosedMap fun x ↦ x ^ n

Tactic:
simpa [eval_X_pow] using (X ^ n).isClosedMap_eval

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f

Tactic:
rw [analyticOn_univ]
  exact analyticOnNhd_univ_iff_differentiable

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

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ ((u + v).num * (↑u.den * ↑v.den)) • 1 < (↑u.den * ↑v.den * ↑(u + v).den) • (x + y)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ ((u + v).num * ↑u.den * ↑v.den) • 1 < (↑u.den * ↑v.den * ↑(u + v).den) • (x + y)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case mp
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
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
z : ℂ
⊢ (∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z) →
    (aeval z) p = 0 ∧ z.im ≠ 0

pp: case mpr
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
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
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im ≠ 0 →
    ∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z

Tactic:
· rintro ⟨w, hw, rfl⟩
      exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩

Goal state after:
case mpr
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
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
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im ≠ 0 →
    ∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ∀ (a₁ b₁ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
          (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) →
            IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
              a₁ ≤ b₁ →
                ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                  (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) +
                      ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
                    ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
h₁ : ¬a₁ ≤ b₁
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
specialize this b₁ a₁
    rw [uIcc_comm b₁ a₁, min_comm b₁ a₁, max_comm b₁ a₁] at this
    simp only [intervalIntegral.integral_symm b₁ a₁]
    refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₁))).trans ?_; abel

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(hφ.embedding x) = φ x

Tactic:
by
  apply Complex.ext
  · rfl
  · rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
    exact RingHom.congr_fun hφ x

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

Goal state before:
pp: case mpr
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 y : M
a u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ a ∈ ratLt (x + y)

Tactic:
rw [← huv]

Goal state after:
case mpr
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 y : M
a u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ u + v ∈ ratLt (x + y)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - C (z + (starRingEnd ℂ) z) * X + C (↑‖z‖ ^ 2) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
map_add,

Goal state after:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - (C z + C ((starRingEnd ℂ) z)) * X + C (↑‖z‖ ^ 2) = (X - C ((starRingEnd ℂ) z)) * (X - C z)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ∫ (x : ℝ × ℝ) in Set.Icc (a₁, a₂) (b₁, b₂), (f' x) (1, 0) + (g' x) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
apply integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g'
        (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ (coeff d) (φ + ψ) = 0

Tactic:
map_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ (coeff d) φ + (coeff d) ψ = 0
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_1.inr
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
⊢ ∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U

Tactic:
obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp hε)
          use Units.mk0 (valuation.restrict x) (by simp [Valuation.restrict_def, hx])
          intro y hy
          apply h
          simp only [Metric.mem_ball, dist_zero_right]
          simp only [Units.val_mk0, mem_ofPred_eq, restrict_lt_iff, ← NNReal.coe_lt_coe] at hy
          apply lt_trans hy
          simpa [RankLeOne.hom', valuation.restrict_def] using! hxy

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

Goal state before:
pp: case refine_1
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U

Tactic:
have hδ_pos : 0 < δ := by
            rw [hδ, ← map_zero hv.hom]
            exact hv.strictMono _ (Units.zero_lt ε)

Goal state after:
case refine_1
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
hδ_pos : 0 < δ
⊢ ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ 𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑(min x y)} ∧
    𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑(min x y)}

Tactic:
simp only [le_principal_iff, mem_principal, ofPred_subset_ofPred, Prod.forall]

Goal state after:
case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ (∀ (a b : L), v.norm (a - b) < ↑(min x y) → v.norm (a - b) < ↑x) ∧
    ∀ (a b : L), v.norm (a - b) < ↑(min x y) → v.norm (a - b) < ↑y
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff φ = 0 ∧ ¬constantCoeff ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1

Tactic:
← mul_assoc,

Goal state after:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff φ = 0 ∧ ¬constantCoeff ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * φ * ψ = 1
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Function.HasFiniteMulSupport fun w ↦ w ↑x

Tactic:
have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 :=
    ne_iff_lt_iff_le.mpr <| norm_embedding_eq w x ▸ norm_le_one K w.maximalIdeal x
  simp_rw [Function.HasFiniteMulSupport, Function.mulSupport, this, ← norm_embedding_eq,
    norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton]
  have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by
    apply Ideal.finite_factors
    simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]
  have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}} :=
    Function.Injective.injOn maximalIdeal_injective
  refine (h.subset ?_).of_finite_image h_inj
  simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_ofPred_eq, subset_refl]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 ≠ 0
⊢ (if 0 = 0 then if 3 = 0 then ofJ1728 F else ofJ0 F else if 0 = 1728 then ofJ1728 F else ofJNe0Or1728 0) = ofJ0 F

Tactic:
if_pos rfl,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 ≠ 0
⊢ (if 3 = 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ (if 0 = 0 then if 3 = 0 then ofJ1728 F else ofJ0 F else if 0 = 1728 then ofJ1728 F else ofJNe0Or1728 0) = ofJ1728 F

Tactic:
if_pos rfl,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ (if 3 = 0 then ofJ1728 F else ofJ0 F) = ofJ1728 F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ (if 0 = 0 then if 3 = 0 then ofJ1728 F else ofJ0 F else if 0 = 1728 then ofJ1728 F else ofJNe0Or1728 0) = ofJ0 F

Tactic:
if_pos rfl,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ (if 3 = 0 then ofJ1728 F else ofJ0 F) = ofJ0 F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ j).j = j

Tactic:
simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
⊢ grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

Tactic:
rw [grothendieckTopology, ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
⊢ (Precoverage.toPretopology Scheme (precoverage P)).toGrothendieck =
    (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

Tactic:
by_cases hPz : P z = 0
  · simp only [neg_of_Z_eq_zero hP.left hPz, nonsingular_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      nonsingular_zero]
  · simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
      nonsingular_neg_of_Z_ne_zero hP hPz]

Goal state after:
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
⊢ Nonempty (IsLimit (E.multifork F))

Tactic:
Multifork.isLimit_types_iff

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
⊢ Function.Bijective (E.multifork F).toSections
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ ∀ (i j : E.I₀),
    (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).inj (i, j) ≫
        (Iso.refl (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).pt).hom ≫
          pullback.fst ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.fst (E.f (equiv.symm (i, j)).fst.1) (E.f (equiv.symm (i, j)).fst.2) ≫ c.inj i

Tactic:
simp [c', equiv, Equiv.sigmaPUnit]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ ∀ (i j : E.I₀),
    (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).inj (i, j) ≫
        (Iso.refl (Cofan.mk c'.pt fun i ↦ c'.inj (equiv.symm i)).pt).hom ≫
          pullback.snd ((E.sigmaOfIsColimit hc).f PUnit.unit) ((E.sigmaOfIsColimit hc).f PUnit.unit) =
      pullback.snd (E.f (equiv.symm (i, j)).fst.1) (E.f (equiv.symm (i, j)).fst.2) ≫ c.inj j

Tactic:
simp [c', equiv, Equiv.sigmaPUnit]

Goal state after:
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
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦Q⟧

Tactic:
addMap_eq,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ ⟦W.add P Q⟧ = ⟦Q⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦Q⟧

Tactic:
addMap_eq,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
⊢ ⟦W.add P Q⟧ = ⟦Q⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
addMap_eq,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ ⟦W.add P Q⟧ = ⟦P⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
addMap_eq,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦W.add P Q⟧ = ⟦P⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular 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 = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
addMap_eq,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular 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 = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ ⟦W.add P Q⟧ = ⟦![0, 1, 0]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular 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 = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
addMap_eq,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular 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 = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ ⟦W.add P Q⟧ = ⟦![0, 1, 0]⟧