mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
⊢ f m = 1 • f m

Tactic:
one_smul

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
⊢ f m = f m
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))
s : S
m : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f')) s) (eM m) =
    ((((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)).compl₂ ↑eM.symm).compr₂
          ↑(LinearEquiv.restrictScalars R eN))
        s)
      (eM m)

Tactic:
simp [this]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))
s : S
m : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m =
    ((((↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f')).compl₂ ↑eM).compr₂
          ↑(LinearEquiv.restrictScalars R eN.symm))
        s)
      m

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2

Tactic:
simp [hm, mem_sym2_iff]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
by
    rw [List.sym, ← nil_append (List.sym (n + 1) xs)]
    apply Sublist.append (nil_sublist _)
    exact h.sym (n + 1)

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : Rel α a✝ b✝
⊢ Rel β (Prod.map f f a✝) (Prod.map f f b✝)

Tactic:
cases h

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (x✝, y✝))

case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (y✝, x✝))
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' : α
h : Rel α (a, b) (a', a')
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a'

Tactic:
cases h

Goal state after:
case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ diag (s(x✝, y✝).diagElem h) = s(x✝, y✝)

Tactic:
cases h

Goal state after:
case h.refl
α : Type u_1
x✝ : α
⊢ diag (s(x✝, x✝).diagElem ⋯) = s(x✝, x✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
tauto

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ ↑R q' ∘ₗ ↑R h ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f

Tactic:
← LinearMap.comp_assoc

Goal state after:
case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ (↑R q' ∘ₗ ↑R h) ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ LeftInverse (Quot.map fromVector ⋯) (Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯)

Tactic:
by apply Sym2.ind; aesop (add norm unfold [Sym2.fromVector])

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
⊢ IsPushout R T R' T' ↔ IsPushout S T S' T'

Tactic:
let f : R' →ₗ[R] S' := (IsScalarTower.toAlgHom R R' S').toLinearMap
  have : IsScalarTower R S T' := .of_algebraMap_eq fun x ↦ by
    rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']
  have heq : (toAlgHom S S' T').toLinearMap.restrictScalars R ∘ₗ f =
      (toAlgHom R R' T').toLinearMap := by
    ext x
    simp [f, ← IsScalarTower.algebraMap_apply]
  rw [isPushout_iff, isPushout_iff, ← heq, IsBaseChange.comp_iff]
  exact Algebra.IsPushout.out

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso g

Tactic:
rw [← id_comp g, ← inv_hom_id f, assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ∃ i_1, X i_1 = X i

Tactic:
exact ⟨i, rfl⟩

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

Goal state before:
pp: case mp.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝)

Tactic:
tauto

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

Goal state before:
pp: case mp.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝)

Tactic:
tauto

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Tactic:
tauto

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Tactic:
tauto

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Tactic:
tauto

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : nil.toList = (p.cons f).toList
⊢ nil = p.cons f

Tactic:
cases h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : (p.cons f).toList = nil.toList
⊢ p.cons f = nil

Tactic:
cases h

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
⊢ f = eqToHom h ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
cases h

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ (eqToHom h).op = eqToHom ⋯

Tactic:
cases h

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (eqToHom ⋯).op = eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
⊢ (eqToHom h).unop = eqToHom ⋯

Tactic:
cases h

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ (eqToHom ⋯).unop = eqToHom ⋯
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (C ⥤ D)ᵒᵖ
⊢ ∀ {Y : (C ⥤ D)ᵒᵖ} (f : F ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop Y).opUnopIso.op.hom = (unop F).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f

Tactic:
G

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
⊢ ∀ (f : F ⟶ G),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop G).opUnopIso.op.hom = (unop F).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (Cᵒᵖ ⥤ D)ᵒᵖ
⊢ ∀ {Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : F ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop F).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f

Tactic:
G

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
⊢ ∀ (f : F ⟶ G),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop G).rightOpLeftOpIso.op.hom =
      (unop F).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g

Tactic:
cases h

Goal state after:
case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X✝ Y✝ : ι → C
f : (i : ι) → X✝ i ⟶ Y✝ i
X Y : C
i : ι
⊢ ∃ i_1, Arrow.mk (f i) = Arrow.mk (f i_1)

Tactic:
exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ single f f

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

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
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : ∃ hX hY, F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (ConcreteCategory.hom ((forget₂ C D).map f ≫ (forget₂ C D).map g)) x =
    (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x)

Tactic:
CategoryTheory.comp_apply

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x) =
    (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x)
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (hom ((forget₂ C D).map f ≫ (forget₂ C D).map g)) x = (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)

Tactic:
CategoryTheory.comp_apply

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x) =
    (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ ∀ {G : C ⥤ D} (x : F ≅ G), P.map F ≤ P.map G

Tactic:
G

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
⊢ ∀ (x : F ≅ G), P.map F ≤ P.map G
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toRingCatIso.isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F G : C ⟶ D
h : F = G
⊢ (eqToHom h).toNatTrans = eqToHom ⋯

Tactic:
cases h

Goal state after:
case refl
C D : Cat
F : C ⟶ D
⊢ (eqToHom ⋯).toNatTrans = eqToHom ⋯
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
u : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F
⊢ uliftCoyonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) (uliftCoyonedaEquiv u)) =
    uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ uliftCoyonedaEquiv.symm (uliftCoyonedaEquiv u)

Tactic:
rw [uliftCoyonedaEquiv_naturality]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
u : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F
⊢ uliftCoyonedaEquiv.symm (uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ u)) =
    uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ uliftCoyonedaEquiv.symm (uliftCoyonedaEquiv u)
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
this : ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯ = 𝟙 (Arrow.mk (τ.app X))

Tactic:
ext <;> simp [← Functor.map_comp]

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

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv B X).symm l.l ≫ p = v

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv B Y).symm ((adj.homEquiv B Y) v) = v
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = hl.lift { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } } ≫ hi.hom

Tactic:
← hl.uniq _ (f ≫ hi.inv) _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = (f ≫ hi.inv) ≫ hi.hom

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j = { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }

Tactic:
rw [← hl.uniq _ (hi.hom ≫ f) _]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f

Tactic:
by
  rw [hI.hom_ext f (hI.to X)]
  apply InitialMonoClass.isInitial_mono_from

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ limMap (𝟙 F) = 𝟙 (limit F)

Tactic:
apply Limits.limit.hom_ext

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ ∀ (j : J), limMap (𝟙 F) ≫ limit.π F j = 𝟙 (limit F) ≫ limit.π F j