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

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ 𝟙 (Spec (CommRingCat.of K)) = ↑p ≫ f

Tactic:
p.2

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ 𝟙 (Spec (CommRingCat.of K)) = 𝟙 (Spec (CommRingCat.of K))
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) (IsLocalRing.closedPoint K) =
    (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) (IsLocalRing.closedPoint K)

Tactic:
simpa using H x hxS hx

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support fun i ↦ ⇑(F i)
h : (Function.support F).Finite
⊢ ⇑(∑ i ∈ h.toFinset, F i) = ∑ᶠ (i : ι), ⇑(F i)

Tactic:
Function.locallyFinsuppWithin.coe_sum

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support fun i ↦ ⇑(F i)
h : (Function.support F).Finite
⊢ ∑ n ∈ h.toFinset, ⇑(F n) = ∑ᶠ (i : ι), ⇑(F i)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ((PartialMap.id X).compHom f).toRationalMap = Hom.toRationalMap f

Tactic:
PartialMap.id_compHom

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (Hom.toPartialMap f).toRationalMap = Hom.toRationalMap f
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝⁴ : X.Over S
inst✝³ : Y.Over S
inst✝² : Z.Over S
f : X ⤏ Y
g : Y ⟶ Z
inst✝¹ : RationalMap.IsOver S f
inst✝ : Hom.IsOver g S
⊢ ∃ g_1, PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.compHom g

Tactic:
by
    obtain ⟨f, hf, rfl⟩ := f.exists_partialMap_over S
    exact ⟨f.compHom g, inferInstance, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X U S : Scheme
f : U ⟶ X
inst✝¹ : IsOpenImmersion f
inst✝ : IsDominant f
sX : X ⟶ S
sU : U ⟶ S
hf : f ≫ sX = sU
⊢ PartialIso.IsOver sU sX (partialIso f)

Tactic:
by simp [PartialIso.IsOver, hf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : (g₁.restrict W hW hW₁).hom = (g₂.restrict W hW hW₂).hom
⊢ (f.comp g₁).equiv (f.comp g₂)

Tactic:
replace e : g₁.restrict W hW hW₁ = g₂.restrict W hW hW₂ :=
    PartialMap.ext _ _ rfl (by simpa using e)

Goal state after:
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : g₁.restrict W hW hW₁ = g₂.restrict W hW hW₂
⊢ (f.comp g₁).equiv (f.comp g₂)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

Tactic:
rw [← f₃.toRationalMap_representative]

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.comp f₂).comp f₃.representative.toRationalMap = f₁.comp (f₂.comp f₃.representative.toRationalMap)
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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
choose i V hV hVi using fun x : s ↦ hs x.2

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)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = sSup s
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
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Goal state after:
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 φ
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
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
this :
  ∃ k hik hjk,
    (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hik ≫ (inv e).app i ≫ a =
      (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hjk ≫ (inv e).app j ≫ b
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
(inv e).naturality_assoc

Goal state after:
case inr
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
this : ∃ k hik hjk, (inv e).app k ≫ D.map hik ≫ a = (inv e).app k ≫ D.map hjk ≫ b
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i : 𝒰.I₀
⊢ d.transitionMap (𝟙 i) = (MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (𝟙 i)) ⋯).hom.app (d.cocone i).pt

Tactic:
apply (isColimitOfPreserves (Over.map ⊤ (d.prop_trans <| 𝟙 i)) (d.isColimit i)).hom_ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i : 𝒰.I₀
⊢ ∀ (j : J),
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j ≫ d.transitionMap (𝟙 i) =
      ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j ≫
        (MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (𝟙 i)) ⋯).hom.app (d.cocone i).pt
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)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
⊢ IsCompactOpenCovered f U

Tactic:
obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun V : s ↦ V.1) (fun V ↦ V.1.2) (by simp [← hs])

Goal state after:
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
⊢ IsCompactOpenCovered f U
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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
⊢ x ∈ ⋃ i, (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd ↔ x ∈ ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h)

Tactic:
Set.mem_iUnion

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
⊢ (∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd) ↔ ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)
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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
x✝ : ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)
i : ι
hi : i ∈ s
h : X i
hmem : h ∈ ⋃ i_1 ∈ Us ⟨i, hi⟩, ↑i_1
heq : f i h = x
⊢ ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd

Tactic:
Set.mem_iUnion

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
x✝ : ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)
i : ι
hi : i ∈ s
h : X i
hmem : ∃ i_1, h ∈ ⋃ (_ : i_1 ∈ Us ⟨i, hi⟩), ↑i_1
heq : f i h = x
⊢ ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
this : f x ∈ ⋃ i, ⋃ (x : i ∈ s), (fun a ↦ (𝒰.f i) a) '' ↑(V i ⋯)
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)

Tactic:
Set.mem_iUnion

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
this : ∃ i, ∃ (i_1 : i ∈ s), f x ∈ (fun a ↦ (𝒰.f i) a) '' ↑(V i ⋯)
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq✝ : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ ↑(V i ⋯)
heq : (fun a ↦ (𝒰.f i) a) y = f x
⊢ x ∈
    ⋃ i,
      ⋃ (x : i ∈ s),
        (fun a ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
          ↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯)

Tactic:
Set.mem_iUnion

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq✝ : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ ↑(V i ⋯)
heq : (fun a ↦ (𝒰.f i) a) y = f x
⊢ ∃ i,
    ∃ (i_1 : i ∈ s),
      x ∈
        (fun a ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
          ↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

Tactic:
c₄

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.twoTorsionPolynomial.discr = W.Δ

Tactic:
by
  linear_combination W.twoTorsionPolynomial_discr + 5 * W.Δ * CharP.cast_eq_zero R 3

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ W.j = 0 ↔ W.a₁ ^ 12 = 0

Tactic:
rw [j_of_char_two, Units.mul_right_eq_zero]

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
⊢ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      ((toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₃ ≠ 0 ∨
        (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₄ ≠ 0)

Tactic:
variableChange_a₃,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₆ = 0 ∧
      (↑{ u := 1, r := x, s := 0, t := y }.u⁻¹ ^ 3 *
            (W.a₃ + { u := 1, r := x, s := 0, t := y }.r * W.a₁ + 2 * { u := 1, r := x, s := 0, t := y }.t) ≠
          0 ∨
        (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).a₄ ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span {(mk W) (C (X - C x)) * (mk W) (C (X - C x))} ⊔
      (span {(mk W) (C (X - C x)) * (mk W) (Y - C (C y))} ⊔
        (span {(mk W) (C (X - C x)) * (mk W) (Y - C (C (W.negY x y)))} ⊔
          span
            {(AdjoinRoot.mk W.polynomial) (C (X - C x)) *
                (AdjoinRoot.mk W.polynomial)
                  (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)})) =
    XIdeal W x

Tactic:
← span_singleton_mul_span_singleton,

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span {(mk W) (C (X - C x))} * span {(mk W) (C (X - C x))} ⊔
      (span {(mk W) (C (X - C x))} * span {(mk W) (Y - C (C y))} ⊔
        (span {(mk W) (C (X - C x))} * span {(mk W) (Y - C (C (W.negY x y)))} ⊔
          span {(AdjoinRoot.mk W.polynomial) (C (X - C x))} *
            span
              {(AdjoinRoot.mk W.polynomial)
                  (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)})) =
    XIdeal W x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                ((mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span
          {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
              (XClass W x₁ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))} ⊔
      span
        {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
            (XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
← span_singleton_mul_span_singleton,

Goal state after:
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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
            span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
            (span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
              span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) ⊔
        span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
          (span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) ⊔
      span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
        (span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})