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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))

Tactic:
congr

Goal state after:
case e_6.e_8.e_7
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)
⊢ eqToHom ⋯ ≍ 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
by
  conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
  rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (e.toRingHom.comp f)

case refine_2
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (f.comp e.toRingHom)
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ Small.{u, max (u + 1) (v + 1)} (Skeleton (FGAlgCat R)) ∧ LocallySmall.{u, max u v, max (u + 1) (v + 1)} (FGAlgCat R)

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
⊢ Small.{u, max (u + 1) (v + 1)} (Skeleton (FGAlgCat R))

case refine_2
R : Type u
inst✝ : CommRing R
⊢ LocallySmall.{u, max u v, max (u + 1) (v + 1)} (FGAlgCat R)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } =
    { pt := s.1,
            π :=
              Discrete.natTrans fun x ↦
                match x with
                | { as := i } => s.π.app { as := i.succ } }.π.app
      { as := j }

Tactic:
dsimp only [Discrete.natTrans_app]

Goal state after:
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } = s.π.app { as := j.succ }
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m =
    { pt := s.1, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }.ι.app { as := j }

Tactic:
dsimp only [Discrete.natTrans_app]

Goal state after:
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = s.ι.app { as := j.succ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (snd f' g') i₂

Tactic:
· simp only [Category.assoc, lift_snd, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ P.op.IsClosedUnderLimitsOfShape J

Tactic:
by
  rwa [← isClosedUnderColimitsOfShape_op_iff_op]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ M.X ◁ isTerminalTensorUnit.from N.X =
    M.X ◁ ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N).hom

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ isTerminalTensorUnit.from M.X ▷ N.X =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M).hom ▷ N.X

Tactic:
congr

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g ≫ (λ_ Y).hom = g

Tactic:
rw [← Iso.eq_comp_inv]
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g ≫ (ρ_ Y).hom = f

Tactic:
rw [← Iso.eq_comp_inv]
  cat_disch

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }

Tactic:
congr

Goal state after:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
⊢ e₁ = e₂
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ { toBraidedCategory := toBraidedCategory✝¹, symmetry := symmetry✝¹ } =
    { toBraidedCategory := toBraidedCategory✝, symmetry := symmetry✝ }

Tactic:
congr

Goal state after:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ toBraidedCategory✝¹ = toBraidedCategory✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
x✝ : C
⊢ IsIso ((prodComparisonBifunctorNatTrans F).app x✝)

Tactic:
by dsimp; apply NatIso.isIso_of_isIso_app

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid C
inst✝³ : Algebra R A
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
⊢ f * g = g * f

Tactic:
ext x; rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ (εIso F).symm.inv = (preservesTerminalIso F).inv

Tactic:
congr

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ (εIso F).symm = preservesTerminalIso F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.inv = (prodComparisonIso F X Y).inv

Tactic:
congr

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm = prodComparisonIso F X Y
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ ↔ lift g f ≫ μ = h

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ → lift g f ≫ μ = h

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift g f ≫ μ = h → f = lift (g ≫ ι) h ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ ↔ lift f h ≫ μ = g

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ → lift f h ≫ μ = g

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f h ≫ μ = g → f = lift g (h ≫ ι) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ lift (μ ≫ ι) μ ≫ μ = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ

Tactic:
nth_rw 2 [← Category.comp_id μ]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ lift (μ ≫ ι) (μ ≫ 𝟙 A) ≫ μ = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f = lift (lift f (f ≫ ι)) f

Tactic:
apply (isPullback B).hom_ext <;> apply CartesianMonoidalCategory.hom_ext <;>
    simp [lift_inv_comp_right, lift_inv_comp_left]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ ↑(Fintype.card ↥s)
⊢ False

Tactic:
exact natCast_lt_aleph0.not_ge this

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : max (lift.{v, u} ℵ₀) (lift.{v, u} #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
lift_aleph0,

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : max ℵ₀ (lift.{v, u} #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x : M₁
⊢ ∀ (y : M₁), (B x) y = 0 → (B y) x = 0

Tactic:
y

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
⊢ (B x) y = 0 → (B y) x = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x : M
⊢ ∀ (y : M), (B (f x)) (f y) = (B x) y

Tactic:
y

Goal state after:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
⊢ (B (f x)) (f y) = (B x) y
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
⊢ (B (v i)) (vi j • v j) = 0

Tactic:
map_smulₛₗ

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
⊢ I' (vi j) • (B (v i)) (v j) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
hij : i ≠ j
⊢ (B (v i)) (v j) = 0

Tactic:
exact h hij

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ v.repr.symm vi = 0

Tactic:
LinearEquiv.map_eq_zero_iff

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ vi = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
⊢ PreservesLimit K G

Tactic:
let i : I ⟶ P := equalizer.ι s t

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ PreservesLimit K G