mathlib-initiative/mathlib-tactics huggingface dataset:
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
j' : ℕ
hj' : j' < 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'

Tactic:
simp only [hj, hj', intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt] at hjj'

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
j' : ℕ
hj' : j' < k
hjj' :
  (((F.orderEmbOfFin h) ⟨j, hj⟩).1, ((F.orderEmbOfFin h) ⟨j, hj⟩).2) =
    (((F.orderEmbOfFin h) ⟨j', hj'⟩).1, ((F.orderEmbOfFin h) ⟨j', hj'⟩).2)
⊢ j = j'
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:
by
  intro j hj j' hj' hjj'
  rw [mem_Iio] at hj hj'
  simp only [hj, hj', intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt] at hjj'
  grind [F.orderEmbOfFin (α := α ×ₗ α) h |>.injective hjj']

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : Function.onFun Disjoint (fun z ↦ Icc z.1 z.2) (G ⟨j - 1, ⋯⟩) (G ⟨j, ⋯⟩)
⊢ (G ⟨j - 1, ⋯⟩).2 ≤ (G ⟨j, ⋯⟩).1

Tactic:
contrapose! this

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
⊢ ¬Function.onFun Disjoint (fun z ↦ Icc z.1 z.2) (G ⟨j - 1, ⋯⟩) (G ⟨j, ⋯⟩)
Module: Mathlib.Data.Int.Interval

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

Tactic:
add_comm n a

Goal state after:
case inr.mpr.inr.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 : n % a ≤ i
⊢ i + a * (n / a) < a + n
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • 0) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun 0

Tactic:
simp_all [TensorProduct.smul_tmul']

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x✝ : M₂
y✝ : M₁
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x✝ ⊗ₜ[R] y✝) =
    (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all [TensorProduct.smul_tmul']

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x✝ y✝ : M₂ ⊗[R] M₁
a✝¹ : (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x✝) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun x✝
a✝ : (↑(TensorProduct.comm R M₂ M₁)).toFun (s • y✝) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun y✝
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • (x✝ + y✝)) =
    (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun (x✝ + y✝)

Tactic:
simp_all [TensorProduct.smul_tmul']

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
· simp only [range_eq_Ico]
    rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]
    simp only [← range_eq_Ico]

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 = s(x, x) :: (map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup)

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

Tactic:
List.Disjoint.dedup_append,

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).dedup ++ xs.sym2.dedup) =
    s(x, x) :: (map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup)

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

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
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case inl
α : Type ?u.3
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
| inl h =>

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (fun p ↦ f x ::ₛ p) ∘ Sym.map f = Sym.map f ∘ fun p ↦ x ::ₛ p

Tactic:
ext s

Goal state after:
case e_f
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
s : Sym α n
⊢ ↑(((fun p ↦ f x ::ₛ p) ∘ Sym.map f) s) = ↑((Sym.map f ∘ fun p ↦ x ::ₛ p) s)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ List.sym (n + 1) (map f (x :: xs)) = map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
by
    rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]
    simp only [map_map, List.sym, map_append, append_cancel_right_eq]
    congr
    ext s
    simp only [Function.comp_apply, Sym.map_cons]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_14
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
e_5✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_6✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_10✝ : toModule ≍ leftModule
e_11✝ : toModule ≍ leftModule
⊢ (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap = AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id

Tactic:
ext s

Goal state after:
case e'_14
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
e_5✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_6✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_10✝ : toModule ≍ leftModule
e_11✝ : toModule ≍ leftModule
s : S
⊢ ((AlgebraTensorModule.curry (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap) 1) s =
    ((AlgebraTensorModule.curry (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)) 1) s
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
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
this : F.Faithful
⊢ Nonempty F.FullyFaithful

Tactic:
have : F.Full := ⟨(hF _ _).surjective⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
this✝ : F.Faithful
this : F.Full
⊢ Nonempty F.FullyFaithful
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

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

Tactic:
· rintro X ⟨Y, hY, ⟨e⟩⟩
    exact ⟨F.obj Y, ⟨Y, hY⟩, ⟨e.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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

Tactic:
cases q

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

Tactic:
cases q

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

Tactic:
cases q

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
⊢ W = W'

Tactic:
funext X Y f
  rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f0x1 ≫ fx11 = fx01 ≫ f1x1

Tactic:
← cancel_epi f00x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f00x ≫ f0x1 ≫ fx11 = f00x ≫ fx01 ≫ f1x1
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
s t : Cone F
h : IsLimit t
f f' : s ⟶ t
⊢ ∀ {g : s ⟶ t}, g = h.liftConeMorphism s

Tactic:
intro g

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s
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.app X ≫ F.map g)) (𝟙 X) = (ConcreteCategory.hom (f.app Y)) (g ≫ 𝟙 Y)

Tactic:
← f.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
⊢ (ConcreteCategory.hom ((coyoneda.obj (op X)).map g ≫ f.app Y)) (𝟙 X) = (ConcreteCategory.hom (f.app Y)) (g ≫ 𝟙 Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app none = i.hom ≫ t.π.app none

pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.left) = i.hom ≫ t.π.app (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.right) = i.hom ≫ t.π.app (some WalkingPair.right)

Tactic:
· have h₁ := s.π.naturality WalkingCospan.Hom.inl
    dsimp at h₁
    simp only [Category.id_comp] at h₁
    have h₂ := t.π.naturality WalkingCospan.Hom.inl
    dsimp at h₂
    simp only [Category.id_comp] at h₂
    simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]

Goal state after:
case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.left) = i.hom ≫ t.π.app (some WalkingPair.left)

case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.right) = i.hom ≫ t.π.app (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
inst✝³ : F.EssSurj
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).EssSurj

Tactic:
apply Comma.essSurj_map

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

Goal state before:
pp: case left.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.left } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.left }

Tactic:
simpa using w ⟨.left⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
by
    obtain ⟨a, ha⟩ := F.map_surjective f.right
    exact ⟨Under.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by ext; simpa⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst✝³ : F.EssSurj
inst✝² : G.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
⊢ (map₂ α β).EssSurj

Tactic:
apply Comma.essSurj_map

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ (pullback.fst f g ≫ f) ≫ i = (pullback.snd f g ≫ g) ≫ i

Tactic:
rw [cancel_mono]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
induction j with | _ j
       =>  _ 

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

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
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk X✝.hom.left).hom

Tactic:
by
    rw [← w φ, comp_left]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
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
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ X✝.left.hom ≫ R.map f.left.right ≫ R.map Y✝.hom = X✝.left.hom ≫ R.map X✝.hom

Tactic:
← R.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
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
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ X✝.left.hom ≫ R.map (f.left.right ≫ Y✝.hom) = X✝.left.hom ≫ R.map X✝.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
⊢ m = s.π

Tactic:
by
    convert! h
    exact (Category.id_comp _).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X _Y _Z : C
r : ℕ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
exact (Preadditive.rightComp X g).map_nsmul r f

Goal state after: