mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j✝ : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f j₁ ≫ f✝.hom = f j₂ ≫ f✝.hom

Tactic:
by simp [f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j✝ : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f✝.hom ≫ f j₁ = f✝.hom ≫ f j₂

Tactic:
by simp [f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
⊢ cG.ι.app j ≫ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app (Classical.arbitrary I)) ⋯ = s.ι.app j

Tactic:
by
    let f (i : _) : cG.pt ⟶ s.pt :=
      (hf i).desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) (by simp)
    have (i j : _) : f i = f j := by
      refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
      refine (hf j₁).hom_ext (by simp [f]) ?_
      rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]
    change _ ≫ f _ = _
    rw [this _ j]
    simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (SpecIso n R).inv)) (coord (Spec R) i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
by
  simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map,
    Quiver.Hom.unop_op, TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, CommRingCat.comp_apply]
  rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
      CommRingCat.comp_apply]
  congr 1
  exact map_X _ _

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = U \ {x | D x = 0 x}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | (fun x ↦ D x = 0 x) x})).Finite

Tactic:
rw [← this]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = U \ {x | D x = 0 x}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
⊢ ∑ᶠ (x : X), restrict (single x (F x)) ⋯ = F

Tactic:
have : (fun x ↦ (single x (F x)).restrict (subset_univ U)).support ⊆ h.toFinset := by
    intro
    contrapose
    aesop

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
⊢ ∑ᶠ (x : X), restrict (single x (F x)) ⋯ = F
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s) =
    0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
← RingHom.mem_ker,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
← RingHom.mem_ker,

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem,
    RingHom.mem_ker] at hx

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      ((algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

case refine_2.hy
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x *
      IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsUnit (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this : IsAffine ↑V
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
suffices ∀ (U₀ V₀) (eU : U = U₀) (eV : V = V₀),
      f.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_left) =
        g.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_right) by
    rw [← cancel_mono V.toScheme.isoSpec.hom]
    simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
    congr 2
    apply this <;> simp

Goal state after:
case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this : IsAffine ↑V
⊢ ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
⊢ ∃ V,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'

Tactic:
obtain ⟨V', hxV', hV', iV'V, H⟩ := X.exists_le_and_germ_injective x V hxV

Goal state after:
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
⊢ ∃ V,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X.PartialIso Y
hf : IsOver sX sY f
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.source
⊢ IsOver sX sY (f.restrictSource U hU hU')

Tactic:
by
  simp [IsOver, hf]

Goal state after:
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
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
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
⊢ IsAffine (A.𝒰D.X j)

Tactic:
dsimp [𝒰D]

Goal state after:
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✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
⊢ IsAffine ((A.𝒰D₀.X j.fst).affineCover.X j.snd)
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)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
⊢ IsCompactOpenCovered f U

Tactic:
have (i : ι) (hi : i ∈ s) : IsOpen (t i) := by
      rw [← Set.mk_preimage_sigma (t := t) hi]
      exact isOpen_sigma_iff.mp (heq' ▸ V.2) i

Goal state after:
case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (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)
U : Set S
⊢ IsCompactOpenCovered f U ↔ IsCompactOpenCovered (fun x p ↦ f p.fst p.snd) U

Tactic:
classical
  rw [iff_of_unique (ι := Unit)]
  refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩
  · refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
    · intro i
      by_cases h : i ∈ s
      · simpa [h] using (V _ _).2
      · simp [h]
    · dsimp only
      exact Set.isCompact_sigma hs fun i ↦ (by simp_all)
    · aesop
  · obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq
    have (i : ι) (hi : i ∈ s) : IsOpen (t i) := by
      rw [← Set.mk_preimage_sigma (t := t) hi]
      exact isOpen_sigma_iff.mp (heq' ▸ V.2) i
    refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
    simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]

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
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered f t
⊢ IsCompactOpenCovered f U

Tactic:
by
  have := hf.to_subtype
  exact of_iUnion_eq_of_finite (fun i : s ↦ i.1) (by simpa) (by simpa)

Goal state after:
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 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, u_2} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
⊢ pullback.fst (D.obj a).hom (𝒰.f i) ≫ (d.gluedCocone.ι.app a).left =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
by
  simp only [gluedCocone]
  generalize_proofs _ _ _ _ _ _ _ _ _ _ _ _ h1 h2
  let 𝒱 : (D.obj a).left.OpenCover := 𝒰.pullback₁ (D.obj a).hom
  apply 𝒱.map_glueMorphismsOverOfLocallyDirected_left _ h1 h2

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✝ : IsReduced R
⊢ W.j = 0 ↔ W.c₄ = 0

Tactic:
by
  rw [j_eq_zero_iff', pow_eq_zero_iff three_ne_zero]

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

Goal state before:
pp: case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ ↑C.u⁻¹ * ↑C'.u⁻¹ * (W.a₁ + 2 * (↑C'.u * C.s + C'.s)) = ↑C.u⁻¹ * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s) + 2 * C.s)

Tactic:
linear_combination ↑C.u⁻¹ * C.s * 2 * C'.u.inv_mul

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)

Tactic:
simp only [b₂, b₄, variableChange_a₁, variableChange_a₃, variableChange_a₄]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 2 * (↑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)) +
      ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    ↑C.u⁻¹ ^ 4 * (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (W.a₁ ^ 2 + 4 * W.a₂) + 6 * C.r ^ 2)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT : comap MvPolynomial.C '' S'.toSet = T.toSet
hT' :
  ∀ C ∈ T,
    C.n ≤ MvPolynomialC.numBound (k + n) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          Submodule.restrictScalars ℤ (degreesLE R (Fin n) Finset.univ.val) ^
            MvPolynomialC.degBound (k + n) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
i : Fin C.n
j : Fin n
⊢ degreeOf j (C.g i) ≤ degBound k m n d

Tactic:
· have := (hT' C hCT).2 i
    rw [← Submodule.restrictScalars_pow (MvPolynomialC.degBound_pos ..).ne', ← degreesLE_nsmul,
      Submodule.restrictScalars_mem, mem_degreesLE,
        Multiset.le_iff_count] at this
    simpa only [Multiset.count_nsmul, Multiset.count_univ, mul_one, ← degreeOf_def]
      using! this j

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

Goal state before:
pp: case some.some.mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0

Tactic:
exact fun ⟨hx, hy⟩ => add_of_Y_eq hx hy

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
P Q : W.Point
h : xRep 0 = xRep 0
⊢ 0 = 0 ∨ 0 = -0

Tactic:
exact .inl rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
⊢ (W.toCharTwoNF • W).IsCharTwoNF

Tactic:
by_cases ha₁ : W.a₁ = 0

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
ha₁ : W.a₁ = 0
⊢ (W.toCharTwoNF • W).IsCharTwoNF

case neg
R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
ha₁ : ¬W.a₁ = 0
⊢ (W.toCharTwoNF • W).IsCharTwoNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case odd.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ (if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤ if Even m then 0 else 2 * 3

Tactic:
split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case odd.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ (if Even m then W.Ψ₂Sq ^ 2 else 1).natDegree ≤ if Even m then 2 * 3 else 0

Tactic:
split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

Goal state after: