mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
case some.right.none.term
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.term WalkingPair.right) ≫
      (match none with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.term WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f

Tactic:
cases f

Goal state after:
case some.right.some.right.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (cospan f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
case none.none.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.unop g.unop).map (WidePullbackShape.Hom.id none) ≫
      (match none with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map (WidePullbackShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (cospan f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
case some.left.none.term
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.unop g.unop).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (match none with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map (WidePullbackShape.Hom.term WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.unop g.unop).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (cospan f✝.unop g.unop).map f ≫
      (match none with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
case some.right.none.term
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.unop g.unop).map (WidePullbackShape.Hom.term WalkingPair.right) ≫
      (match none with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map (WidePullbackShape.Hom.term WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (cospan f✝.unop g.unop).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f✝.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f✝.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).leftOp).map f

Tactic:
cases f

Goal state after:
case some.right.some.right.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.unop g.unop).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((cospan f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
        | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = 𝟙_ C ◁ (λ_ X).hom

Tactic:
braiding_rightUnitor_aux₂

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (λ_ X).hom = 𝟙_ C ◁ (λ_ X).hom
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrpCat
inst✝ : Small.{w, max u w} (Quot F)
⊢ desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

Tactic:
by
  refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
  simpa only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe]
    using! Quot.ι_desc F (colimitCocone F) j x

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : C
⊢ tensorμ X X Y Y ≫ (β_ (X ⊗ Y) (X ⊗ Y)).hom = ((β_ X X).hom ⊗ₘ (β_ Y Y).hom) ≫ tensorμ X X Y Y

Tactic:
simp [tensorμ, SymmetricCategory.braiding_swap_eq_inv_braiding Y X, tensorHom_def]

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

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).fst = x⁻¹.fst

Tactic:
simp [fst_invOf, snd_invOf]

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).snd = x⁻¹.snd

Tactic:
simp [fst_invOf, snd_invOf]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ ∘ₗ comul) a = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ) (comul a) = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul =
    lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul

Tactic:
by
    ext i : 1
    simp_rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, comul_comp_lsingle,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_lsingle, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq]

Goal state after: