mathlib-initiative/mathlib-tactics huggingface dataset:
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
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'
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∈ Ideal.comap φ P''
⊢ e' 0 ∈ P''

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
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'
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∈ Ideal.comap φ P''
h₁ : e' (Fin.last (n + 1)) ∈ P''
h₂ : ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
h : e' (Fin.castSucc 0) ∉ P''
⊢ e' (Fin.castSucc 0) ∈ P''

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
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'
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∈ Ideal.comap φ P''
h₁ : e' (Fin.last (n + 1)) ∈ P''
h₂ : ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
⊢ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Fin.cons (↑P'φ) Q' i.succ

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 ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
a b : B
f : a ⟶ b
⊢ 𝟙 (obj a) ≫ map f = map (𝟙 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 ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ map (𝟙 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 : StrictlyUnitaryLaxFunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.mapComp f g ▷ S.map h ≫ S.mapComp (f ≫ g) h ≫ S.map₂ (α_ f g h).hom =
    (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ S.mapComp g h ≫ S.mapComp f (g ≫ h)

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 : StrictlyUnitaryLaxFunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).inv = (λ_ (S.map f)).inv ≫ eqToHom ⋯ ▷ S.map f ≫ S.mapComp (𝟙 a✝) 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
S : StrictlyUnitaryLaxFunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (ρ_ f).inv = (ρ_ (S.map f)).inv ≫ S.map f ◁ eqToHom ⋯ ≫ S.mapComp f (𝟙 b✝)

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
a b : B
f : a ⟶ b
⊢ map (𝟙 a ≫ 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
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ IsIso (F.mapId 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 : StrictlyUnitaryLaxFunctor B C
x : B
⊢ F.mapId x ≫ eqToHom ⋯ = 𝟙 (𝟙 (F.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 : StrictlyUnitaryLaxFunctor B C
x : B
⊢ eqToHom ⋯ ≫ F.mapId x = 𝟙 (F.map (𝟙 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 : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
x✝ : B
⊢ (F.comp G.toLaxFunctor).map (𝟙 x✝) = 𝟙 ((F.comp G.toLaxFunctor).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 : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
x✝ : B
⊢ (F.comp G.toLaxFunctor).mapId x✝ = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map (f ≫ 𝟙 b) = map f ≫ 𝟙 (obj b)

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map ((f ≫ g) ≫ h) = (map f ≫ map g) ≫ map h

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map f ≫ map g ≫ map h = map (f ≫ g ≫ h)

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (eqToIso ⋯).hom ≫ S.map f ◁ S.map₂ η ≫ (eqToIso ⋯).inv

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).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
F : StrictlyUnitaryLaxFunctor B C
⊢ F.comp (id C) = F

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (eqToIso ⋯).hom ≫
      (eqToIso ⋯).hom ▷ S.map h ≫ (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (eqToIso ⋯).inv ≫ (eqToIso ⋯).inv

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom ▷ S.map f ≫ (λ_ (S.map f)).hom

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (ρ_ f).hom = (eqToIso ⋯).hom ≫ S.map f ◁ (eqToIso ⋯).hom ≫ (ρ_ (S.map f)).hom

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝ : a✝ ⟶ b✝
⊢ ∀ (g : b✝ ⟶ c✝),
    (F.comp G.toStrictlyUnitaryPseudofunctor).map (x✝ ≫ g) =
      (F.comp G.toStrictlyUnitaryPseudofunctor).map x✝ ≫ (F.comp G.toStrictlyUnitaryPseudofunctor).map g

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝ : a✝ ⟶ b✝
⊢ ∀ (g : b✝ ⟶ c✝),
    (F.comp G.toStrictlyUnitaryPseudofunctor).map (x✝ ≫ g) =
      (F.comp G.toStrictlyUnitaryPseudofunctor).map x✝ ≫ (F.comp G.toStrictlyUnitaryPseudofunctor).map g

Tactic:
by simp [StrictPseudofunctor.map_comp]

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

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

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (eqToIso ⋯).hom ≫ S.map f ◁ S.map₂ η ≫ (eqToIso ⋯).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
F : StrictlyUnitaryLaxFunctor B C
⊢ (id B).comp F = F

Tactic:
by

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).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''
⊢ ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
⊢ PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (algΓ R)

Tactic:
by

Goal state after: