mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ C a'

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Sum.inr a'' ∈ f a'
⊢ C a'

Tactic:
· apply hbase
    convert! e
    exact Part.mem_unique h (fix_stop e)

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Sum.inr a'' ∈ f a'
⊢ C a'
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ▷ X

Tactic:
by
  rw [rightDistrib_hom, coprod.inl_desc]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)

Tactic:
apply of_commSq
  -- This line transforms the first goal in suitable form; the last line closes all three goals.
  on_goal 1 => rw [p.map_comp]
  apply CommSq.horiz_comp (commSq p f φ) (commSq p g ψ)

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ S = T

Tactic:
by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : a' = a
hφ' : p.IsHomLift f (eqToHom h ≫ φ)
⊢ p.IsHomLift f φ

Tactic:
by subst h; simpa using hφ'

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b b' : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : b = b'
hφ' : p.IsHomLift f (φ ≫ eqToHom h)
⊢ p.IsHomLift f φ

Tactic:
by subst h; simpa using hφ'

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : R' = R
hφ' : p.IsHomLift (eqToHom h ≫ f) φ
⊢ p.IsHomLift f φ

Tactic:
by subst h; simpa using hφ'

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S S' : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : S = S'
hφ' : p.IsHomLift (f ≫ eqToHom h) φ
⊢ p.IsHomLift f φ

Tactic:
by subst h; simpa using hφ'

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R S : 𝒮
ha : p.obj a = S
f : R ⟶ S
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
subst ha; exact IsPreFibered.exists_isCartesian' f

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
⊢ (lift s ≫ precompEnrichedHom V F₁ F₂ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k

Tactic:
have := s.w k.hom

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
k : Under j
this : s.π.app j ≫ (functorEnrichedHom V F₁ F₂).map k.hom = s.π.app k.right
⊢ (lift s ≫ precompEnrichedHom V F₁ F₂ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t)))
      ((ConcreteCategory.hom (F.map (u ≫ Pi.map' ⇑(fiberPerm h b) fun j ↦ (Iso.refl X).hom))) a)

Tactic:
rw [map_comp, FintypeCat.comp_apply, h]

Goal state after:
case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t)))
      ((ConcreteCategory.hom (F.map (Pi.map' ⇑(fiberPerm h b) fun j ↦ (Iso.refl X).hom))) (mkSelfProdFib F X))
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
⊢ IsIso f

Tactic:
rw [← isUnit_iff_isIso]
  exact FibreFunctor.end_isUnit F f

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X)))
      ((ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (t.hom.app A)) a)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)

Tactic:
ht

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((ConcreteCategory.hom (F.map f)) a) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case htc
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (i : PointedGaloisObject F), IsClosed (cl i)

pp: case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (u : Finset (PointedGaloisObject F)), (Set.univ ∩ ⋂ i ∈ u, cl i).Nonempty

Tactic:
· intro X
      apply IsClosed.leftCoset
      exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)

Goal state after:
case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (u : Finset (PointedGaloisObject F)), (Set.univ ∩ ⋂ i ∈ u, cl i).Nonempty
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C ⋆ D
f : x.Hom y
⊢ comp f y.id = f

Tactic:
by
    cases x <;> cases y <;> simp only [Hom, id, comp, Category.comp_id] <;> tauto

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
⊢ IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J

Tactic:
by
  wlog hJ : IsConnected J generalizing J
  · refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ U V f ↦ ?_⟩
    have hα (i j) (f : i ⟶ j) : α.app i ≫ c.map f = α.app j := by simp [← NatTrans.naturality]
    have hc' := WithTerminal.isLimitEquiv.symm hc
    have inst : IsConnected (WithTerminal J) := isConnected_of_hasTerminal _
    exact (this (J := WithTerminal J) inst).1 G ⟨⟨WithTerminal.liftToTerminal c Over.mkIdTerminal,
      { app i := i.casesOn α.app (Over.mkIdTerminal.from _) }, isLimitOfReflects (Over.forget _) (by
      refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (WithTerminal.isLimitEquiv.symm hc)
      · exact NatIso.ofComponents (fun i ↦ i.casesOn (fun _ ↦ .refl _) (.refl _)) <| by
          rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp
      · exact Cone.ext (.refl _) (by rintro ⟨⟩ <;> simp))⟩, fun i ↦
        i.casesOn H (.of_isIso (𝟙 F))⟩ f
  refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ i j f ↦ ⟨⟨by simp⟩, ⟨Limits.PullbackCone.isLimitAux' _ fun s ↦ ?_⟩⟩⟩
  let hcᵢ := isLimitOfPreserves (Over.forget _ ⋙ (evaluation _ _).obj i) hc
  let hcⱼ := isLimitOfPreserves (Over.forget _ ⋙ (evaluation _ _).obj j) hc
  let l : s.pt ⟶ G.left.obj i := hcᵢ.lift ⟨_, fun k ↦ (H k f).lift (s.fst ≫ (α.app k).left.app j)
    s.snd (by simp [← s.condition, ← NatTrans.comp_app]), fun k₁ k₂ fk₁k₂ ↦ (H _ f).hom_ext
    (by simp [← NatTrans.naturality, ← NatTrans.comp_app, ← Over.comp_left])
    (by simp [← NatTrans.comp_app])⟩
  refine ⟨l, hcⱼ.hom_ext fun k ↦ ?_, ?_, fun {m} hm₁ hm₂ ↦ hcᵢ.hom_ext
    fun k ↦ ((H k f).hom_ext ?_ ?_).trans (hcᵢ.fac ⟨_, _⟩ k).symm⟩
  · simpa [Category.assoc, NatTrans.naturality] using (hcᵢ.fac_assoc _ _ _).trans (by simp)
  · dsimp
    obtain ⟨k⟩ : Nonempty J := inferInstance
    rw [show G.hom.app i = (α.app k).left.app i ≫ (c.obj k).hom.app i by simp [← comp_app]]
    exact (hcᵢ.fac_assoc ..).trans (by simp)
  · dsimp at *
    simp [← NatTrans.naturality, reassoc_of% hm₁]
  · simpa [← NatTrans.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ False

Tactic:
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
      rw [Cardinal.two_le_iff]
      exact ⟨_, _, r_ne_s⟩

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi (functorMap f n)

Tactic:
functorMap,

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun m ↦ if h : m < n then eqToHom ⋯ else if h' : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y : C
⊢ ((braidingNatIso L W ε).hom.app (L'.obj X)).app (L'.obj Y) =
    LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X

Tactic:
simp [braidingNatIso, lift₂NatIso]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y : C
⊢ ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                  (tensorBifunctor L W ε)).hom.app
            X).app
        Y ≫
      L'.map (β_ X Y).hom ≫
        ((Lifting₂.iso L' L' W W ((curriedTensor C).flip ⋙ (whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε).flip).inv.app
              X).app
          Y =
    LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
⊢ ∀ {X : C} {Y Y' : Over I} (f : (toOver I).obj X ⟶ Y) (g : Y ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
intro A X' X u g

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (u ≫ g) =
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } u ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft) ▷ Q.X

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ (R.X ⊗ R.X) P.X Q.X).inv

Tactic:
comp_whiskerRight,

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft ≫ P.actLeft) ▷ Q.X

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ (R.X ⊗ R.X) P.X Q.X).inv
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
⊢ (∀ (T : C), Function.Bijective fun x ↦ x ≫ leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m, m • x = y

Tactic:
congr! with Z

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (Function.Bijective fun x ↦ x ≫ leftSMul M X) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalLeftAction C D
M' N' O' : D
A : C
inst✝⁴ : MonObj A
M N O : D
inst✝³ : ModObj A M
inst✝² : ModObj A N
inst✝¹ : ModObj A O
f : M ≅ N
inst✝ : IsModHom A f.hom
⊢ γ ≫ f.inv = A ⊴ₗ f.inv ≫ γ

Tactic:
by simp [Iso.comp_inv_eq]

Goal state after: