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

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
x : ↥(D.obj A.i')
⊢ ∃ j y,
    ((Precoverage.ZeroHypercover.pullback₁ A.g (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X)).f ⟨j.fst, (j.snd, j.snd)⟩)
        y =
      x

Tactic:
by simpa [← Set.mem_range, Scheme.Pullback.range_fst,
        Scheme.Pullback.diagonalCoverDiagonalRange] using A.range_g_subset ⟨x, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
inst✝⁶ : P.IsStableUnderComposition
X✝ : Scheme
𝒰✝ : Cover (precoverage P) X✝
𝒱✝ : (x : 𝒰✝.I₀) → Cover (precoverage P) (𝒰✝.X x)
inst✝⁵ : X✝.Over S
inst✝⁴ : Cover.Over S 𝒰✝
inst✝³ : (x : 𝒰✝.I₀) → Cover.Over S (𝒱✝ x)
X : Scheme
𝒰 : Cover (precoverage P) X
𝒱 : (x : 𝒰.I₀) → Cover (precoverage P) (𝒰.X x)
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : (x : 𝒰.I₀) → Cover.Over S (𝒱 x)
x✝ : (Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀
i : 𝒰.I₀
j : ((fun i ↦ (𝒱 i).toPreZeroHypercover) i).I₀
⊢ (𝒱 i).X j ↘ S = (𝒱 i).X j ↘ S

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
k : Fin n
a✝ : k ∈ Finset.univ
hkj : ¬k = j
⊢ (c.val k).degree ≤ (c.val k).degree

Tactic:
rfl

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

Goal state before:
pp: case refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ ∀ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), IsCompactOpenCovered f t_1

Tactic:
grind

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

Goal state before:
pp: case refine_1.refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
x : S
⊢ ∀ (U_1 : Set S), IsOpen U_1 → ∀ (x_1 : S) (x_2 : x_1 ∈ U), Us x_1 ⋯ = U_1 → x ∈ U_1 → x ∈ U

Tactic:
grind

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

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
⊢ ∀ t ∈ {x | ∃ x_1, ∃ (h : x_1 ∈ U), Us x_1 h = ↑x}, IsCompactOpenCovered f ↑t

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
a✝ : k ∈ Finset.univ
hkj : ¬k = j
⊢ (c.val k).degree.succ ≤ (c.val k).degree.succ

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
⊢ { I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.presieve₀ ∈ (precoverage P).coverings S

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
⊢ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.I₀),
      P ({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f i)
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
a✝ : ↑X
⊢ (Hom.hom g) ((ConcreteCategory.hom π) a✝) = (Hom.hom (π ≫ g)) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ (g₁ ≫ g i₁) ≫ f i₁ = (g₂ ≫ g i₂) ≫ f i₂

Tactic:
by simpa [assoc] using eq

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂

Tactic:
grind

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)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
⊢ (ConcreteCategory.hom (Scheme.Hom.appLE (c.π.app i) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯)) s =
    (ConcreteCategory.hom (Scheme.Hom.appLE (c.π.app i) ⊤ (⋯.functor.obj ⊤) ⋯)) s

Tactic:
rfl

Goal state after:
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✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
⊢ ∃ U, ∃ (_ : IsAffineOpen U) (_ : x ∈ U), ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) ((s |_ U) ⋯) = 0

Tactic:
obtain ⟨j, f, hj⟩ := exists_appTop_map_eq_zero_of_isAffine_of_isLimit _ _
      (isLimitOpensCone D c hc i U) (.mk (𝟙 i)) (((opensDiagramι D i U).app _).appTop s) (by
        convert congr((c.pt.presheaf.map (homOfLE le_top).op).hom $hs)
        · simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE, ← ConcreteCategory.comp_apply]; rfl
        · simp)

Goal state after:
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)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s) =
    0
⊢ ∃ U, ∃ (_ : IsAffineOpen U) (_ : x ∈ U), ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) ((s |_ U) ⋯) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k₀ (fun t ↦ Nat.casesOn t k D) (n + 1 + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
by
    rw [degBound_succ, numBound_casesOn_succ, degBound_casesOn_succ, numBound_succ, degBound_succ,
      numBound_succ]
    ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case zero.refine_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ comap MvPolynomial.C '' S.toSet = ⇑(comapEquiv (isEmptyRingEquiv R (Fin 0))) '' S.toSet

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)

Tactic:
← sub_ne_zero (a := y)

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y - (-y - W.a₁ * x - W.a₃) ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case pos.a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ { a := 1,
        b :=
          -((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 -
              W.a₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
              (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -x₁ ^ 2 * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }.a =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
        c :=
          x₁ * x₁ + x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d := -(x₁ * x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.a

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
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 (c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE H).op))) s

Tactic:
rfl

Goal state after:
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✝³ : 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
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s

Tactic:
rfl

Goal state after:
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✝³ : 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
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
k : I
fkj : k ⟶ j
hk :
  (ConcreteCategory.hom (Scheme.Hom.app (D.map fkj) (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
      (((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ -
        ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))
          ⋯) =
    0
⊢ (TopologicalSpace.Opens.map (D.map fkj).base).obj ((TopologicalSpace.Opens.map (D.map fjx).base).obj (U x)) ⊓
      (TopologicalSpace.Opens.map (D.map fkj).base).obj ((TopologicalSpace.Opens.map (D.map fjy).base).obj (U y)) ≤
    D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)

Tactic:
rfl

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x : R[X]
y : W'.CoordinateRing
⊢ (mk (W'.map f)) (C ((mapRingHom f) x)) * (map W' f) y = (mk (W'.map f)) (C (Polynomial.map f x)) * (map W' f) y

Tactic:
rfl

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
⊢ Ideal.map (mk W') (span {C (X - C x), Y - C y}) =
    Ideal.map (Quotient.mkₐ R (span {W'.polynomial})) (span {C (X - C x), Y - C y})

Tactic:
rfl

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)),
      c :=
        x₁ * x₂ + x₁ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂) +
          x₂ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂),
      d := -(x₁ * x₂ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) }

Tactic:
grind

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
· apply nonsingular_negAdd_of_eval_derivative_ne_zero <| equation_negAdd h₁.left h₂.left hxy
      rw [derivative_addPolynomial_slope h₁.left h₂.left hxy]
      eval_simp
      simp only [neg_ne_zero, sub_self, mul_zero, add_zero]
      exact mul_ne_zero (sub_ne_zero_of_ne hx₁) (sub_ne_zero_of_ne hx₂)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
i : Fin 3
⊢ (W.addSubMap i).IsHomogeneous 2

Tactic:
simp only [addSubMap]
  fin_cases i <;>
    simp only [Fin.isValue, Fin.mk_one, Fin.zero_eta, Fin.reduceFinMk, Matrix.cons_val,
      Matrix.cons_val_one, Matrix.cons_val_zero]
  · exact isHomogeneous_X_pow .. |>.sub CXY |>.sub CXY |>.sub CXX
  · exact CXY.add CXY |>.add CXY |>.add CXX
  · exact isHomogeneous_X_pow .. |>.sub CXY

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((a + b + (c + d) - (d + c)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((a + b + (c + d) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((a + b + (c + d) - (d + b)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((a + b + (c + d) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((a + b + (c + d) - (d + a)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((a + b + (c + d) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ 2 ∣ a + b + (c + d)

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 3) = 2 * m + 1 + 5

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 2) + 1 = 2 * m + 5

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ ↑m + 1 + 1 + 1 = ↑m + 1 + 2

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ 2 * -(↑m + 1) + 1 = -(2 * ↑m + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -(↑m + 1) - 1 = -(↑m + 2)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n

Tactic:
normEDS,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ (preNormEDS (b ^ 4) c d (-n) * if Even (-n) then b else 1) = -(preNormEDS (b ^ 4) c d n * if Even n then b else 1)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)

Tactic:
normEDS,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (preNormEDS (b ^ 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (b ^ 4) c d (2 * k) * if Even (2 * k) then b else 1