mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 0 < 5
⊢ (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
    else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * (↑(0 - (0 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩

pp: case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
    else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * (↑(0 - (1 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩

pp: case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
    else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * (↑(0 - (2 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩

pp: case «0».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
    else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * (↑(0 - (3 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩

pp: case «0».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 = 0 then f.coeff (0 - 4) else 0
    else if 4 ≤ 2 then f.coeff (0 - (4 - 2) + 1) * (↑(0 - (4 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨4, hj⟩

Tactic:
<;>

Goal state after:
case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 0 < 5
⊢ (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
    else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * (↑(0 - (0 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩

case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
    else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * (↑(0 - (1 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩

case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
    else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * (↑(0 - (2 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩

case «0».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
    else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * (↑(0 - (3 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩

case «0».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 = 0 then f.coeff (0 - 4) else 0
    else if 4 ≤ 2 then f.coeff (0 - (4 - 2) + 1) * (↑(0 - (4 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
    else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * (↑(1 - (0 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩

pp: case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
    else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * (↑(1 - (1 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩

pp: case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
    else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * (↑(1 - (2 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩

pp: case «1».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
    else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * (↑(1 - (3 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩

pp: case «1».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 1 then f.coeff (1 - 4) else 0
    else if 4 ≤ 3 then f.coeff (1 - (4 - 2) + 1) * (↑(1 - (4 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨4, hj⟩

Tactic:
<;>

Goal state after:
case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
    else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * (↑(1 - (0 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩

case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
    else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * (↑(1 - (1 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩

case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
    else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * (↑(1 - (2 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩

case «1».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
    else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * (↑(1 - (3 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩

case «1».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 1 then f.coeff (1 - 4) else 0
    else if 4 ≤ 3 then f.coeff (1 - (4 - 2) + 1) * (↑(1 - (4 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «4».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 0 < 5
⊢ (if 0 = 1 then 1 else if 0 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨0, hj⟩

pp: case «4».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 1 < 5
⊢ (if 1 = 1 then 1 else if 1 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨1, hj⟩

pp: case «4».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 2 < 5
⊢ (if 2 = 1 then 1 else if 2 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨2, hj⟩

pp: case «4».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 3 < 5
⊢ (if 3 = 1 then 1 else if 3 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨3, hj⟩

pp: case «4».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 4 < 5
⊢ (if 4 = 1 then 1 else if 4 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨4, hj⟩

Tactic:
<;>

Goal state after:
case «4».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 0 < 5
⊢ (if 0 = 1 then 1 else if 0 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨0, hj⟩

case «4».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 1 < 5
⊢ (if 1 = 1 then 1 else if 1 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨1, hj⟩

case «4».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 2 < 5
⊢ (if 2 = 1 then 1 else if 2 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨2, hj⟩

case «4».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 3 < 5
⊢ (if 3 = 1 then 1 else if 3 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨3, hj⟩

case «4».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 4 < 5
⊢ (if 4 = 1 then 1 else if 4 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨4, hj⟩
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case ofNat
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
a✝ : ℕ
⊢ (f ^ Int.ofNat a✝).hom.hom = f.hom.hom ^ Int.ofNat a✝

pp: case negSucc
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
a✝ : ℕ
⊢ (f ^ Int.negSucc a✝).hom.hom = f.hom.hom ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
a✝ : ℕ
⊢ (f ^ Int.ofNat a✝).hom.hom = f.hom.hom ^ Int.ofNat a✝

case negSucc
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
a✝ : ℕ
⊢ (f ^ Int.negSucc a✝).hom.hom = f.hom.hom ^ Int.negSucc a✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam (α.homEquiv' (snd X X) * α.homEquiv' (fst X X) = α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
    mul_comm._autoParam

Tactic:
_root_.mul_comm

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
⊢ QuasiFiniteAt f x

Tactic:
have hxU : f x ∈ U := by
    convert! show _ ∈ U from (normalization f).basicOpen_le _ hxV
    rw [← Scheme.Hom.comp_apply, f.toNormalization_fromNormalization]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
hxU : f x ∈ U
⊢ QuasiFiniteAt f x
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ F.mapId x ≫ eqToHom ⋯ = 𝟙 (𝟙 (F.obj x))

Tactic:
simp [F.mapId_eq_eqToHom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ eqToHom ⋯ ≫ F.mapId x = 𝟙 (F.map (𝟙 x))

Tactic:
simp [F.mapId_eq_eqToHom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝¹ : a✝ ⟶ b✝
x✝ : b✝ ⟶ c✝
⊢ ((F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x✝¹ x✝).hom = (eqToIso ⋯).hom

Tactic:
simp [StrictPseudofunctor.mapComp_eq_eqToIso,
      PrelaxFunctor.map₂_eqToHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝ R A : CommRingCat
inst✝ : Bialgebra ↑R ↑A
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A)) ≫ ((Spec A).asOver (Spec R)).hom =
    ((algSpec R).obj (𝟙_ (CommAlgCat ↑R)ᵒᵖ)).hom

Tactic:
by simp [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
            CommRingCat.of_carrier]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₀
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
this : includeLeftRingHom = algebraMap S (S ⊗[R] T)
⊢ (Over.Hom.left
          (μ ≫
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S))) ≫
            μ) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
simp [Scheme.monObjAsOverPullback_mul, pullbackSpecIso', specOverSpec_over, ← Spec.map_comp,
        ← CommRingCat.ofHom_comp, OverClass.asOver, mul_spec_asOver_spec_left, this, Hom.asOver,
        OverClass.asOverHom, pullback.condition]

Goal state after:
case h₀
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
this : includeLeftRingHom = algebraMap S (S ⊗[R] T)
⊢ pullback.snd (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    pullback.snd (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) ↘ Spec (of S))
        (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) ↘ Spec (of S)) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑C
⊢ F.toFunctor.map (adj.unit.toNatTrans.app X) ≫ adj.counit.toNatTrans.app (F.toFunctor.obj X) = 𝟙 (F.toFunctor.obj X)

Tactic:
by
    simpa using congr($(adj.left_triangle).toNatTrans.app X)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
⊢ (mateEquiv adj₁ adj₂) α = 𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)

Tactic:
rw [mateEquiv_apply, Adjunction.homEquiv₂_apply, Adjunction.homEquiv₁_apply]
  bicategory

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
⊢ (∀ (p : PrimeSpectrum R), p ∈ Set.range (comap (algebraMap R S))) ↔ Set.range (comap (algebraMap R S)) = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
⊢ 1 ≤ finrank f ↔ Surjective f

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ ?_⟩
  · wlog hY : ∃ R, Y = Spec R
    · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Surjective) Y.affineCover]
      intro i
      dsimp only [Scheme.Cover.pullbackHom]
      refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
      rw [finrank_pullback_snd]
      exact h _
    obtain ⟨R, rfl⟩ := hY
    wlog hX : ∃ S, X = Spec S
    · have _ : IsAffine X := isAffine_of_isAffineHom f
      rw [← MorphismProperty.cancel_left_of_respectsIso @Surjective X.isoSpec.inv]
      refine this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
      rw [finrank_comp_left_of_isIso]
      exact h x
    obtain ⟨S, rfl⟩ := hX
    obtain ⟨φ, rfl⟩ := Spec.map_surjective f
    constructor
    intro x
    specialize h x
    simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
    rw [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
    algebraize [φ.hom]
    exact (PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap _).mp h
  · intro y
    obtain ⟨x, rfl⟩ := f.surjective y
    exact one_le_finrank_map f x

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case pos.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

pp: case pos.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

Tactic:
<;>

Goal state after:
case pos.top
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (⊤ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ⊤ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'

case pos.coe
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
x y : R
_✝ : x * y ∈ nonZeroDivisors R
_ : x ∈ nonZeroDivisors R
b : y ∈ nonZeroDivisors R
y' : ℕ∞
a✝ : ℕ
⊢ ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (↑a✝ + y') =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑a✝ * ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) y'
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : R
ha : a ∈ R⁰
⊢ (ordMonoidWithZeroHom R) a ≠ 0

Tactic:
lift a to R⁰ using ha

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : ↥R⁰
⊢ (ordMonoidWithZeroHom R) ↑a ≠ 0
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a b : R
ha : a ∈ R⁰
hb : b ∈ R⁰
⊢ ord R a ≤ ord R b ↔ (ordMonoidWithZeroHom R) a ≤ (ordMonoidWithZeroHom R) b

Tactic:
lift a to R⁰ using ha

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
b : R
hb : b ∈ R⁰
a : ↥R⁰
⊢ ord R ↑a ≤ ord R b ↔ (ordMonoidWithZeroHom R) ↑a ≤ (ordMonoidWithZeroHom R) b
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ
⊢ (fun I ↦ zeroLocus 𝒜 ↑I) I ≤ t ↔ I ≤ (fun t ↦ vanishingIdeal t) t

Tactic:
simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using!
    subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asHomogeneousIdeal.toSubmodule

pp: case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asHomogeneousIdeal.toSubmodule

Tactic:
<;>

Goal state after:
case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asHomogeneousIdeal.toSubmodule

case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asHomogeneousIdeal.toSubmodule
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal → ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

pp: case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ (∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u) → f ∉ z.asHomogeneousIdeal

Tactic:
<;>

Goal state after:
case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal → ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ (∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u) → f ∉ z.asHomogeneousIdeal