mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
rw [← det_transpose, det_succ_row _ j]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
by
  simp only [det_succ_row_zero, submatrix_apply, Fin.succ_zero_eq_one, submatrix_submatrix,
    det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, Fin.sum_univ_succ,
    Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,
    Fin.succ_succAbove_zero, sum_singleton, Fin.succ_succAbove_one]
  ring

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

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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
⊢ IsLimit d

Tactic:
let i : F.mapCone d' ≅ F.mapCone d :=
          (h (F.mapCone d) hd).toLiftableCone.validLift

Goal state after:
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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
⊢ IsLimit d
Module: Mathlib.CategoryTheory.Limits.Creates

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
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : (Cocone.whiskeringEquivalence e).inverse.obj (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  (Cocone.whiskeringEquivalence e).inverse.obj (Cocone.whisker e.functor c) :=
  (Cocone.whiskeringEquivalence e).inverse.mapIso (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCocone ((Cocone.whiskeringEquivalence e).inverse.obj (liftColimit (hc.whiskerEquivalence e))) ≅ c

Tactic:
refine ?_ ≪≫ inner ≪≫ ((Cocone.whiskeringEquivalence e).unitIso.app c).symm

Goal state after:
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
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : (Cocone.whiskeringEquivalence e).inverse.obj (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  (Cocone.whiskeringEquivalence e).inverse.obj (Cocone.whisker e.functor c) :=
  (Cocone.whiskeringEquivalence e).inverse.mapIso (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCocone ((Cocone.whiskeringEquivalence e).inverse.obj (liftColimit (hc.whiskerEquivalence e))) ≅
    (Cocone.whiskeringEquivalence e).inverse.obj (F.mapCocone (liftColimit (hc.whiskerEquivalence e)))
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ G.whiskerLeft (limit.π F j) =
    limit.π (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
ext d

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
d : D
⊢ ((limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ G.whiskerLeft (limit.π F j)).app d =
    (limit.π (F ⋙ (whiskeringLeft D K C).obj G) j).app d
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom =
    G.whiskerLeft (colimit.ι F j)

Tactic:
ext d

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
d : D
⊢ (colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom).app d =
    (G.whiskerLeft (colimit.ι F j)).app d
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ ∃ X' Y' eX eY f', f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Linear R C
inst✝¹ : Linear R D
F : C ⥤ D
e : C ≌ D
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.inverse.map (f • r) = f • e.inverse.map r

Tactic:
by
    apply e.functor.map_injective
    simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
    μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
← associativity_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ F.map (α_ X Y Z).inv = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv

Tactic:
← associativity_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ F.map (α_ X Y Z).inv
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ μ G (F.obj x✝¹) (F.obj x✝) ≫
        μ G (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝) ≫ G.map (F.obj x✝² ◁ μ F x✝¹ x✝) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
← associativity_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom ≫ G.map (F.obj x✝² ◁ μ F x✝¹ x✝) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z =
    F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv

Tactic:
← associativity_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z =
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : epimorphisms C f
hg : epimorphisms C g
⊢ epimorphisms C (f ≫ g)

Tactic:
epimorphisms.iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case δ
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
· simp [homEquiv_counit, homEquiv_unit, ← δ_natural_assoc]

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom (s.ι.app j))

Tactic:
← hm

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom ((colimitCocone F).ι.app j ≫ m))
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₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app d = ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
    exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d)

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₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₃) β = (conjugateEquiv adj₁ adj₃) (β ≫ α)

Tactic:
ext d

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
⊢ ((conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₃) β).app d = ((conjugateEquiv adj₁ adj₃) (β ≫ α)).app d
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

Tactic:
ext d

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
d : D
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans.app d =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α).app d
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
⊢ counit ∘ₗ Finsupp.lcoeFun = counit

Tactic:
apply LinearMap.ext fun x ↦ ?_
  rw [← Finsupp.univ_sum_single x]
  simp [-Finsupp.univ_sum_single, Finsupp.lcoeFun, Finsupp.single_eq_pi_single]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i✝ =
    (TensorProduct.mk R R ((i : n) → A i)) 1 ∘ₗ LinearMap.single R A i✝

Tactic:
rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (lift { toFun := fun s ↦ HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (1 ⊗ₜ[R] x) = (Hom.hom g) x

Tactic:
lift.tmul,

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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ ({ toFun := fun s ↦ HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ } 1) x = (Hom.hom g) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s' ⊗ₜ[R] (ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))

Tactic:
lift.tmul,

Goal state after:
case tmul
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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ ({ toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ } s')
      ((ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))
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
g : (extendScalars f).obj X ⟶ Y
x : ↑X
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f) g)) x =
    (Hom.hom ((ExtendRestrictScalarsAdj.unit f).app X ≫ (restrictScalars f).map g)) x

Tactic:
by
      dsimp
      rfl

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

Goal state before:
pp: case e'_3.tmul.tmul
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
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
⊢ x₁ ⊗ₜ[R] y₁ ⊗ₜ[S] (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (comul x₂ ⊗ₜ[R] comul y₂) =
    F (x₁ ⊗ₜ[S] comul x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] comul y₂))

Tactic:
hopf_tensor_induction comul (R := S) x₂ with x₂₁ x₂₂

Goal state after:
case e'_3.tmul.tmul.tmul
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
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
x₂₁ x₂₂ : A
⊢ x₁ ⊗ₜ[R] y₁ ⊗ₜ[S] (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₂₁ ⊗ₜ[S] x₂₂ ⊗ₜ[R] comul y₂) =
    F (x₁ ⊗ₜ[S] (x₂₁ ⊗ₜ[S] x₂₂) ⊗ₜ[R] (y₁ ⊗ₜ[R] comul y₂))
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: case h
X✝ Y✝ Z✝ : Preord
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a✝ : ↑X✝
⊢ (PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization)) (Quotient.mk'' a✝) =
    (PartOrd.Hom.hom
        (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization))
      (Quotient.mk'' a✝)

Tactic:
exact OrderHom.antisymmetrization_apply_mk ..

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x * invSelf x = 1

Tactic:
convert! IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1

Goal state after:
case e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x = mk' S (↑⟨x, ⋯⟩) 1
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Tactic:
case mem_ideal_of_subset =>
    simp only [I, SetLike.mem_coe, mem_mk'] at hz
    induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ s * t ⊆ ↑I

Tactic:
rintro - ⟨x, hx, r, -, rfl⟩

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
x : R
hx : x ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) x r ∈ ↑I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * (algebraMap R B) x ^ d = (algebraMap R B) a₀
⊢ ¬(algebraMap R B) a₀ = 0

Tactic:
rw [← H]

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * (algebraMap R B) x ^ d = (algebraMap R B) a₀
⊢ ¬b * (algebraMap R B) x ^ d = 0