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

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

Tactic:
piSplitLE_lt (h.trans_lt hj),

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
s : Set M
inst✝ : Small.{u, u_2} ↑s
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
suffices span R s = iSup (fun i : s ↦ span R ({(↑i : M)} : Set M)) by
    rw [this]
    apply small_iSup
  simp [← Submodule.span_iUnion]

Goal state after:
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
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q ⧸ (rTensor Q f).range
⊢ (inverse_of_rightInverse Q hfg hgh) ((toFun Q hfg).toFun y) = y

Tactic:
by
    simp only [rTensor.toFun, AddHom.toFun_eq_coe, coe_toAddHom]
    obtain ⟨y, rfl⟩ := Submodule.mkQ_surjective _ y
    simp only [Submodule.mkQ_apply, Submodule.liftQ_apply, rTensor.inverse_of_rightInverse_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap).ker = Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Tactic:
Ideal.map_includeRight_eq

Goal state after:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap).ker =
    (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype).range
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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ 0 * ⟦⟨i, x✝⟩⟧ = 0

Tactic:
simp_rw [zero_def i, mul_def, zero_mul]

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
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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
x✝ : ℚ
i : ι
x : G i
⊢ ⟦⟨i, x✝ • x⟩⟧ = ⟦⟨i, ↑x✝ * x⟩⟧

Tactic:
Rat.smul_def

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

Goal state before:
pp: case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a₁ ∈ range k, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂

Tactic:
intro i hi j hj hij

Goal state after:
case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i ∈ range k
j : ℕ
hj : j ∈ range k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ i = j
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
have hn := Int.emod_add_mul_ediv n a

Goal state after:
case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: 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
⊢ 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)

Tactic:
by gcongr; exact (Int.emod_lt_of_pos n ha).le

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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
r : S
x : S ⊗[R] M
⊢ ∀ (x y : S ⊗[R] M),
    (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x →
      (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y →
        (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)

Tactic:
intro x y hx hy
        rw [map_add, smul_add, map_add, smul_add, hx, hy]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

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

Tactic:
rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]

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

Goal state before:
pp: α : Type u_1
⊢ Function.Injective Finset.sym2

Tactic:
by
  intro s t h
  ext x
  simpa using congr(s(x, x) ∈ $h)

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

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

Tactic:
dedup_cons_of_notMem hm,

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

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

Tactic:
exact map_mk_disjoint_sym2 x xs hm

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

Goal state before:
pp: case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
      ← Multiset.coe_add, ← Multiset.singleton_add]

Goal state after:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ {s(y, y)} + (↑(List.map (fun y_1 ↦ s(y, y_1)) xs) + ({s(x, x)} + (↑(List.map (fun y ↦ s(x, y)) xs) + ↑xs.sym2))) =
    {s(x, x)} + (↑(List.map (fun y ↦ s(x, y)) xs) + ({s(y, y)} + (↑(List.map (fun y_1 ↦ s(y, y_1)) xs) + ↑xs.sym2)))
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case slnil
α : Type u_1
xs ys : List α
⊢ [].sym2 <+ [].sym2

Tactic:
apply slnil

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

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

Tactic:
rw [List.sym, Nat.multichoose]

Goal state after:
α : Type u_1
n : ℕ
xs x✝ : List α
⊢ [Sym.nil].length = 1
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
g : N →ₗ[S] O
hg : IsBaseChange T g
⊢ ∀ (Q : Type (max v₁ u_5 u_4)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module T Q]
    [inst_3 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1

Tactic:
intro Q _ _ _ _ i

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
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
by
      simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.coe_nil, Multiset.cons_zero,
        Multiset.cons_eq_cons, Multiset.singleton_inj, ne_eq, Multiset.singleton_eq_cons_iff,
        exists_eq_right_right, and_true]
      tauto

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
Y : D
⊢ (∃ X, P X ∧ F.obj X = Y) → P.strictMap F Y

Tactic:
by rintro ⟨X, hX, rfl⟩; exact ⟨X, hX⟩

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

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
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full

Tactic:
by
  have := Full.of_iso h.symm
  exact Full.of_comp_faithful F G

Goal state after:
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'
Φ : Symmetrify V ⥤q V'
hΦ : of ⋙q Φ = φ
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift φ

Tactic:
by
  subst_vars
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    cases f
    · rfl
    · exact hΦinv (Sum.inl _)

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

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hp : (p'.cons α).length ≤ n + 1
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
⊢ q'.length ≤ n

Tactic:
simp [Quiver.Path.length] at hq; lia

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
F : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    ext X
    exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

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

Goal state before:
pp: α : Type u₁
X Y Z : Discrete α
g : ULift.{u₁, 0} (PLift (X.as = Y.as))
f : ULift.{u₁, 0} (PLift (Y.as = Z.as))
⊢ ULift.{u₁, 0} (PLift (X.as = Z.as))

Tactic:
cases X

Goal state after:
case mk
α : Type u₁
Y Z : Discrete α
f : ULift.{u₁, 0} (PLift (Y.as = Z.as))
as✝ : α
g : ULift.{u₁, 0} (PLift ({ as := as✝ }.as = Y.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as✝ }.as = Z.as))
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u_1
X : I → C
⊢ Set.range (functor X).obj = Set.range X

Tactic:
simp [Discrete.functor, Set.range_comp, Discrete.as_bijective.surjective.range_eq]

Goal state after:
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
⊢ Monotone fun x ↦ x.map F

Tactic:
intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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

Goal state before:
pp: case refine_2
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
a✝ : ⊤ f
⊢ Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv))) ≅ Arrow.mk f

Tactic:
exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
      (by simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone isoClosure

Tactic:
intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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

Goal state before:
pp: X Y : GrpCat
f : X ⟶ Y
x✝ : IsIso ((forget GrpCat).map f)
i : (forget GrpCat).obj X ≅ (forget GrpCat).obj Y := asIso ((forget GrpCat).map f)
e : ↑X ≃* ↑Y :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toGrpIso.isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
coyonedaEquiv_naturality,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ coyonedaEquiv (coyoneda.map g.op ≫ f) = (ConcreteCategory.hom (f.app Y)) g
Module: Mathlib.CategoryTheory.Limits.Cones

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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : Cone F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd })).toFun X =
    (ConcreteCategory.hom (𝟙 (Cone F))).toFun X

Tactic:
cases X

Goal state after:
case mk
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd })).toFun
      { pt := pt✝, π := π✝ } =
    (ConcreteCategory.hom (𝟙 (Cone F))).toFun { pt := pt✝, π := π✝ }
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: case fst
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).fst =
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).fst

pp: case snd
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).snd

Tactic:
cases X

Goal state after:
case fst.mk
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
fst✝ : Cᵒᵖ
snd✝ : (const J).obj (unop fst✝) ⟶ F
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun
        ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun ⟨fst✝, snd✝⟩).fst

case snd
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).snd
Module: Mathlib.CategoryTheory.Limits.Cones

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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : Cocone F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd })).toFun X =
    (ConcreteCategory.hom (𝟙 (Cocone F))).toFun X

Tactic:
cases X

Goal state after:
case mk
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd })).toFun { pt := pt✝, ι := ι✝ } =
    (ConcreteCategory.hom (𝟙 (Cocone F))).toFun { pt := pt✝, ι := ι✝ }
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: case fst
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).fst =
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).fst

pp: case snd
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).snd

Tactic:
cases X

Goal state after:
case fst.mk
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
fst✝ : C
snd✝ : F.cocones.obj fst✝
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun ⟨fst✝, snd✝⟩).fst

case snd
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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).snd
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
by
  rw [Arrow.iso_w' e]
  infer_instance

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) → IsSplitEpi f

pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi f → IsSplitEpi (F.map f)

Tactic:
· intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi f → IsSplitEpi (F.map f)