mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: case snd
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).2 = (↑((ConcreteCategory.hom g).toFun y)).2

Tactic:
exact congr($h₂ y)

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

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (λ_ (𝟙_ V)).inv ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
unitors_inv_equal,

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (ρ_ (𝟙_ V)).inv ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
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 : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ

Tactic:
by
  subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

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 : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
⊢ p.IsHomLift f φ

Tactic:
by
  subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (∏ᶜ X).obj
i : ι
⊢ (productEquiv X) x i = (ConcreteCategory.hom (Pi.π X i)) x

Tactic:
simpa [productEquiv, equivEquivIso, equivIsoIso, Iso.toEquiv] using!
    piComparison_comp_π_apply FintypeCat.incl X i x

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

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Type u_1
inst✝ : ∀ (j : J), Finite (K.obj j)
⊢ Fintype (colimit K)

Tactic:
have : Finite (colimit K) := finite_of_isColimit (colimit.isColimit K)

Goal state after:
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Type u_1
inst✝ : ∀ (j : J), Finite (K.obj j)
this : Finite (colimit K)
⊢ Fintype (colimit K)
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) = β.app X₂

Tactic:
eq₂,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ η.app (L₁.obj (F.obj X₂)) ≫ F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) = β.app X₂
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ ↑y ∈ Set.range ⇑(ConcreteCategory.hom f.hom)

Tactic:
use (X.ρ g⁻¹).hom x

Goal state after:
case h
G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom (X.ρ g⁻¹).hom) x) = ↑y
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
⊢ (g * h) • a = g • h • a

Tactic:
change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (h.hom ≫ g.hom))) a = (ConcreteCategory.hom (F.map h.hom ≫ F.map g.hom)) a
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

pp: case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ¬∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
· obtain ⟨Y, v, hni, hvmono, hvnoiso⟩ :=
      has_non_trivial_subobject_of_not_isConnected_of_not_initial X h nhi
    obtain ⟨Z, u, ⟨c⟩⟩ := PreGaloisCategory.monoInducesIsoOnDirectSummand v
    let t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
    have hn1 : Nat.card (F.obj Y) < n := by
      rw [hn]
      exact lt_card_fiber_of_mono_of_notIso F v hvnoiso
    have i : X ≅ Y ⨿ Z := (colimit.isoColimitCocone t).symm
    have hnn : Nat.card (F.obj X) = Nat.card (F.obj Y) + Nat.card (F.obj Z) := by
      rw [card_fiber_eq_of_iso F i]
      exact card_fiber_coprod_eq_sum F Y Z
    have hn2 : Nat.card (F.obj Z) < n := by
      rw [hn, hnn, lt_add_iff_pos_left]
      exact Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)
    let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl
    let ⟨ι₂, f₂, g₂, hc₂, hf₂, he₂⟩ := hi (Nat.card (F.obj Z)) hn2 Z rfl
    refine ⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩
    use Cofan.combPairIsColimit hc₁ hc₂ c
    refine ⟨fun i ↦ ?_, inferInstance⟩
    cases i
    · exact hf₁ _
    · exact hf₂ _

Goal state after:
case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ¬∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: 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 := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
hne : c.Nonempty
⊢ ∃ a, (toAut F G) a = t

Tactic:
obtain ⟨g, hg⟩ := hne

Goal state after:
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 := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
hg : g ∈ c
⊢ ∃ a, (toAut F G) a = t
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i j k : X.I
hij : i = j
hjk : j = k
⊢ X.objIsoOfEq hij ≪≫ X.objIsoOfEq hjk = X.objIsoOfEq ⋯

Tactic:
subst hij hjk
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ = h.p₃

Tactic:
simp [p₂₃, hp₃]

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

Goal state before:
pp: case refine_1
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m

Tactic:
split_ifs

Goal state after:
case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : m < n + 1
⊢ M m = M m

case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = M m

Tactic:
split_ifs

Goal state after:
case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = if x : m < n then M m else N m

Tactic:
split_ifs

Goal state after:
case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m

Tactic:
split_ifs

Goal state after:
case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
split_ifs

Goal state after:
case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
h✝ : k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
h✝ : ¬k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫
      (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }

Tactic:
split_ifs

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫
      (if h : m < n then eqToHom ⋯ else eqToHom ⋯ ≫ f m ≫ eqToHom ⋯) ≫ eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
x✝¹ x✝ : (j : J) × (F.obj (op j)).obj j
⊢ Types.coendRel F x✝¹ x✝ →
    (match x✝¹ with
      | ⟨j, y⟩ => Quot.mk (Types.coendRel G) ⟨j, (hom ((f.app (op j)).app j)) y⟩) =
      match x✝ with
      | ⟨j, y⟩ => Quot.mk (Types.coendRel G) ⟨j, (hom ((f.app (op j)).app j)) y⟩

Tactic:
by
        rintro ⟨g, y⟩
        apply Quot.sound
        rw [Types.coendRel_iff]
        refine ⟨g, (f.app _).app _ y, ?_, ?_⟩
        · simp only [← NatTrans.comp_app_apply, f.naturality]
        · simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝¹ : Φ.functor.Full
inst✝ : Φ.functor.Faithful
X₁ : C₁
⊢ W₁ ((ι i).app X₁)

Tactic:
simpa [hW₁] using hi (Φ.functor.obj X₁)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ Y✝ : (i : J₁) → C₂ (e i)
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi (fun j ↦ W₂ (e j)) f
⊢ (MorphismProperty.pi W₂).isoClosure.inverseImage E.functor f

Tactic:
refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ Y✝ : (i : J₁) → C₂ (e i)
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi (fun j ↦ W₂ (e j)) f
i : J₂
⊢ W₂ i (E.functor.map f i)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (f✝.tensor g✝) = projectMapAux f✝¹ (f'✝.tensor g'✝)

Tactic:
dsimp only [projectMapAux]; rw [hfg, hfg']

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ adj.toMonad.Algebra ⥤ D

Tactic:
refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_
  · apply comparisonLeftAdjointHomEquiv
  · intro A B B' g h
    ext1
    simp [Cofork.IsColimit.homIso, Adjunction.homEquiv_unit]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f = (unitCofork A).π

Tactic:
dsimp only [beckCofork_π, unitCofork_π]

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ A.a ≫ ((comparisonAdjunction adj).unit.app A).f = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))