mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor =
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor

Tactic:
]

Goal state after:
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
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor =
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor
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: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap ↑R ↑A))).FiniteType

Tactic:
]

Goal state after:
R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap ↑R ↑A))).FiniteType
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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map (f ≫ g) ≅ map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    map₂ (f ◁ η) = (mapComp f g).hom ≫ map f ◁ map₂ η ≫ (mapComp f h).inv
map₂_whisker_right :
  ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    map₂ (η ▷ h) = (mapComp f h).hom ≫ map₂ η ▷ map h ≫ (mapComp g h).inv
a b : B
f : a ⟶ b
⊢ 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f

Tactic:
]

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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map (f ≫ g) ≅ map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    map₂ (f ◁ η) = (mapComp f g).hom ≫ map f ◁ map₂ η ≫ (mapComp f h).inv
map₂_whisker_right :
  ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    map₂ (η ▷ h) = (mapComp f h).hom ≫ map₂ η ▷ map h ≫ (mapComp g h).inv
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = (mapComp (𝟙 a) f).hom ≫ eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)

Tactic:
]

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

Goal state before:
pp: case e'_2.e_a
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)
⊢ (pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom =
    Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv

Tactic:
]

Goal state after:
case e'_2.e_a
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)
⊢ (pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom =
    Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv
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))
⊢ (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) =
    f

Tactic:
by ext1; 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 = p ◁ η ≪≫ p ◁ θ ≪≫ η_h

Tactic:
]

Goal state after:
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 = p ◁ η ≪≫ p ◁ θ ≪≫ η_h
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e_a
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)
⊢ (map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
        map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
      (pullbackSpecIso R S S).inv =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯

Tactic:
]

Goal state after:
case e_a
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)
⊢ (map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
        map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
      (pullbackSpecIso R S S).inv =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯
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 : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
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 = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
]

Goal state after:
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 = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_4
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = P'
⊢ e' (Fin.castSucc 0) ∉ Fin.cons (↑P'φ) Q' 0

Tactic:
rw [← hP'φ] at heP'; simpa [he'0]

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 = η_g

Tactic:
]

Goal state after:
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 = η_g
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
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ (pullbackSpecIso' R T S).inv ≫ pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
]

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
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ (pullbackSpecIso' R T S).inv ≫ pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
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
this : (↑(Algebra.TensorProduct.comm R S T)).comp ↑includeRight = includeLeftRingHom
⊢ (pullbackSpecIso' R T S).inv ≫ pullback.fst (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
]

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
this : (↑(Algebra.TensorProduct.comm R S T)).comp ↑includeRight = includeLeftRingHom
⊢ (pullbackSpecIso' R T S).inv ≫ pullback.fst (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: 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✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫ pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
]

Goal state after:
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✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫ pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
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
⊢ 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))) =
    pullback.fst
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom ≫
      Over.Hom.left
          (Hom.asOver
            ((pullbackSymmetry (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
        Spec.map (ofHom ↑includeRight)

Tactic:
]

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))) =
    pullback.fst
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom ≫
      Over.Hom.left
          (Hom.asOver
            ((pullbackSymmetry (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
        Spec.map (ofHom ↑includeRight)
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
⊢ 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.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    pullback.snd
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom ≫
      Over.Hom.left
          (Hom.asOver
            ((pullbackSymmetry (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
        Spec.map (ofHom ↑includeRight)

Tactic:
]

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.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.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    pullback.snd
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom
        (OverClass.asOver (pullback (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
            (Spec (of S))).hom ≫
      Over.Hom.left
          (Hom.asOver
            ((pullbackSymmetry (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
        Spec.map (ofHom ↑includeRight)
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
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ {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 = n + 1
q : Ideal S
hq : q.IsPrime
hq' : q.LiesOver p
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
left✝ : Module.Finite R' (Localization.Away e)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
F : ↑(P.primesOver (R' ⊗[R] S)) ≃o ↑(p.primesOver S) := Ideal.fiberIsoOfBijectiveResidueField hpP
⊢ Nat.card ↑(p.primesOver S) ≤ Nat.card ↑(p.primesOver S)

Tactic:
]

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

Goal state before:
pp: 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
⊢ 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 =
    Over.Hom.left η ≫ (pullbackSpecIso' R S T).inv

Tactic:
]

Goal state after:
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
⊢ 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 =
    Over.Hom.left η ≫ (pullbackSpecIso' R S T).inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)

Tactic:
]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)