mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddZeroClass (G i)
inst✝² : (i : ι) → DistribSMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ r • (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = r • ⟦⟨i, x✝¹⟩⟧ + r • ⟦⟨i, x✝⟩⟧

Tactic:
by
    simp_rw [add_def, smul_def, smul_add, add_def]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
inst✝ : Fintype ι
⊢ 𝔼 i, f i = (↑(Fintype.card ι))⁻¹ • ∑ i, f i

Tactic:
rw [expect, card_univ]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ i ∈ range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1) *
      ∏ z ∈ F, g z.2 / g z.1 =
    g b / g a

Tactic:
rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm,
      prod_range_succ, ← mul_assoc,
      ← prod_mul_distrib,
      prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
      prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)]
  simp

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by
  ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂

Tactic:
apply h.equiv.injective

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv (h.equiv.symm ((f x₁) x₂)) = h.equiv (x₁ ⊗ₜ[R] x₂)
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 0 [ZMOD n]
⊢ s.sum ≡ 0 [ZMOD n]

Tactic:
simpa using multisetSum_map_zero h

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

Goal state before:
pp: α : Type u_1
m : Multiset α
⊢ m.sym2.card = (m.card + 1).choose 2

Tactic:
refine m.inductionOn fun xs => ?_

Goal state after:
α : Type u_1
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
⊢ ∀ (a₁ : α × α) (b₁ : β × β) (a₂ : α × α) (b₂ : β × β),
    a₁ ≈ a₂ → b₁ ≈ b₂ → ↑f a₁.1 a₁.2 b₁.1 b₁.2 = ↑f a₂.1 a₂.2 b₂.1 b₂.2

Tactic:
rintro _ _ _ _ ⟨⟩ ⟨⟩

Goal state after:
case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2

case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (y✝, x✝).1 (y✝, x✝).2

case swap.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (y✝¹, x✝¹).1 (y✝¹, x✝¹).2 (x✝, y✝).1 (x✝, y✝).2

case swap.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (y✝¹, x✝¹).1 (y✝¹, x✝¹).2 (y✝, x✝).1 (y✝, x✝).2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ z.IsDiag

Tactic:
have h' := Sym2.other_spec h

Goal state after:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ z.IsDiag
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
hd : ¬z.IsDiag
h : a ∈ z
⊢ Mem.other h ≠ a

Tactic:
by
  contrapose hd
  have h' := Sym2.other_spec h
  rw [hd] at h'
  rw [← h']
  simp

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
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ ↑(cancelBaseChangeAlg R S A B C) = cancelBaseChange R S A B C

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom

Tactic:
apply Category.id_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
x✝ : CC X
⊢ (hom (𝟙 X)) x✝ = id x✝

Tactic:
simp [ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.map (eqToHom p) = eqToHom ⋯

Tactic:
cases p; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ P.strictMap (𝟭 C) f✝ ↔ P f✝

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f → P f

Tactic:
intro hf
    rw [ofHoms_iff] at hf
    obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
    exact hf

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ Groupoid C

Tactic:
apply Groupoid.ofIsIso

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ ∀ {X Y : C} (f : X ⟶ Y), IsIso f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
intro X Y Z e f

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
intro X Y Z e f

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

Tactic:
intro X Y Z e f

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)

Tactic:
intro X Y Z e f

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

Tactic:
intro X Y Z e f

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
intro X Y Z e f

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ g₁ = g₂

Tactic:
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by cat_disch

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = (colimitCocone h).extend f

Tactic:
by
  dsimp [coconeOfHom, colimitCocone, Cocone.extend]
  congr
  conv_lhs => rw [← Category.id_comp f]
  exact h.homEquiv_comp f (𝟙 X)

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : yoneda.obj (unop X) ⟶ F
⊢ (ConcreteCategory.hom ((yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a =
    (ConcreteCategory.hom ((yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f)).toFun a

Tactic:
apply ULift.ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : yoneda.obj (unop X) ⟶ F
⊢ ((ConcreteCategory.hom ((yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a).down =
    ((ConcreteCategory.hom ((yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f)).toFun a).down
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (a₁ b₁ a₂ b₂ : C), a₁ ≈ a₂ → b₁ ≈ b₂ → Nonempty (a₁ ⟶ b₁) = Nonempty (a₂ ⟶ b₂)

Tactic:
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
          exact
            propext
              ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
                Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F G : C ⥤ Type v₁
α : coyoneda.obj (op X) ⟶ F
β : F ⟶ G
⊢ coyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app X)) (coyonedaEquiv α)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : coyoneda.obj (op X) ⟶ F
⊢ (ConcreteCategory.hom ((coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a =
    (ConcreteCategory.hom ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f)).toFun a

Tactic:
apply ULift.ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : coyoneda.obj (op X) ⟶ F
⊢ ((ConcreteCategory.hom ((coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a).down =
    ((ConcreteCategory.hom ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f)).toFun
        a).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
isIso_iff_coyoneda_map_bijective

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x ↦ f ≫ x) ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map.up
X✝ : Type u
X Y : Discrete X✝
down✝ : PLift (X.as = Y.as)
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map { down := down✝ } =
    eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map { down := down✝ } ≫ eqToHom ⋯

Tactic:
apply ULift.ext

Goal state after:
case h_map.up
X✝ : Type u
X Y : Discrete X✝
down✝ : PLift (X.as = Y.as)
⊢ ((Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map { down := down✝ }).down =
    (eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map { down := down✝ } ≫ eqToHom ⋯).down
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x y : ↑(typeToCat.obj X✝)
f : x ⟶ y
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
apply ULift.ext

Goal state after:
X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x y : ↑(typeToCat.obj X✝)
f : x ⟶ y
⊢ ((typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f).down =
    (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
x : ↑F.sections
⊢ (G.sectionsEquivHom X) ((ConcreteCategory.hom ((sectionsFunctor C).map f)) x) = (F.sectionsEquivHom X) x ≫ f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ (G.sectionsEquivHom X).symm (τ ≫ f) =
    (ConcreteCategory.hom ((sectionsFunctor C).map f)) ((F.sectionsEquivHom X).symm τ)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case e_a.e_a
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b

Tactic:
apply ULift.ext

Goal state after:
case e_a.e_a
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y := ⋯
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C

Tactic:
by
  constructor
  intro F
  apply hasColimit_of_equivalence_comp e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
⊢ { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        default ≫
      s.ι.app default =
    s.ι.app default

Tactic:
apply Category.id_comp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := left } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := left }

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := right } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := right }

Tactic:
· simp [Category.id_comp]

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := right } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryProduct X Y
x✝ : Discrete WalkingPair
⊢ (limit.cone (pair X Y)).π.app { as := right } =
    (Iso.refl (limit.cone (pair X Y)).pt).hom ≫ (BinaryFan.mk prod.fst prod.snd).π.app { as := right }

Tactic:
· simp [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
⊢ f.comp (id Y) = f

Tactic:
by
  cases f <;> rfl

Goal state after: