mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
x✝ : S
⊢ ((algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)).comp TensorProduct.includeRight.toRingHom) x✝ =
    TensorProduct.includeRight.toRingHom x✝

Tactic:
;

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
x✝ : S
⊢ ((algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)).comp TensorProduct.includeRight.toRingHom) x✝ =
    TensorProduct.includeRight.toRingHom x✝
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsProper (pullback.snd G.hom f)

Tactic:
;

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
⊢ IsProper (pullback.snd G.hom f)
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this : IsProper G'.hom
⊢ IsIntegral (pullback (pullback.snd G.hom f) (pullback.snd G.hom f))

Tactic:
;

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
G' : Over (Spec (CommRingCat.of (AlgebraicClosure K))) := (Over.pullback f).obj G
this : IsProper G'.hom
⊢ IsIntegral (pullback (pullback.snd G.hom f) (pullback.snd G.hom f))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ x ∈ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x}

Tactic:
refine ⟨⟨x, hxV⟩, show (f.resLE _ _ _).QuasiFiniteAt _ from ?_, rfl⟩

Goal state after:
case inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ QuasiFiniteAt (resLE f U V hVU) ⟨x, hxV⟩
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ 0 = (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨0, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ 0 = (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨0, ⋯⟩
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
x : ↥↑(f ⁻¹ᵁ V)
H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ False

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
x : ↥↑(f ⁻¹ᵁ V)
H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ False
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a✝ : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x y : T ⊗[R] ↥(Submodule.restrictScalars R I)
a : T ⊗[R] I.Cotangent
ha :
  (tensorCotangentHom R T I) a =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩
b : T ⊗[R] I.Cotangent
hb :
  (tensorCotangentHom R T I) b =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩
⊢ (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩ +
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩ =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x +
          (LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y,
        ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a✝ : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x y : T ⊗[R] ↥(Submodule.restrictScalars R I)
a : T ⊗[R] I.Cotangent
ha :
  (tensorCotangentHom R T I) a =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩
b : T ⊗[R] I.Cotangent
hb :
  (tensorCotangentHom R T I) b =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩
⊢ (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩ +
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩ =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x +
          (LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y,
        ⋯⟩
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (f ≫ g)

Tactic:
;

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (f ≫ g)
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✝ = eqToIso ⋯

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

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

Goal state before:
pp: R : CommRingCat
⊢ PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (Over.post Γ.rightOp ⋙
      Over.map (ΓSpecIso R).inv.op ⋙ (Over.opEquivOpUnder R).functor ⋙ (commAlgCatEquivUnder R).inverse.op)

Tactic:
;

Goal state after:
R : CommRingCat
⊢ PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (Over.post Γ.rightOp ⋙
      Over.map (ΓSpecIso R).inv.op ⋙ (Over.opEquivOpUnder R).functor ⋙ (commAlgCatEquivUnder R).inverse.op)
Module: Mathlib.Tactic.CategoryTheory.BicategoricalComp

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ

Tactic:
;

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ (preservesTerminalIso (algSpec R)).hom = (Over.isoMk (Iso.refl (Spec R)) ⋯).hom

Tactic:
;

Goal state after:
R : CommRingCat
⊢ (preservesTerminalIso (algSpec R)).hom = (Over.isoMk (Iso.refl (Spec R)) ⋯).hom
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.isoMk (Iso.refl (Spec R)) ⋯).inv = 𝟙 (Spec R)

Tactic:
;

Goal state after:
R : CommRingCat
⊢ Over.Hom.left (Over.isoMk (Iso.refl (Spec R)) ⋯).inv = 𝟙 (Spec R)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (Over.isoMk (Iso.refl (Spec R)) ⋯).hom

Tactic:
;

Goal state after:
R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (Over.isoMk (Iso.refl (Spec R)) ⋯).hom
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv

Tactic:
;

Goal state after:
R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e'_2.e_a.h₀
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)

Tactic:
;

Goal state after:
case e'_2.e_a.h₀
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₁
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)

Tactic:
;

Goal state after:
case h₁
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ Spec.map (CommRingCat.ofHom ↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) =
    Spec.map (CommRingCat.ofHom ↑↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)) ≫
      Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ Over.Hom.left
      ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)))
        ((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
          f)) =
    Over.Hom.left f

Tactic:
;

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ Over.Hom.left
      ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)))
        ((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
          f)) =
    Over.Hom.left f
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η η' : g ⟶ h
θ : f ≫ g ⟶ f ≫ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
by
  simp [e_η, e_θ]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η η' : f ⟶ g
θ : f ≫ h ⟶ g ≫ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
by
  simp [e_η, e_θ]

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

Goal state before:
pp: case e_a.h₀
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
x✝ : S
⊢ ((↑((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv))).comp
        Algebra.TensorProduct.includeLeftRingHom)
      x✝ =
    ↑f.ofConv x✝

Tactic:
;

Goal state after:
case e_a.h₀
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
x✝ : S
⊢ ((↑((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv))).comp
        Algebra.TensorProduct.includeLeftRingHom)
      x✝ =
    ↑f.ofConv x✝
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₁
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
x✝ : S
⊢ (((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    g.ofConv x✝

Tactic:
;

Goal state after:
case h₁
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
x✝ : S
⊢ (((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    g.ofConv x✝
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(AlgHom.id R p.ResidueField)

Tactic:
;

Goal state after:
case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(AlgHom.id R p.ResidueField)