mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ v ((algebraMap O F) y) = v ((algebraMap O F) y)

Tactic:
by simp

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
inst✝¹ : ZeroLEOneClass M
inst✝ : NeZero 1
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ 0 < 1

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ Rat.ofInt (-1) ∈ ratLt 0

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n + 1 ≠ 0

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ n < n + 1

Tactic:
by simp

Goal state after:
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
hγ_pos : 0 < γ
⊢ ∃ x, x ≠ 0 ∧ (hom v) (v.restrict x) < γ

Tactic:
obtain ⟨x, h⟩ := NNReal.exists_lt_of_strictMono (RankOne.strictMono v.restrict) hγ_pos

Goal state after:
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
⊢ ∃ x, x ≠ 0 ∧ (hom v) (v.restrict x) < γ
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
have hn : 2 ∣ n :=
    Equiv.Perm.two_dvd_card_support
      (by
         rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one])

Goal state after:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
Module: Mathlib.Analysis.Complex.Polynomial.Basic

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

Tactic:
by simp

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
⊢ (valueGroup₀_equiv_withZeroMulInt v) 0 = 0

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ n + 1 ≠ 0

Tactic:
by simp

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ (Int.natAbs 1).Coprime (n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
hy : y ∈ closedBall x r
x✝ : closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
cases closedBall_eq_or_disjoint x y r with

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✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ a ::ₘ t ≠ 0 → a ∈ a ::ₘ t

Tactic:
by simp

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✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : 0 ≠ 0 → M ∈ 0
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ a ::ₘ 0 ≠ 0 → a ∈ a ::ₘ 0

Tactic:
by simp

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✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : 0 ≠ 0 → M ∈ 0
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f a‖

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
⊢ valuation.restrict 1 ≠ 0

Tactic:
by simp

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
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ((↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊) → ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
⊢ ↑s ⊆ ↑(Finset.cons a s ha)

Tactic:
by simp

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
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (p, q) ∈ Finset.antidiagonal (p + q)

Tactic:
by simp

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

Goal state before:
pp: K✝ : Type u_1
hK : NormedField K✝
inst✝² : IsUltrametricDist K✝
K : Type u_2
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
h : 1 < ‖x‖
⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ↑u *
        (-↑u⁻¹ *
          ∑ x ∈ antidiagonal (0, n).2, if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0

Tactic:
neg_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ↑u *
        -(↑u⁻¹ *
            ∑ x ∈ antidiagonal (0, n).2, if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ ≤ 1

Tactic:
norm_embedding

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) ≤ 1
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ = 1 ↔ x ∉ v.asIdeal

Tactic:
norm_embedding

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) = 1 ↔ x ∉ v.asIdeal
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ ‖(embedding v) ((algebraMap R K) x)‖ < 1 ↔ x ∈ v.asIdeal

Tactic:
norm_embedding

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) < 1 ↔ x ∈ v.asIdeal
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : IsDedekindDomain R
inst✝¹ : IsFractionRing R K
v✝ : HeightOneSpectrum R
inst✝ : NumberField K
v : FinitePlace K
⊢ ∀ {a : K}, v a = 0 → a = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * W'.neg P x * W'.neg P z + 3 * P x * W'.neg P x ^ 2 * P z + P y ^ 2 * W'.neg P z ^ 2 -
                      W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * W'.neg P z ^ 2 -
                  W'.a₁ * W'.neg P x * W'.neg P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * W'.neg P z ^ 2 +
              W'.a₂ * W'.neg P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * W'.neg P z ^ 2 -
          W'.a₃ * W'.neg P y * P z ^ 2 * W'.neg P z -
        W'.a₄ * P x * P z * W'.neg P z ^ 2 +
      W'.a₄ * W'.neg P x * P z ^ 2 * W'.neg P z =
    0

Tactic:
neg_X,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * W'.neg P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * W'.neg P z ^ 2 - W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * W'.neg P z ^ 2 -
                  W'.a₁ * P x * W'.neg P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * W'.neg P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * W'.neg P z ^ 2 -
          W'.a₃ * W'.neg P y * P z ^ 2 * W'.neg P z -
        W'.a₄ * P x * P z * W'.neg P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * W'.neg P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

Tactic:
neg_X,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * W'.neg P y ^ 2 * P z + P x * P y ^ 2 * W'.neg P z - 2 * P x * P y * W'.neg P y * W'.neg P z +
                              2 * P x * P y * W'.neg P y * P z -
                            W'.a₁ * P x ^ 2 * W'.neg P y * W'.neg P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * W'.neg P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * W'.neg P z ^ 2 +
                  W'.a₃ * P x * W'.neg P y * P z ^ 2 -
                2 * W'.a₃ * P x * W'.neg P y * P z * W'.neg P z +
              2 * W'.a₃ * P x * P y * P z * W'.neg P z +
            W'.a₄ * P x ^ 2 * W'.neg P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * W'.neg P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * W'.neg P z =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ -3 * P x ^ 2 * W'.neg P x * W'.neg P y + 3 * P x * W'.neg P x ^ 2 * P y - P y ^ 2 * W'.neg P y * W'.neg P z +
                                      P y * W'.neg P y ^ 2 * P z +
                                    W'.a₁ * P x * W'.neg P y ^ 2 * P z -
                                  W'.a₁ * W'.neg P x * P y ^ 2 * W'.neg P z -
                                W'.a₂ * P x ^ 2 * W'.neg P y * W'.neg P z +
                              W'.a₂ * W'.neg P x ^ 2 * P y * P z +
                            2 * W'.a₂ * P x * W'.neg P x * P y * W'.neg P z -
                          2 * W'.a₂ * P x * W'.neg P x * W'.neg P y * P z -
                        W'.a₃ * P y ^ 2 * W'.neg P z ^ 2 +
                      W'.a₃ * W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₄ * P x * P y * W'.neg P z ^ 2 -
                  2 * W'.a₄ * P x * W'.neg P y * P z * W'.neg P z +
                2 * W'.a₄ * W'.neg P x * P y * P z * W'.neg P z -
              W'.a₄ * W'.neg P x * W'.neg P y * P z ^ 2 +
            3 * W'.a₆ * P y * P z * W'.neg P z ^ 2 -
          3 * W'.a₆ * W'.neg P y * P z ^ 2 * W'.neg P z +
        -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (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:
neg_X,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ -3 * P x ^ 2 * P x * W'.neg P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * W'.neg P y * W'.neg P z +
                                      P y * W'.neg P y ^ 2 * P z +
                                    W'.a₁ * P x * W'.neg P y ^ 2 * P z -
                                  W'.a₁ * P x * P y ^ 2 * W'.neg P z -
                                W'.a₂ * P x ^ 2 * W'.neg P y * W'.neg P z +
                              W'.a₂ * P x ^ 2 * P y * P z +
                            2 * W'.a₂ * P x * P x * P y * W'.neg P z -
                          2 * W'.a₂ * P x * P x * W'.neg P y * P z -
                        W'.a₃ * P y ^ 2 * W'.neg P z ^ 2 +
                      W'.a₃ * W'.neg P y ^ 2 * P z ^ 2 +
                    W'.a₄ * P x * P y * W'.neg P z ^ 2 -
                  2 * W'.a₄ * P x * W'.neg P y * P z * W'.neg P z +
                2 * W'.a₄ * P x * P y * P z * W'.neg P z -
              W'.a₄ * P x * W'.neg P y * P z ^ 2 +
            3 * W'.a₆ * P y * P z * W'.neg P z ^ 2 -
          3 * W'.a₆ * W'.neg P y * P z ^ 2 * W'.neg P z +
        -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (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.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
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i : E.I₀
⊢ (ConcreteCategory.hom (F.map (E.f i).op)) (h.amalgamate x hc) = x i

Tactic:
by
  rw [amalgamate, Presieve.IsSheafFor.valid_glue _ _ _ ⟨i⟩]
  simp

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
b : E.toPreOneHypercover.I₁'
⊢ E.f b.fst.1 ≫ 𝟙 S = c.inj b.fst.1 ≫ (E.sigmaOfIsColimit hc).f PUnit.unit

Tactic:
by simp

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
b : E.toPreOneHypercover.I₁'
⊢ E.f b.fst.2 ≫ 𝟙 S = c.inj b.fst.2 ≫ (E.sigmaOfIsColimit hc).f PUnit.unit

Tactic:
by simp

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 : E.I₀), c.inj i ≫ (E.sigmaOfIsColimit hc).f PUnit.unit = E.f i

Tactic:
by simp

Goal state after:
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
s : Set ↑(uliftFunctor.mapCocone c).pt
⊢ s ⊆ Set.range ⇑Homeomorph.ulift.symm

Tactic:
by simp

Goal state after:
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
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ ⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s ⊆ Set.range ⇑Homeomorph.ulift

Tactic:
by simp

Goal state after:
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
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s) ↔ IsOpen s

Tactic:
rw [Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)]

Goal state after:
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ IsOpen (⇑Homeomorph.ulift ⁻¹' ⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s) ↔ IsOpen s
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
i : 𝒰.I₀
y : ↑(𝒰.X i)
⊢ (ConcreteCategory.hom (𝒰.f i)) y ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f i))

Tactic:
by simp

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Projective R
W : Projective F
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid A

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₂ e * (1 - f₁ e) = -f₂ e * (f₁ e - f₂ e)

Tactic:
neg_mul,

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₂ e * (1 - f₁ e) = -(f₂ e * (f₁ e - f₂ e))