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

Goal state before:
pp: X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝⁴ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝³ : LocallyQuasiFinite f
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ Scheme.Hom.toNormalization f =
    X.topIso.inv ≫ (X.isoOfEq ⋯).inv ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f

Tactic:
simp

Goal state after:
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)
⊢ f ((f ⁻¹ᵁ V).ι x) = f ↑x

Tactic:
simp

Goal state after:
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
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
x : ↥I
⊢ (Submodule.mkQ (map a I ^ 2)) ↑⟨1 ⊗ₜ[R] ↑x, ⋯⟩ = (Quotient.mk (map a I ^ 2)) (1 ⊗ₜ[R] ↑x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring) (1 ⊗ₜ[P.Ring] 0) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case mem
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
y : P.Ring
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring)
        (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) ((KaehlerDifferential.D R P.Ring) y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hc₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ 0 ∘ₗ 0 = 0 ∘ₗ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hc₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ 0 ∘ₗ 0 = ↑R (P.tensorToH1Cotangent T) ∘ₗ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hc₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
x✝¹ : T
x✝ : P.H1Cotangent
⊢ (((AlgebraTensorModule.curry (↑R h1Cotangentι ∘ₗ ↑R (P.tensorToH1Cotangent T))) x✝¹) x✝).val =
    (((AlgebraTensorModule.curry
            (↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) ∘ₗ LinearMap.lTensor T (↑R h1Cotangentι)))
          x✝¹)
        x✝).val

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

Tactic:
simp

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

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).obj x✝ = F.obj x✝

Tactic:
simp

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

Goal state before:
pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝² x✝¹ : B
x✝ : x✝² ⟶ x✝¹
⊢ (F.comp (id C)).map x✝ = F.map x✝

Tactic:
simp

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

Goal state before:
pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ (F.comp (id C)).map₂ x✝ = F.map₂ x✝

Tactic:
simp

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

Goal state before:
pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).mapId x✝ = F.mapId x✝

Tactic:
simp

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

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ x✝² : B
x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝³ ⟶ x✝²
⊢ (F.comp (id C)).mapComp x✝¹ x✝ = F.mapComp x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).obj x✝ = F.obj x✝

Tactic:
simp

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

Goal state before:
pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝² x✝¹ : B
x✝ : x✝² ⟶ x✝¹
⊢ ((id B).comp F).map x✝ = F.map x✝

Tactic:
simp

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

Goal state before:
pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ ((id B).comp F).map₂ x✝ = F.map₂ x✝

Tactic:
simp

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

Goal state before:
pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).mapId x✝ = F.mapId x✝

Tactic:
simp

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

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ x✝² : B
x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝³ ⟶ x✝²
⊢ ((id B).comp F).mapComp x✝¹ x✝ = F.mapComp x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case obj
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝ : B
⊢ ((F.comp G).comp H).obj x✝ = (F.comp (G.comp H)).obj x✝

Tactic:
simp

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

Goal state before:
pp: case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝² x✝¹ : B
x✝ : x✝² ⟶ x✝¹
⊢ ((F.comp G).comp H).map x✝ = (F.comp (G.comp H)).map x✝

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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
⊢ η ⊗≫ θ = η ≫ θ

Tactic:
dsimp [bicategoricalComp]; simp

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

Goal state before:
pp: case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ ((F.comp G).comp H).map₂ x✝ = (F.comp (G.comp H)).map₂ x✝

Tactic:
simp

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

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (LaxMonoidal.ε (algSpec R))

Tactic:
simp

Goal state after:
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)).hom ⋯) =
    Over.Hom.left (LaxMonoidal.μ (algSpec R) X Y)

Tactic:
simp

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

Goal state before:
pp: case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝ : B
⊢ ((F.comp G).comp H).mapId x✝ = (F.comp (G.comp H)).mapId x✝

Tactic:
simp

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

Goal state before:
pp: case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝⁴ x✝³ x✝² : B
x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝³ ⟶ x✝²
⊢ ((F.comp G).comp H).mapComp x✝¹ x✝ = (F.comp (G.comp H)).mapComp x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
p : a ⟶ b
f : b ⟶ c
g : c ⟶ d
h : d ⟶ e
pf : a ⟶ c
pfg : a ⟶ d
pfgh : a ⟶ e
η_f : p ≫ f ≅ pf
η_g : pf ≫ g ≅ pfg
η_h : pfg ≫ h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
simp

Goal state after:
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 ◁ᵢ α).hom = (f ◁ᵢ α).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ Iso.refl f ≪≫ η_f).hom = η_f.hom

Tactic:
simp

Goal state after:
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 : WithConv (S →ₐ[R] T)
⊢ ↑((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
          ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R))) f)).ofConv =
    ↑f.ofConv

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ (p ◁ (η ≪≫ θ) ≪≫ η_h).hom = (p ◁ η ≪≫ p ◁ θ ≪≫ η_h).hom

Tactic:
simp

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
α : f ≅ g
h : b ⟶ c
⊢ α.hom ▷ h = α.hom ▷ h

Tactic:
simp

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
η : f ⟶ g
h : b ⟶ c
⊢ η ▷ h = (Iso.refl (f ≫ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ≫ h)).hom

Tactic:
simp

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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp

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

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Over.Hom.left
        (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))
          (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
      pullback.fst (Over.mk (Spec.map (ofHom (algebraMap R T))) ⊗ Over.mk (Spec.map (ofHom (algebraMap R T)))).hom
        (Spec.map (ofHom (algebraMap R S))) =
    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 S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) includeRight.toRingHom includeRight.toRingHom ⋯ ⋯)) ≫
          (pullbackSpecIso R T T).inv

Tactic:
simp

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Over.Hom.left
        (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))
          (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
      pullback.fst
        (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
          Spec.map (ofHom (algebraMap R T)))
        (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫ (pullbackSpecIso R T T).inv
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: 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 = ∅
⊢ ∑ i, 1 i = 1

Tactic:
simp

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

Goal state before:
pp: case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (Over.Hom.left
          (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S))))
            (Over.mk (Spec.map (ofHom (algebraMap R T)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
        pullback.fst
          (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
            Spec.map (ofHom (algebraMap R T)))
          (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) =
    (Over.Hom.left
          (Hom.asOver
              ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
                (pullbackSpecIso' R S T).hom)
              (Spec (of S)) ⊗ₘ
            Hom.asOver
              ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
                (pullbackSpecIso' R S T).hom)
              (Spec (of S))) ≫
        (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
          Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
simp

Goal state after:
case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.fst (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.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫
          Spec.map (ofHom includeLeftRingHom)