mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
⊢ 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / ↑(#s)

Tactic:
by
  rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

pp: case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
· calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind

Goal state after:
case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum, apply_ite Nat.cast] at *

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = if a ∈ s then ↑(f a) else 0
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ioc m n, f i • g i =
    f n • ∑ i ∈ range (n + 1), g i - f (m + 1) • ∑ i ∈ range (m + 1), g i -
      ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
by
  simpa only [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (Nat.one_le_of_lt hmn),
    add_tsub_cancel_right] using! sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)

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

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
Sym2.eq_swap

Goal state after:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, x)

Tactic:
Sym2.eq_swap

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(x, y)
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
⊢ Function.Bijective ⇑f'

Tactic:
simp_rw [DFunLike.ext_iff, LinearMap.comp_apply, LinearMap.restrictScalars_apply] at hg

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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ Function.Bijective ⇑f'
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inl.inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ z
⊢ a ∈ x :: xs

Tactic:
· exact mem_of_mem_of_mem_sym ha hz

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')

Tactic:
simp [hinj.eq_iff]

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

Goal state before:
pp: α : Type u_1
⊢ fromRel ⋯ = {z | ¬z.IsDiag}

Tactic:
ext z; exact z.ind (by simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X

Tactic:
convert! w (𝟙 X)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
classical
    rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'

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

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c p' e, p = p'.cons e

pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0

Tactic:
· cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩

Goal state after:
case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0
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 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

Tactic:
f

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.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
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
⊢ ∀ (f : X ⟶ Y), (fun x ↦ x.map F) P f → (fun x ↦ x.map F) Q f

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
f : X ⟶ Y
⊢ (fun x ↦ x.map F) P f → (fun x ↦ x.map F) Q f
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
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
⊢ ∀ (f : X ⟶ Y), ⊤ f → ⊤.map F f

Tactic:
f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
⊢ ⊤ f → ⊤.map F f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
⊢ φ = ψ

Tactic:
have : ∀ g, (aux g).right = g ≫ f.hom := fun g => rfl

Goal state after:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ φ = ψ
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
⊢ ∀ (f : X ⟶ Y), P.isoClosure f → Q.isoClosure f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
⊢ P.isoClosure f → Q.isoClosure f
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)
X Y : C
⊢ ∀ (f : X ⟶ Y), IsIso f

Tactic:
f

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: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
⊢ ∀ (f : X ⟶ Y), P.isoClosure f → P f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
⊢ P.isoClosure f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : D
⊢ ∀ (f : X ⟶ Y), P.map F f → (P.map (F ⋙ G)).inverseImage G f

Tactic:
f

Goal state after:
case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : D
f : X ⟶ Y
⊢ P.map F f → (P.map (F ⋙ G)).inverseImage G f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → ((P.map F).map G).inverseImage (F ⋙ G) f

Tactic:
f

Goal state after:
case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ P f → ((P.map F).map G).inverseImage (F ⋙ G) f
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 G : C ⥤ D
e : F ≅ G
X Y : D
⊢ ∀ (f : X ⟶ Y), P.map F f → P.map G f

Tactic:
f

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
e : F ≅ G
X Y : D
f : X ⟶ Y
⊢ P.map F f → P.map G f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
⊢ ∀ (f : X ⟶ Y), P.inverseImage E.functor f → P.map E.inverse f

Tactic:
f

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage E.functor f → P.map E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
⊢ ∀ (f : X ⟶ Y), P f → (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
f

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
f : X ⟶ Y
⊢ P f → (P.inverseImage E.functor).inverseImage E.inverse 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:
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:
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:
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:
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:
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:
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.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
⊢ ∀ (f : X ⟶ X') (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g

Tactic:
f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
f : X ⟶ X'
⊢ ∀ (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
⊢ ∀ (f : yoneda.obj Z ⟶ yoneda.obj W), yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z)))) = f

Tactic:
f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
⊢ yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z)))) = f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
⊢ ∀ (f : coyoneda.obj Z ⟶ coyoneda.obj W),
    coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z)))) = f

Tactic:
f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : coyoneda.obj Z ⟶ coyoneda.obj W
⊢ coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z)))) = f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
    (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X Y : C
⊢ ∀ (f : X ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X Y : C
f : X ⟶ Y
⊢ (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
    (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ yonedaEquiv (yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom ((yoneda.map f).app (op X))) (𝟙 X) = f
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)),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f

Tactic:
f

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)
⊢ (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (f : Y ⟶ Z),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type v₁
f : Y ⟶ Z
⊢ ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
      ((evaluation Cᵒᵖ (Type v₁) ⋙
                (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
            X).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
⊢ ∀ (f : Y ⟶ Z),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation Cᵒᵖ (Type v₁) ⋙
            (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
      yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
    yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ ↾Quot.map (f ≫ g).toFunctor.obj ⋯ = ↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯

Tactic:
by -- Porting note(s): idem
    ext x
    apply @Quot.recOn _ _ _ x
    all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y

Tactic:
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y
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)),
    (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f

Tactic:
f

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)
⊢ (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : C
⊢ ∀ (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f

Tactic:
f

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : C
f : X ⟶ Y
⊢ (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f