mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (d.natTrans.app j) xj = ((functorOfLocallyDirected 𝒰).map fj) uk

Tactic:
apply (𝒰.f j).injective

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) (((functorOfLocallyDirected 𝒰).map fj) uk)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝¹⁰ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁸ : IsCofiltered I
inst✝⁷ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁶ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝² : ∀ (i : I), IsIso (e.app i)
inst✝¹ : IsIso e
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ (inv e).app i ≫ a =
    ((Cone.postcompose (asIso e).hom).obj c).π.app j ≫ (inv e).app j ≫ b

Tactic:
simp [hab]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h₀
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := ⋯
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := ⋯
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) ≫ pullback.fst f f =
    (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) ≫ pullback.fst f f

Tactic:
simp [hab]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h₁
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := ⋯
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := ⋯
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) ≫ pullback.snd f f =
    (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) ≫ pullback.snd f f

Tactic:
simp [hab]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
this : ∀ (i : κ), ∃ V, IsCompact V.carrier ∧ (fun x ↦ f x.fst x.snd) '' V.carrier = s i
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
choose V hVeq hVc using this

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
V : κ → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc : ∀ (i : κ), (fun x ↦ f x.fst x.snd) '' (V i).carrier = s i
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
this : g = ofHom (hπ.liftEquiv ⟨Hom.hom e, ⋯⟩)
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
assumption

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3

Tactic:
Δ

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: case a₁
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ f x✝¹.a₁ = f x✝.a₁

Tactic:
assumption

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

Goal state before:
pp: case a₂
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ f x✝¹.a₂ = f x✝.a₂

Tactic:
assumption

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

Goal state before:
pp: case a₃
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ f x✝¹.a₃ = f x✝.a₃

Tactic:
assumption

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

Goal state before:
pp: case a₄
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ f x✝¹.a₄ = f x✝.a₄

Tactic:
assumption

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

Goal state before:
pp: case a₆
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ f x✝¹.a₆ = f x✝.a₆

Tactic:
assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1✝ :
  ↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    ↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
⊢ (ConcreteCategory.hom (Scheme.Hom.app (c.π.app j.left) ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) t =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE H).op))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t)

Tactic:
convert! ConcreteCategory.comp_apply _ _ _
        congr
        simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (C • W).j = W.j

Tactic:
by
  rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]

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

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ ↑x✝¹.u = φ ↑x✝.u

Tactic:
assumption

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

Goal state before:
pp: case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.r = φ x✝.r

Tactic:
assumption

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

Goal state before:
pp: case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.s = φ x✝.s

Tactic:
assumption

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

Goal state before:
pp: case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.t = φ x✝.t

Tactic:
assumption

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ C.map φ • W.map φ = (C • W).map φ

Tactic:
simp only [map, variableChange_def, VariableChange.map]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { a₁ := ↑((Units.map ↑φ) C.u)⁻¹ * (φ W.a₁ + 2 * φ C.s),
      a₂ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 2 * (φ W.a₂ - φ C.s * φ W.a₁ + 3 * φ C.r - φ C.s ^ 2),
      a₃ := ↑((Units.map ↑φ) C.u)⁻¹ ^ 3 * (φ W.a₃ + φ C.r * φ W.a₁ + 2 * φ C.t),
      a₄ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 4 *
          (φ W.a₄ - φ C.s * φ W.a₃ + 2 * φ C.r * φ W.a₂ - (φ C.t + φ C.r * φ C.s) * φ W.a₁ + 3 * φ C.r ^ 2 -
            2 * φ C.s * φ C.t),
      a₆ :=
        ↑((Units.map ↑φ) C.u)⁻¹ ^ 6 *
          (φ W.a₆ + φ C.r * φ W.a₄ + φ C.r ^ 2 * φ W.a₂ + φ C.r ^ 3 - φ C.t * φ W.a₃ - φ C.t ^ 2 -
            φ C.r * φ C.t * φ W.a₁) } =
    { a₁ := φ (↑C.u⁻¹ * (W.a₁ + 2 * C.s)), a₂ := φ (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)),
      a₃ := φ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
      a₄ :=
        φ (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)),
      a₆ := φ (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) }
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) =
    Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)

Tactic:
simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul]

Goal state after:
case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - C (C (W.slope x₁ x₂ y₁ y₂ * (x₂ - x₁) + y₁)) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) =
    Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy : (D.map fkj) x ∈ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
⊢ IsAffineOpen (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))

Tactic:
exact ⟨((hf _).preimage _).preimage _, hy⟩

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

Goal state before:
pp: case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.toCharTwoJEqZeroNF • W).a₂ = 0

Tactic:
toCharTwoJEqZeroNF,

Goal state after:
case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ ({ u := 1, r := W.a₂, s := 0, t := 0 } • W).a₂ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Tactic:
rw [polynomialY_eq]
  simp

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧
      ((eval P) W.polynomialX / P z ^ 4 ≠ 0 ∨
        Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
div_ne_zero_iff,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧
      ((eval P) W.polynomialX ≠ 0 ∧ P z ^ 4 ≠ 0 ∨
        Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY / P z ^ 3 ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
div_ne_zero_iff,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0 ∧ P z ^ 3 ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
a : A
s : ↥S
b : A
t : ↥S
⊢ ∃ a_1 b_1 s_1, f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b_1 s_1 = f.mk' b t

Tactic:
use a * t, b * s, s * t

Goal state after:
case h
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := ⋯
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (a * ↑t) (s * t) = f.mk' a s ∧ f.mk' (b * ↑s) (s * t) = f.mk' b t
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ ⇑f ⁻¹' U ∈ 𝓝 1

Tactic:
apply emb.continuous.tendsto

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
H : Type u_2
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding ⇑f
U : Set H
hU : U ∈ 𝓝 1
⊢ U ∈ 𝓝 (f 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblY P = W'.dblU P ^ 3

Tactic:
by
  rw [dblY, negY_eq, negDblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']
  ring1

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y ↦ a + y) '' ↑(B i)
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
⊢ RingSubgroupsBasis fun i ↦ (B i).toAddSubgroup

Tactic:
by
  apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul
  intro a i
  rcases hB.leftMul a i with ⟨j, hj⟩
  use j
  rintro b (b_in : b ∈ B j)
  exact hj ⟨b, b_in, rfl⟩

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

Goal state before:
pp: case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Tactic:
rcases Q

Goal state after:
case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

Goal state after:
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ x * z * ↑(t * u) ≤ᵥ y * w * ↑(s * v)

Tactic:
Submonoid.coe_mul,

Goal state after:
case h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ x * z * (↑t * ↑u) ≤ᵥ y * w * ↑(s * v)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ x * z * (↑t * ↑u) ≤ᵥ y * w * ↑(s * v)

Tactic:
Submonoid.coe_mul,

Goal state after:
case h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ x * z * (↑t * ↑u) ≤ᵥ y * w * (↑s * ↑v)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ y * w * ↑(s * v) ≤ᵥ x * z * ↑(t * u)

Tactic:
Submonoid.coe_mul,

Goal state after:
case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ y * w * (↑s * ↑v) ≤ᵥ x * z * ↑(t * u)