mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ e ^ 1 * (x * e ^ n) = e ^ (n + 1) * x

pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ e ^ (n + 1) * x = e ^ 1 * x

Tactic:
· ring

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ e ^ (n + 1) * x = e ^ 1 * x
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
m : Ideal R
inst✝ : m.IsMaximal
⊢ jacobson R ≤ m

Tactic:
Ring.jacobson_eq_sInf_isMaximal

Goal state after:
R : Type u_1
inst✝¹ : Ring R
m : Ideal R
inst✝ : m.IsMaximal
⊢ sInf {I | I.IsMaximal} ≤ m
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * (-(1 - i) + 1) ∈ M

Tactic:
neg_sub,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * (i - 1 + 1) ∈ M
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f (a ^ (0 + n) * c) = f (a ^ (0 + (n + m)) * b ^ m) * s

Tactic:
simp [e, pow_add]; ring

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ↑((Units.map ↑f) ⋯.unit) = ↑a

Tactic:
exact hb

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
rw [selfZPow_of_nonneg x B hd.le, selfZPow_of_nonpos, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec'_mk, map_one]

Goal state after:
case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
    m ≫ (PullbackCone.mk h k ⋯).fst = s.fst →
      m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
intro m h₁ h₂

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk h k ⋯).snd = s.snd
⊢ m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
intro m h₁ h₂

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))

Tactic:
change fst = e₁.hom ≫ fst' ≫ e₂.inv
              rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
⊢ ∀ {m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt},
    m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst →
      m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd → m = prod.lift s.fst (s.snd ≫ prod.snd)

Tactic:
intro m h₁ h₂

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt
h₁ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
intro m h₁ h₂

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1

Tactic:
simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ (↑a.2 * (a.1 * (↑s * ↑p.2))) • p'.1 = (↑s * (↑a.2 * ↑p.2 * a.1)) • p'.1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i - 1)).IsSupported s

Tactic:
Int.cast_sub,

Goal state after:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i) - ↑1).IsSupported s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
| mk 0 ((IsLocalization.sec S x).2 * 1)

Tactic:
zero_mk

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
| 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ mk 0 (1 * s) = 0

Tactic:
zero_mk

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit K

Tactic:
rw [hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]
  exact hasColimit_comp_equivalence (K ⋙ E) E.inv

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.e_6
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ mk m 1 = mk (↑s • m) s

Tactic:
rw [LocalizedModule.mk_eq]

Goal state after:
case h.e_6
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ ∃ u, u • s • m = u • 1 • ↑s • m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
r : R'
⊢ e.toFun ((algebraMap R' (R' ⊗[R] S)) r) = (algebraMap R' S') r

Tactic:
by simp [Iso.commRingCatIsoToRingEquiv, h2, e, h3]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)

Tactic:
delta mk'
  rw [← map_add, LocalizedModule.mk_add_mk]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (hc.lift inv_r ≫ c.π.app j)) (FreeCommRing.of PUnit.unit) = inv j

Tactic:
IsLimit.fac

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op zero))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

Tactic:
refine ⟨op zero, 𝟙 _, op left, inferInstance, ?_⟩
    simp only [CategoryTheory.Functor.map_id, hom_id, limit.cone_x, limit.cone_π,
      RingHom.id_apply]
    exact (limit.w_apply F (op left) x).symm

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv

Tactic:
rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h,
      hom_inv_id, comp_id]

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) =
    ((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
      inv (F.map f ◁ F.mapComp g h)

Tactic:
IsIso.eq_comp_inv

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
    (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
rwa [isoClosure_le_iff]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure ≤ P

Tactic:
rwa [isoClosure_le_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    colimit.ι (Grothendieck.ι F X ⋙ G) d

Tactic:
conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    eqToHom ⋯ ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: case e_a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ f = (Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber

Tactic:
apply Grothendieck.ext

Goal state after:
case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ f.fiber = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).fiber

case e_a.w_base
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ f.base = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber } =
    𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }

Tactic:
apply Grothendieck.ext

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ eqToHom ⋯ ≫ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.fiber =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).fiber

case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.base =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).base
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber } =
    { base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫ { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }

Tactic:
apply Grothendieck.ext

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.fiber =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).fiber

case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber }.base =
    ({ base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫
        { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }).base
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂

Tactic:
intro Z₁

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ : C
⊢ ∀ (X₂ : C) (k₁ : X ⟶ F.obj Z₁) (k₂ : X ⟶ F.obj X₂) (f_1 : Z₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂