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

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p ≫ f) ⁻¹' s)

Tactic:
← Category.assoc,

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑(((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p) ≫ f) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
let c : Cone F := (Under.pushout (f.appLE US UT hUST) ⋙ Under.forget _).mapCone
    (Under.liftCone (X.presheaf.mapCone c₀.op) _)

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
c : Cone F :=
  (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)).mapCone
    (Under.liftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX))
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = (Hom.toPartialMap (X ↘ S)).restrict f.domain ⋯ ⋯

Tactic:
by
  simp [PartialMap.ext_iff]

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

Goal state before:
pp: case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)

Tactic:
← Category.assoc,

Goal state after:
case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ (((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈
      ↑((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι ''ᵁ
          ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain ≫ g.hom) ⁻¹ᵁ h.domain) ↔
    x✝ ∈ ↑(f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)

Tactic:
← Category.assoc,

Goal state after:
case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈
      ↑((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι ''ᵁ
          (((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain) ≫ g.hom) ⁻¹ᵁ h.domain) ↔
    x✝ ∈ ↑(f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)
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₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| (X₁.isoOfEq ⋯).hom ≫
    (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
      (↑f.domain).homOfLE ⋯ ≫
        (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
          f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
← Category.assoc,

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| ((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
    (↑f.domain).homOfLE ⋯ ≫
      (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
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₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| ((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
    (↑f.domain).homOfLE ⋯ ≫
      (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
← Category.assoc,

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| (((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
      (↑f.domain).homOfLE ⋯) ≫
    (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
      f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
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
i : I
U : (D.obj i).Opens
j : Over i
⊢ c.π.app i ⁻¹ᵁ U ≤ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ U

Tactic:
by rw [← Scheme.Hom.comp_preimage, c.w]

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

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Field K
f : F →+* E
g : E →+* K
hf : f.IsPurelyInseparable
hg : g.IsPurelyInseparable
⊢ (g.comp f).IsPurelyInseparable

Tactic:
algebraize [f, g, g.comp f]
  exact IsPurelyInseparable.trans F E K

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
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
⊢ zeroLocus {g.val i} ⊆ zeroLocus {g.val j}

Tactic:
· rw [hi_min j (.symm hij), zeroLocus_singleton_zero]; exact Set.subset_univ _

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

Goal state before:
pp: 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
⊢ ∀ i_1 ∈ Finset.univ, (Function.update c.val j (c.val j %ₘ c.val i) i_1).degree.succ ≤ (c.val i_1).degree.succ

Tactic:
intro k _

Goal state after:
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
⊢ (Function.update c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).degree.succ
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case h
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ ((V { down := idx s }.down).ι ≫ 𝒰.f (f { down := idx s }.down)) ⟨x s, ⋯⟩ = s

Tactic:
simp [hx]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ g a ≫ i a ≫ 𝟙 (Y a) ≫ e a = 𝟙 (Y a) ≫ e a

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ (g a ≫ i a) ≫ 𝟙 (Y a) ≫ e a = 𝟙 (Y a) ≫ e a
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
a : α
⊢ f a ≫ x✝ = i a ≫ (g a ≫ f a) ≫ x✝

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
a : α
⊢ f a ≫ x✝ = (i a ≫ g a ≫ f a) ≫ x✝
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
a : α
⊢ f a ≫ x✝ = (i a ≫ g a ≫ f a) ≫ x✝

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
a : α
⊢ f a ≫ x✝ = ((i a ≫ g a) ≫ f a) ≫ x✝
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u

Tactic:
refine ⟨𝒰, fun i ↦ ?_⟩

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
⊢ ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₁ ^ 2 + 4 * W.a₂ = W.a₁ ^ 2

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

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

Tactic:
equation_zero,

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)

Tactic:
equation_zero,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
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)).Equation 0 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
equation_zero,

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

Tactic:
by
  simp only [b₂, b₄, b₆, b₈, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]
  ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ (C (X - C x)).natDegree < W'.polynomial.natDegree

Tactic:
rw [natDegree_polynomial, natDegree_C]; norm_num1

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

Goal state before:
pp: case add
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))
H : Ideal.span s₀ ≤ RingHom.ker g
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
q₃ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₄ : MvPolynomial (Fin m) R
hq₃ : q₃ ∈ Ideal.span s₀
⊢ ∃ q₁_1 q₂_1,
    q₁_1 ∈ Ideal.span s₀ ∧
      (commAlgEquiv R (Fin n) (Fin m)).symm (q₁ + σ q₂) + (commAlgEquiv R (Fin n) (Fin m)).symm (q₃ + σ q₄) =
        (commAlgEquiv R (Fin n) (Fin m)).symm (q₁_1 + σ q₂_1)

Tactic:
refine ⟨q₁ + q₃, q₂ + q₄, add_mem hq₁ hq₃, by simp only [map_add, add_add_add_comm]⟩

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a |b| * atom W c d - atom W a c * atom W |b| d + atom W a d * atom W |b| c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_abs_left odd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a |b| * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W |c| d - atom W a |c| * atom W b d + atom W a d * atom W b |c| =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_abs_left odd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W c d - atom W a |c| * atom W b d + atom W a d * atom W b |c| =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1), f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (2 * (m✝ + 1))) = complEDS' (f b) (f c) (f d) k (2 * (m✝ + 1))

Tactic:
simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1), f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (m✝ + 1)) * complEDS₂ (f b) (f c) (f d) ((↑m✝ + 1) * k) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) * complEDS₂ (f b) (f c) (f d) ((↑m✝ + 1) * k)