mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (preservesTerminalIso (algSpec R)).inv = 𝟙 (Spec R)

Tactic:
by

Goal state after:
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
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
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
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'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝² : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝¹ : (↑P'φ).LiesOver P
this✝ : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
this : ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''
⊢ e' (Fin.last (n + 1)) ∈ P''

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ≫ ((algSpec R).obj X ⊗ (algSpec R).obj Y).hom =
    ((algSpec R).obj (X ⊗ Y)).hom

Tactic:
by

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

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

Goal state after:
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
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
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
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'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝² : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝¹ : (↑P'φ).LiesOver P
this✝ : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
this : ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''
⊢ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Fin.cons (↑P'φ) Q' i.succ

Tactic:
by

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

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

Tactic:
by

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
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ (F.comp G).comp H = F.comp (G.comp H)

Tactic:
by

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)).inv ⋯) =
    Over.Hom.left (OplaxMonoidal.δ (algSpec R) X Y)

Tactic:
by

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

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec A ↘ Spec R)

Tactic:
by

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

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
a b : B
f : a ⟶ b
⊢ map (𝟙 a) ≫ map f = 𝟙 (obj a) ≫ map f

Tactic:
by

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 ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)

Tactic:
by

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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (S.mapComp f x✝¹).hom ≫ S.map f ◁ S.map₂ η ≫ (S.mapComp f x✝).inv

Tactic:
by

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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (S.mapComp f✝ f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g✝ f).inv

Tactic:
by

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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (S.mapComp (f ≫ g) h).hom ≫
      (S.mapComp f g).hom ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (S.mapComp g h).inv ≫ (S.mapComp f (g ≫ h)).inv

Tactic:
by

Goal state after:
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
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
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
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'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝² : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝¹ : (↑P'φ).LiesOver P
this✝ : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
this : ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''
x✝ : e' (Fin.castSucc 0) ∉ P''
⊢ (AlgHom.restrictScalars R φ).comp TensorProduct.includeRight = TensorProduct.includeRight

Tactic:
by

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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = (S.mapComp (𝟙 a✝) f).hom ≫ (eqToIso ⋯).hom ▷ S.map f ≫ (λ_ (S.map f)).hom

Tactic:
by

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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (ρ_ f).hom = (S.mapComp f (𝟙 b✝)).hom ≫ S.map f ◁ (eqToIso ⋯).hom ≫ (ρ_ (S.map f)).hom

Tactic:
by

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 : StrictlyUnitaryPseudofunctor B C
x : B
⊢ F.toLax.map (𝟙 x) = 𝟙 (F.toLax.obj x)

Tactic:
by

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 : StrictlyUnitaryPseudofunctor B C
x : B
⊢ F.toLax.mapId x = eqToHom ⋯

Tactic:
by

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✝ F : StrictlyUnitaryPseudofunctor B C
G : StrictlyUnitaryPseudofunctor C D
x✝ : B
⊢ (F.comp G.toPseudofunctor).map (𝟙 x✝) = 𝟙 ((F.comp G.toPseudofunctor).obj x✝)

Tactic:
by

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✝ F : StrictlyUnitaryPseudofunctor B C
G : StrictlyUnitaryPseudofunctor C D
x✝ : B
⊢ (F.comp G.toPseudofunctor).mapId x✝ = eqToIso ⋯

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ η.symm.hom = η.inv

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (f ◁ᵢ η').hom = f ◁ η

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (η' ▷ᵢ h).hom = η ▷ h

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b : B
f g h i : a ⟶ b
inst✝ : BicategoricalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
by

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

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

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
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
by

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
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
by

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

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 : a ⟶ b
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
by

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

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

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

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
⊢ (β_ ((Spec A).asOver (Spec R)) ((Spec A).asOver (Spec R))).hom ≫ μ = μ

Tactic:
by

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 i j : b ⟶ c
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ≫ i ⟶ f ≫ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (f ◁ᵢ α).hom ≫ f ◁ η ≫ θ

Tactic:
by

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

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✝¹ : Algebra R S
inst✝ : Algebra R T
f : S →ₐ[R] T
⊢ Spec.map (CommRingCat.ofHom f.toRingHom) ≫ Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R) =
    Spec (CommRingCat.of T) ↘ Spec (CommRingCat.of R)

Tactic:
by

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))
⊢ ∀ (r : R), (↑↑(CommRingCat.Hom.hom (preimage (Over.Hom.left f)))).toFun ((algebraMap R S) r) = (algebraMap R T) r

Tactic:
suffices CommRingCat.ofHom (algebraMap R S) ≫ Spec.preimage f.left =
      CommRingCat.ofHom (algebraMap R T) from fun r ↦ congr($this r)

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))
⊢ CommRingCat.ofHom (algebraMap R S) ≫ preimage (Over.Hom.left f) = CommRingCat.ofHom (algebraMap R T)
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:
by

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))
⊢ ∀ (r : R), (↑↑(CommRingCat.Hom.hom (preimage (Over.Hom.left f)))).toFun ((algebraMap R S) r) = (algebraMap R T) r

Tactic:
by

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

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) =
    f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h i : c ⟶ d
η : h ⟶ i
η₁ : g ≫ h ⟶ g ≫ i
η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i
η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i
η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ≫ g) ◁ η = η₄

Tactic:
by

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))
⊢ (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

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
η₁ : f ⟶ 𝟙 a ≫ g
η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙 a ◁ η = η₂

Tactic:
by

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 ≫ g ⟶ f ≫ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
by

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

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

Goal state after: