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

Goal state before:
pp: 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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id none) ≫
      (match none with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp).map (WidePushoutShape.Hom.id none)

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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

Goal state before:
pp: 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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp).map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

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

Goal state before:
pp: 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 ⟶ Z
g : Y ⟶ Z
⊢ (span f.unop g.unop).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f.unop g.unop).obj none)
        | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp).map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

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

Goal state before:
pp: 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.op g.op).map (WidePullbackShape.Hom.id none) ≫
      (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 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 ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id none)

Tactic:
cat_disch

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

Goal state before:
pp: 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.op g.op).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (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.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.term WalkingPair.left)

Tactic:
cat_disch

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

Goal state before:
pp: 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))

Tactic:
cat_disch

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

Goal state before:
pp: 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)

Tactic:
cat_disch

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

Goal state before:
pp: 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))

Tactic:
cat_disch

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

Goal state before:
pp: 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)

Tactic:
cat_disch

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

Goal state before:
pp: 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)

Tactic:
cat_disch

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

Goal state before:
pp: 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))

Tactic:
cat_disch

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

Goal state before:
pp: 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)

Tactic:
cat_disch

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

Goal state before:
pp: 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))

Tactic:
cat_disch

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

Goal state before:
pp: 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
inst✝ : HasPushout f g
⊢ HasPullback f.op g.op

Tactic:
rwa [hasPullback_op_iff_hasPushout]

Goal state after:
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₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)

Tactic:
by rw [whisker_exchange, braiding_tensor_left_hom]; monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
⊢ Function.LeftInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
⊢ Function.RightInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (Adjunction.id.comp adj)) L.leftUnitor.hom = R.rightUnitor.inv

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (adj.comp Adjunction.id)) L.rightUnitor.hom = R.leftUnitor.inv

Tactic:
cat_disch

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

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : ↑X
⊢ s • (ConcreteCategory.hom g) (r • x) = (RingHom.id R) r • s • (ConcreteCategory.hom g) x

Tactic:
RingHom.id_apply,

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : ↑X
⊢ s • (ConcreteCategory.hom g) (r • x) = r • s • (ConcreteCategory.hom g) x
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y

Tactic:
convert!
      congr((TensorProduct.rid S _).symm
        (TensorProduct.rid _ _ $(lTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.rid _ _ $(lTensor_counit_comul (R := R) y)))

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) ((LinearMap.lTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (comul y)))

case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) (x ⊗ₜ[S] 1) ⊗ₜ[R] (TensorProduct.rid R B) (y ⊗ₜ[R] 1))
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * (1 + a) = 0

Tactic:
rw [mul_add, mul_one, mul_self, add_self]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A✝ B✝ : Comon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ { hom := inv f.hom, isComonHom_hom := ⋯ } = 𝟙 A✝ ∧ { hom := inv f.hom, isComonHom_hom := ⋯ } ≫ f = 𝟙 B✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M✝ N✝ O : C
inst✝² : ComonObj M✝
inst✝¹ : ComonObj N✝
inst✝ : ComonObj O
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.hom, isComonHom_hom := this } ≫ { hom := f.inv, isComonHom_hom := ⋯ } = 𝟙 M

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M✝ N✝ O : C
inst✝² : ComonObj M✝
inst✝¹ : ComonObj N✝
inst✝ : ComonObj O
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.inv, isComonHom_hom := ⋯ } ≫ { hom := f.hom, isComonHom_hom := this } = 𝟙 N

Tactic:
cat_disch

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

Goal state before:
pp: x✝¹ : Type u
x✝ : CommRingCat
⊢ Function.RightInverse (fun f ↦ ofHom (homEquiv.symm ⇑(ConcreteCategory.hom f))) fun f ↦ ↾homEquiv (Hom.hom f)

Tactic:
cat_disch

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

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
      {
            app := fun S ↦
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯,
            naturality := ⋯ }.app
        (R.monoidAlgebra.obj G) =
    𝟙 (R.monoidAlgebra.obj G)

Tactic:
ext : 2
    apply MonoidAlgebra.ringHom_ext <;> intro <;> simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ ∏ᶠ (p : R), p ^ count p (normalizedFactors x) ~ᵤ x

Tactic:
rw [← Multiset.prod_map_eq_finprod, Multiset.map_id']
  exact prod_normalizedFactors hx

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Function.Injective ⇑(map S Q f r) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
injective_iff_map_eq_zero

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0