mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = (piLTLim hi).symm ((invLimEquiv nat) (equivLim t)) ⟨↑l, ⋯⟩

Tactic:
piLTLim_symm_apply hi ⟨k, hk⟩ (by exact l.2),

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = ↑((invLimEquiv nat) (equivLim t)) ⟨k, hk⟩ ⟨↑⟨↑l, ⋯⟩, ⋯⟩
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
hfg : Exact ⇑f ⇑g
⊢ (rTensor Q f).range ≤ (rTensor Q g).ker

Tactic:
range_le_iff_comap,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
hfg : Exact ⇑f ⇑g
⊢ Submodule.comap (rTensor Q f) (rTensor Q g).ker = ⊤
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R P
inst✝ : Module.Flat R N
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(map f g)

Tactic:
rw [← LinearMap.rTensor_comp_lTensor]
  exact (Module.Flat.rTensor_preserves_injective_linearMap f hf).comp
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype β
s : Finset α
inst✝ : DecidableEq α
f : β → α
t : Finset β
h : Set.MapsTo f ↑t ↑s
⊢ t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens

Tactic:
simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]

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 : α
⊢ (F.intervalGapsWithin h a b (last k)).2 = b

Tactic:
simp [intervalGapsWithin, intervalGapsWithin.snd]

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 : α
j : ℕ
hj : j < k
this : ↑j ≠ last k
⊢ (F.intervalGapsWithin h a b ↑j).2 = ((F.orderEmbOfFin h) ⟨j, hj⟩).1

Tactic:
simp only [intervalGapsWithin, intervalGapsWithin.snd, this, ↓reduceDIte]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : ↑j ≠ last k
⊢ ((F.orderEmbOfFin h) ((↑j).castPred ⋯)).1 = ((F.orderEmbOfFin h) ⟨j, hj⟩).1
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : 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 < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
this :
  ∀ ⦃j : ℕ⦄,
    j < k + 1 →
      ∀ ⦃j' : ℕ⦄,
        j' < k + 1 →
          j ≠ j' →
            j < j' →
              Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2)
                j j'
hij' : ¬j < j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'

Tactic:
exact (this hj' hj hjj'.symm (by omega)).symm

Goal state after:
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
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m + ∑ k ∈ Ico (m + 1) n, f k • g k =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
conv in (occs := 3) (f _ • g _) => rw [← sum_range_succ_sub_sum g]

Goal state after:
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
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m + ∑ k ∈ Ico (m + 1) n, f k • (∑ i ∈ range (k + 1), g i - ∑ i ∈ range k, g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
Module: Mathlib.Data.List.Sym

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

Tactic:
intro h
    exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩

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

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (map (fun y ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
specialize ih h.of_cons

Goal state after:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (map (fun y ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
⊢ ∀ (a : α) (x : β) (x_1 : x ∈ d), ⋯.choose = a → a ∈ s

Tactic:
intro i e he hi

Goal state after:
case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ i ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
xs ys : List α
x : α
l₁✝ l₂✝ : List α
h : l₁✝ ~ l₂✝
ih : l₁✝.sym2 ~ l₂✝.sym2
⊢ List.map (fun y ↦ s(x, y)) l₁✝ ++ l₁✝.sym2 ~ List.map (fun y ↦ s(x, y)) l₂✝ ++ l₂✝.sym2

Tactic:
exact (h.map _).append ih

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

Goal state before:
pp: case property
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ ∀ (a₁ a₂ : α), (fun x1 x2 ↦ ↑[x1, x2]) a₁ a₂ = (fun x1 x2 ↦ ↑[x1, x2]) a₂ a₁

Tactic:
simp [List.Perm.swap]

Goal state after:
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:
by
  classical
    rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'

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
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'
h : IsPushout R S R' S'
x✝ : S
⊢ (let __spread.0 := (TensorProduct.comm R R' S).toAddEquiv.trans (equiv R S R' S').toAddEquiv;
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      (1 ⊗ₜ[R] x✝) =
    (toAlgHom R S S').toLinearMap x✝

Tactic:
by simp [equiv_tmul]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β

Tactic:
by
  rw [← trans_assoc, self_symm_id, refl_trans]

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

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
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ g.app X = h.app X

Tactic:
rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
hzero : p.length = 0
⊢ a = b

Tactic:
cases p

Goal state after:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

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
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a : V
p : Path a a
hzero : p.length = 0
⊢ p = nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
h : p₁.comp q₁ = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁ = q₂

Tactic:
induction q₁ with
  | nil =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · exact ⟨h, rfl⟩
    · cases hq
  | cons q₁ f₁ ih =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · cases hq
    · simp only [comp_cons, cons.injEq] at h
      obtain rfl := h.1
      obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
      rw [h.2.2.eq]
      exact ⟨rfl, rfl⟩

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.length + 1 = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
Nat.zero_add,

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 = 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
rintro X ⟨X', hX', ⟨e⟩⟩
  exact ⟨X', h _ hX', ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
Y : D
⊢ F.essImage Y

Tactic:
obtain ⟨X, rfl⟩ := h Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
X : C
⊢ F.essImage (F.obj X)
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToHom p ≫ eqToHom q = eqToHom ⋯

Tactic:
cases p

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast ⋯ q = eqToHom p ≫ q

Tactic:
cases p

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast ⋯ q = eqToHom ⋯ ≫ q
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ ⋯.mpr q = eqToHom p ≫ q

Tactic:
cases p

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ ⋯.mpr q = eqToHom ⋯ ≫ q
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

Goal state after:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯
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.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom

Tactic:
cases p

Goal state after:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ P (e ≫ f)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf
    simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
Q.isoClosure_eq_self

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ Q ≤ Q
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
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F

Tactic:
by
  rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget RingCat).map f)

Goal state after:
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)
⊢ IsIso f
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 : C
Y : D
g : X ⟶ G.obj Y
⊢ adj.unit.app X ≫ G.map (F.map g) ≫ G.map (adj.counit.app Y) = g

Tactic:
← assoc,

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 : C
Y : D
g : X ⟶ G.obj Y
⊢ (adj.unit.app X ≫ G.map (F.map g)) ≫ G.map (adj.counit.app 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
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
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'

Tactic:
← assoc,

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
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y'))) ≫ g'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : F.IsRepresentable
X : Cᵒᵖ
f : unop X ⟶ F.reprX
⊢ (ConcreteCategory.hom (F.reprW.hom.app X)) f = (ConcreteCategory.hom (F.map f.op)) F.reprx

Tactic:
apply RepresentableBy.homEquiv_eq

Goal state after:
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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
this : Setoid D := isIsomorphicSetoid D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X

Tactic:
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
⊢ ∀ [Mono z], HasLiftingProperty g z

Tactic:
by
    intro
    apply HasLiftingProperty.of_arrow_iso_left e z

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 G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
⊢ lift F c ≫ limMap α = lift G ((Cone.postcompose α).obj c)

Tactic:
ext
  rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
  rfl

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✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
← assoc,

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✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ (ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D) ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
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)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
← assoc,

Goal state after:
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)
c : Cocone F
j✝ : J
⊢ (ι (F ⋙ G) j✝ ≫ post F G) ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
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)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
← assoc,

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

Tactic:
← assoc,

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
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ (ι ((E ⋙ F) ⋙ G) j ≫ post (E ⋙ F) G) ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G
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✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
← assoc,

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✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (ι (E ⋙ F) j✝ ≫ pre F E) ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (E.whiskerLeft α) ≫ pre G E
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✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = ι (E ⋙ F) j✝ ≫ colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
← assoc,

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✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (ι (E ⋙ F) j✝ ≫ colim.map (E.whiskerLeft α)) ≫ pre G E
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
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
← assoc,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (ι (F ⋙ H) j✝ ≫ post F H) ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H