mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : none ⟶ some WalkingPair.left),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case none.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : none ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫ ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : none ⟶ some WalkingPair.right),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case none.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : none ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫ ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.left ⟶ none),
    ((span f g).map f_1 ≫ Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.left.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.left ⟶ none
⊢ ((span f✝ g).map f ≫ Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.left ⟶ some WalkingPair.left),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.left ⟶ some WalkingPair.right),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.right ⟶ none),
    ((span f g).map f_1 ≫ Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.right.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.right ⟶ none
⊢ ((span f✝ g).map f ≫ Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.right ⟶ some WalkingPair.left),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.left) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.left) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : some WalkingPair.right ⟶ some WalkingPair.right),
    ((span f g).map f_1 ≫ Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn (some WalkingPair.right) (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ ((span f✝ g).map f ≫ Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn (some WalkingPair.right) (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
      ((Functor.const WalkingSpan).obj W).map f
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Over X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Over (F.obj X)
A' : T
e : F.obj A' ≅ B.left
⊢ (post F).essImage B

Tactic:
obtain ⟨f, hf⟩ := F.map_surjective (e.hom ≫ B.hom)

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Over (F.obj X)
A' : T
e : F.obj A' ≅ B.left
f : A' ⟶ X
hf : F.map f = e.hom ≫ B.hom
⊢ (post F).essImage B
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Under X
⊢ Hom.right (mkIdInitial.to Y) = Y.hom

Tactic:
mkIdInitial.hom_ext (mkIdInitial.to Y) (homMk Y.hom)

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Under X
⊢ Hom.right (homMk Y.hom ⋯) = Y.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default

Tactic:
intro f

Goal state after:
case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
⊢ f = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default

Tactic:
intro f

Goal state after:
case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
⊢ f = default
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
by cases f; cases g; simpa using! h

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
A✝ B✝ : SemimoduleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (SemimoduleCat R) AddCommMonCat).map f)
⊢ IsIso f

Tactic:
have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommMonCat).map f))
      infer_instance
    apply isIso_of_reflects_iso _ (forget _)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ 0 ≫ f = 0

Tactic:
by
    change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
    rw [Category.assoc]
    congr
    apply hO.eq_of_src

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
x✝ : f ≫ g = f ≫ h
⊢ 0 = h

Tactic:
zero_of_source_iso_zero h i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
x✝ : f ≫ g = f ≫ h
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map (0 ≫ 0)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((colimit.isColimit F).desc c)
⊢ IsColimit c

Tactic:
apply IsColimit.ofPointIso (colimit.isColimit F)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))

Tactic:
by
              apply fun s m => (Cocone.functoriality K F).map_injective _
              intro s m
              rw [Functor.map_preimage]
              apply t.uniq_cocone_morphism

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
⊢ (ι f ≫ p) ≫ f' = 0

Tactic:
by simp [← w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)

Tactic:
by
  classical
    ext
    simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ cokernelZeroIsoTarget.hom = cokernel.desc 0 (𝟙 Y) ⋯

Tactic:
ext; simp [cokernelZeroIsoTarget]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : f ≫ cokernel.π f = 0
| f ≫ cokernel.π f = 0

Tactic:
lhs

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : f ≫ cokernel.π f = 0
| f ≫ cokernel.π f
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ image.ι f ≫ cokernel.π f = 0

Tactic:
by
        have w := cokernel.condition f
        conv at w =>
          lhs
          congr
          rw [← image.fac f]
        rw [← HasZeroMorphisms.comp_zero (Limits.factorThruImage f), Category.assoc,
          cancel_epi] at w
        exact w

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| f ≫ cokernel.π (image.ι f) = 0

Tactic:
lhs

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| f ≫ cokernel.π (image.ι f)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).hom = prod.lift fst snd

Tactic:
by
      ext <;> simp [biprod.isoProd]

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
⊢ matrix m ≫ π g k = desc fun j ↦ m j k

Tactic:
by
  ext
  simp [biproduct.matrix]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
by cases f; cases g; simpa using! h

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ Pi.Lex (fun x1 x2 ↦ x1 < x2) s (cons x₀ x) (cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i ↦ s) x y

Tactic:
Pi.Lex,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (∃ i, (∀ (j : Fin n.succ), j < i → cons x₀ x j = cons y₀ y j) ∧ s (cons x₀ x i) (cons y₀ y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
⊢ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)

Tactic:
intro f

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) → f ∈ s.finsuppAntidiag (e n)
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)

Tactic:
lhs

Goal state after:
u : ℤˣ
n : ℕ
| u ^ n
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
⊢ l.formPerm = l'.formPerm

Tactic:
obtain ⟨n, rfl⟩ := h
  exact (formPerm_rotate l hd n).symm

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
intro f

Goal state after:
case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
⊢ f ∈ permsOfList l → f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l → False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight 1)) b) (f x) = y) ↔ f.SameCycle x y

Tactic:
simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Tactic:
have h₀ := Int.natCast_pos.mpr (orderOf_pos f)

Goal state after:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case zero
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ 1 x = (f ^ 0) x

Tactic:
pow_zero

Goal state after:
case zero
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ 1 x = 1 x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb

Goal state after:
case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
a✝ : List β
b✝ : List α
hs : ∀ (x : α), x ∈ ⟦b✝⟧
ht : ∀ (x : β), x ∈ ⟦a✝⟧
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
change signAux2 _ _ = signAux2 _ _

Goal state after:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
a✝ : List β
b✝ : List α
hs : ∀ (x : α), x ∈ ⟦b✝⟧
ht : ∀ (x : β), x ∈ ⟦a✝⟧
⊢ signAux2 a✝ ((e.symm.trans f).trans e) = signAux2 b✝ f
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ sign (swap x y) = a

Tactic:
by rw [sign_swap hxy, h]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
⊢ (noncommPiCoprod ϕ hcomm).ker ≤ ⊥

Tactic:
intro f

Goal state after:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
⊢ f ∈ (noncommPiCoprod ϕ hcomm).ker → f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
hy : f.SameCycle x y
⊢ ¬f y = y ↔ True

Tactic:
rcases hy with ⟨k, rfl⟩

Goal state after:
case pos
α : Type u_2
f : Perm α
x : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
k : ℤ
⊢ ¬f ((f ^ k) x) = (f ^ k) x ↔ True