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

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ ↦ φ x) = range fun ψ ↦ ψ x

Tactic:
ext a

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
a : A
⊢ (a ∈ range fun φ ↦ φ x) ↔ a ∈ range fun ψ ↦ ψ x
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
⊢ den • x ≤ (n * ↑den) • 1

Tactic:
rw [mul_comm, ← smul_smul]

Goal state after:
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
⊢ den • x ≤ ↑den • n • 1
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
⊢ ratLt (x + y) = ratLt x + ratLt y

Tactic:
ext a

Goal state after:
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 : ℚ
⊢ a ∈ ratLt (x + y) ↔ a ∈ ratLt x + ratLt y
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Function.Bijective ⇑(galActionHom p ℂ)

Tactic:
by
  have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree := by
    simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
    rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
    · exact IsAlgClosed.splits _
    · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
  let conj' := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
  refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩
  apply Equiv.Perm.subgroup_eq_top_of_swap_mem
  · rwa [h1]
  · rw [h1]
    simpa only [Fintype.card_eq_nat_card,
      Nat.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv.symm]
      using prime_degree_dvd_card p_irr p_deg
  · exact ⟨conj', rfl⟩
  · rw [← Equiv.Perm.card_support_eq_two]
    apply Nat.add_left_cancel
    rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
⊢ ball x r = ball y r

Tactic:
ext a

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
a : X
⊢ a ∈ ball x r ↔ a ∈ ball y r
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
⊢ embedRealFun 1 ≤ 1

Tactic:
apply csSup_le (ratLt'_nonempty 1)

Goal state after:
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
⊢ ∀ b ∈ ratLt' 1, b ≤ 1
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case e'_4.e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) x = dist 0 x

Tactic:
simp [SeminormedAddGroup.dist_eq]

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

Goal state before:
pp: case e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) y = dist x (x + y)

Tactic:
simp [SeminormedAddGroup.dist_eq]

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

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ dist x⁻¹ 1 ≠ dist 1 y

Tactic:
by simp [h]

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
h : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ Lex (σ →₀ ℕ)

Tactic:
apply WellFounded.min _ (toLex '' φ.support) ne

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ Lex (σ →₀ ℕ) → Lex (σ →₀ ℕ) → Prop

σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ WellFounded ?m.40
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : 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
⊢ (coeff e) x = 0

Tactic:
← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,

Goal state after:
σ : 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
⊢ constantCoeff φ * (coeff e) x = 0
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_2
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✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
⊢ ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U

Tactic:
have : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.v⟩

Goal state after:
case refine_2
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✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
this : Nontrivial Γ₀ˣ
⊢ ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case left
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X}

Tactic:
rw [Ideal.mem_span_singleton]

Goal state after:
case left
k : Type u_2
inst✝ : Field k
⊢ ¬X ∣ 1
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
h1728 : ¬j = 1728
⊢ (ofJ j).IsElliptic

Tactic:
· have := Fact.mk (Ne.isUnit h0)
      have := Fact.mk (sub_ne_zero.2 h1728).isUnit
      rw [ofJ_ne_0_ne_1728 j h0 h1728]
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ Nonempty (IsLimit c) ↔ Function.Bijective c.toSections

Tactic:
rw [Types.isLimit_iff_bijective_sectionOfCone, ← toSections_fac, EquivLike.comp_bijective]

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 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 - W'.negY P ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * W'.negY P * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * W'.negY P * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0

Tactic:
negY

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * 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
⊢ W'.addZ P (W'.neg P) = 0

Tactic:
rw [addZ, neg_X, neg_Y, neg_Z, negY]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * 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'.negY P ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * W'.negY P * P z + 2 * P x * P y * W'.negY P * P z -
                            W'.a₁ * P x ^ 2 * W'.negY P * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * W'.negY P * P z ^ 2 -
                2 * W'.a₃ * P x * W'.negY P * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Tactic:
negY

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

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 * (-P y - W'.a₁ * P x - W'.a₃ * P z) + 3 * P x * P x ^ 2 * P y -
                                        P y ^ 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                                      P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z +
                                    W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z -
                                  W'.a₁ * P x * P y ^ 2 * P z -
                                W'.a₂ * P x ^ 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                              W'.a₂ * P x ^ 2 * P y * P z +
                            2 * W'.a₂ * P x * P x * P y * P z -
                          2 * W'.a₂ * P x * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z -
                        W'.a₃ * P y ^ 2 * P z ^ 2 +
                      W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₄ * P x * P y * P z ^ 2 -
                  2 * W'.a₄ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z * P z +
                2 * W'.a₄ * P x * P y * P z * P z -
              W'.a₄ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 +
            3 * W'.a₆ * P y * P z * P z ^ 2 -
          3 * W'.a₆ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z +
        -3 * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * 0 -
      (P z * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) ^ 3 +
        -3 * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) *
          (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.Preserves

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
⊢ ∃! x, (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := hi b

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
t : F.obj (∏ᶜ fun x ↦ op (X x))
ht₁ :
  (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      t =
    b
ht₂ :
  ∀ (y : (fun X ↦ X) (F.obj (∏ᶜ fun x ↦ op (X x)))),
    (fun a ↦
          (ConcreteCategory.hom
                (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj))
              a =
            b)
        y →
      y = t
⊢ ∃! x, (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
| ![0, P y, P z]

Tactic:
hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
| ![0, P y, 0]
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1.refine_1
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ (i : 𝒰.I₀) → C(↑(Set.range ⇑(ConcreteCategory.hom (𝒰.f i))), ↑X)

pp: case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ ∀ (i j : 𝒰.I₀) (x : ↑Y) (hxi : x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
    (hxj : x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f j))),
    (?refine_1.refine_1 i) ⟨x, hxi⟩ = (?refine_1.refine_1 j) ⟨x, hxj⟩

pp: case refine_1.refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ ∀ (x : ↑Y), ∃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.f i)) ∈ nhds x

Tactic:
· intro i
      exact ⟨(x i).hom ∘ (isOpenEmbedding_f_zeroHypercover 𝒰 i).toHomeomorph.symm, by fun_prop⟩

Goal state after:
case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ ∀ (i j : 𝒰.I₀) (x_1 : ↑Y) (hxi : x_1 ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
    (hxj : x_1 ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f j))),
    { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ } ⟨x_1, hxi⟩ =
      { toFun := ⇑(Hom.hom (x j)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ } ⟨x_1, hxj⟩

case refine_1.refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ ∀ (x : ↑Y), ∃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.f i)) ∈ nhds x
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve.ofArrows F.obj (colimit.ι F) ∈ Scheme.zariskiTopology (colimit F)

Tactic:
exact (Scheme.IsLocallyDirected.openCover F).mem_grothendieckTopology

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

Goal state before:
pp: ⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
by
  refine stableUnderComposition.respectsIso ?_
  intro R S _ _ e
  exact .of_surjective e.surjective

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

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

Tactic:
negY

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) +
        (Q z ^ 3 * 0 +
            P z ^ 3 *
              (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
                (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)) +
          (P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 +
                  W'.a₂ * P x * Q z ^ 2 * P z +
                W'.a₂ * Q x * P z ^ 2 * Q z +
              W'.a₄ * P z ^ 2 * Q z ^ 2) *
            (Q x * P z)) -
      (0 +
        (Q z ^ 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)) +
            P z ^ 3 * 0 +
          (P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 +
                  W'.a₂ * P x * Q z ^ 2 * P z +
                W'.a₂ * Q x * P z ^ 2 * Q z +
              W'.a₄ * P z ^ 2 * Q z ^ 2) *
            (P x * Q z))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
negY

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0