mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ∀ (i : n × n),
    (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) i) =
      (LinearMap.id f) ((stdBasis R n n) i)

Tactic:
intro ⟨i, j⟩

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) (i, j)) =
    (LinearMap.id f) ((stdBasis R n n) (i, j))
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ ¬IsReduced (C ⊗[R] ↥D)

Tactic:
simp_rw [isReduced_iff, not_forall]

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ ∃ x, ∃ (_ : IsNilpotent x), ¬x = 0
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f g : ι → M
⊢ 𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i

Tactic:
by
  simp [expect, sum_add_distrib]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ InjOn (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Iio k)

Tactic:
intro j hj j' hj' hjj'

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j ∈ Iio k
j' : ℕ
hj' : j' ∈ Iio k
hjj' :
  (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j'
⊢ j = j'
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a

Tactic:
rw [expect, expect, smul_mul_assoc, sum_mul]

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ 𝔼 j, (if i = j then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
expect_univ,

Goal state after:
ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ (↑(Fintype.card ι))⁻¹ • ∑ j, (if i = j then ↑(Fintype.card ι) else 0) * f j = f i
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
inst✝ : InvolutiveNeg α
f : α → β
hf : Function.Odd f
s : Finset α
hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s
⊢ s.sum f = 0

Tactic:
by
  simpa [neg_eq_self, funext hf, hs] using (Finset.sum_map s (Equiv.neg α).toEmbedding f).symm

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (Iio (k + 1)).PairwiseDisjoint fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2

Tactic:
intro j hj j' hj' hjj'

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j ∈ Iio (k + 1)
j' : ℕ
hj' : j' ∈ Iio (k + 1)
hjj' : j ≠ j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ (x :: xs).length + xs.sym2.length = ((x :: xs).length + 1).choose 2

Tactic:
length_cons,

Goal state after:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ xs.length + 1 + xs.sym2.length = (xs.length + 1 + 1).choose 2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)

Tactic:
rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n

Tactic:
length_cons,

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (xs.length + 1).multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
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
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
⊢ ∃! g', ↑S g' ∘ₗ h = r

Tactic:
have : IsScalarTower R T Q := IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp [IsScalarTower.algebraMap_apply R S T]

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
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
⊢ ∃! g', ↑S g' ∘ₗ h = r
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
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
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
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'
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
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ ∀ (c : S) (x : S ⊗[R] M), ↑(cancelBaseChangeAux R S A B M).symm (c • x) = c • ↑(cancelBaseChangeAux R S A B M).symm x

Tactic:
by
    intro s x
    induction x with
    | zero => simp
    | add x y hx hy => simp only [smul_add, map_add, hx, hy]
    | tmul s' m => simp [Algebra.smul_def, TensorProduct.smul_tmul']

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P.Is X

Tactic:
P.is_iff

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P X
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
cases Nat.succ_ne_zero _ hzero

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

Goal state before:
pp: case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
length_cons,

Goal state after:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : p.length + 1 = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
length_cons,

Goal state after:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : p.length + 1 = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ

Tactic:
fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure ≤ P.map F

Tactic:
isoClosure_le_iff

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.strictMap F ≤ P.map F
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ a₁✝ ≫ (L.objObjPreimageIso Y✝).inv = a₂✝ ≫ (L.objObjPreimageIso Y✝).inv

Tactic:
← cancel_epi (L.objObjPreimageIso _).hom

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ (L.objObjPreimageIso X✝).hom ≫ a₁✝ ≫ (L.objObjPreimageIso Y✝).inv =
    (L.objObjPreimageIso X✝).hom ≫ a₂✝ ≫ (L.objObjPreimageIso Y✝).inv
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j'

Tactic:
by
  cases w
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').hom

Tactic:
by
  cases w
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').inv

Tactic:
by
  cases w
  simp

Goal state after:
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
⊢ (P.isoClosure.strictMap F).isoClosure ≤ (P.strictMap F).isoClosure

Tactic:
isoClosure_le_iff

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
⊢ P.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.left ≫ (inv e).left = 𝟙 X.left

Tactic:
← Comma.comp_left,

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (e ≫ inv e).left = 𝟙 X.left
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
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
← Equiv.eq_symm_apply

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
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
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
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
← Equiv.eq_symm_apply

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
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
Module: Mathlib.CategoryTheory.Limits.IsLimit

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
t : Cocone F
h : IsColimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑p j' = ↑p j ≫ ((const J).obj W).map f

Tactic:
dsimp; rw [comp_id]; exact p.2 f

Goal state after:
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
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt, ι := h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) } =
    { pt := s_pt, ι := s_ι }

Tactic:
congr
    exact h.homEquiv.apply_symm_apply s_ι

Goal state after:
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:
intro X X' Y f g; rw [Equiv.symm_apply_eq]; simp [he]

Goal state after:
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:
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✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).obj X✝
⊢ (ConcreteCategory.hom
          ((F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftYoneda.{v₂, v₁, u₁}.obj X).map f)).toFun
      x✝

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫
                (hF.homNatIso Y✝).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).obj X✝
⊢ (ConcreteCategory.hom
          ((F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f)).toFun
      x✝

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝¹ : C
x✝ : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
                (hF.homNatIso' (unop Y✝)).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

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
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F

Tactic:
by
  have : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
  apply hasLimit_of_iso (e.invFunIdAssoc F)

Goal state after:
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
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ ι (F ⋙ G) j ≫ post F G = G.map (ι F j)

Tactic:
simp [colimit.post]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
by
  cases w
  simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ map (𝟙 (⊤_ C)) f = ((leftUnitor X).hom ≫ f) ≫ (leftUnitor Y).inv

Tactic:
Iso.eq_comp_inv,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ map (𝟙 (⊤_ C)) f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ prod.map f (𝟙 (⊤_ C)) = ((prod.rightUnitor X).hom ≫ f) ≫ (prod.rightUnitor Y).inv

Tactic:
Iso.eq_comp_inv,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ prod.map f (𝟙 (⊤_ C)) ≫ (prod.rightUnitor Y).hom = (prod.rightUnitor X).hom ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
⊢ k ≫ t.π.app none = l ≫ t.π.app none

Tactic:
by rw [← t.w inl, reassoc_of% h₀]

Goal state after: