mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁴ : Monoid R
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : (i : ι) → MulDistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
⊢ ⟦⟨Classical.arbitrary ι, r • (fun x ↦ 1) (Classical.arbitrary ι)⟩⟧ = 1

Tactic:
rw [smul_one]

Goal state after:
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✝⁴ : Monoid R
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : (i : ι) → MulDistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
⊢ ⟦⟨Classical.arbitrary ι, 1⟩⟧ = 1
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₁ : 0 < j
hj₂ : j - 1 < k
⊢ j = (j - 1).succ

Tactic:
omega

Goal state after:
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:
by rw [expect, expect, smul_mul_assoc, sum_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
⊢ ∏ z ∈ F, f z.1 z.2 = ∏ i ∈ range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1

Tactic:
by
  set p := F.intervalGapsWithin h a b
  symm
  apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
  · exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)
  · intro i hi j hj hij
    rw [mem_range] at hi hj
    apply F.intervalGapsWithin_injOn h a b <;> grind
  · intro z hz
    obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz
    exact ⟨i, by grind, hi₂⟩
  · simp

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

Goal state before:
pp: α : 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
⊢ k - 1 + 1 = k

Tactic:
omega

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

Goal state before:
pp: α : 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
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ 0 < j

Tactic:
omega

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

Goal state before:
pp: α : 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
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j - 1 < k

Tactic:
omega

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

Goal state before:
pp: α : 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
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j < k

Tactic:
omega

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

Goal state before:
pp: α : 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
⊢ j - 1 < k

Tactic:
omega

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

Goal state before:
pp: α : 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
⊢ j < k

Tactic:
omega

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

Goal state before:
pp: a a✝ : ℤ
⊢ a ≤ a✝ ∧ a✝ ≤ a + 1 ↔ a✝ = a ∨ a✝ = a + 1

Tactic:
omega

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

Goal state before:
pp: α : 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
⊢ j < k

Tactic:
omega

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

Goal state before:
pp: α : 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
⊢ j - 1 < k

Tactic:
omega

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

Goal state before:
pp: α : 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
hG : (G ⟨j - 1, ⋯⟩).1 ≤ (G ⟨j, ⋯⟩).1
⊢ j < k

Tactic:
omega

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
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'
⊢ j' < j

Tactic:
omega

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

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
by
  obtain rfl | ha := eq_or_lt_of_le h
  · simp
  ext i
  simp only [mem_image, mem_Ico]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩
  rintro ⟨hi₀, hia⟩
  have hn := Int.emod_add_mul_ediv n a
  obtain hi | hi := lt_or_ge i (n % a)
  · refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
    · calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
  · refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · exact hn.symm.le.trans (add_le_add_left hi _)
    · rw [add_comm n a]
      refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
      simp only [le_add_iff_nonneg_left]
      exact Int.emod_nonneg n (ne_of_gt ha)
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

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

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) ≤ a✝ ∧ a✝ ≤ ↑n + 1 ↔ a✝ = -(↑m + 1) ∨ a✝ = ↑n + 1 ∨ -↑m ≤ a✝ ∧ a✝ ≤ ↑n

Tactic:
omega

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

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) ≤ a✝ ∧ a✝ < ↑n + 1 ↔ a✝ = -(↑m + 1) ∨ a✝ = ↑n ∨ -↑m ≤ a✝ ∧ a✝ < ↑n

Tactic:
omega

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
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
⊢ j' - 1 + 1 = j'

Tactic:
omega

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
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j < k

Tactic:
omega

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
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j' - 1 < k

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = ↑(f a)

Tactic:
apply Finset.sum_eq_single

Goal state after:
case h₀
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

case h₁
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = ↑(f a)

Tactic:
apply Finset.sum_eq_single

Goal state after:
case h₀
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

case h₁
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
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 +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
        ∑ x ∈ Ico m (n - 1), (f x • ∑ i ∈ range (x + 1), g i - f (x + 1) • ∑ i ∈ range (x + 1), 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

Tactic:
have : ∀ i, f i • G (i + 1) - f (i + 1) • G (i + 1) = -((f (i + 1) - f i) • G (i + 1)) := by
    intro i
    rw [sub_smul]
    abel

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
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
        ∑ x ∈ Ico m (n - 1), (f x • ∑ i ∈ range (x + 1), g i - f (x + 1) • ∑ i ∈ range (x + 1), 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: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
h' : (fun y ↦ s(x, y)) x ∈ map (fun y ↦ s(x, y)) xs
⊢ False

Tactic:
simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs ys : List α
h : xs <+ ys
n : ℕ
⊢ List.sym (n + 1) [] <+ List.sym (n + 1) []

Tactic:
simp only [refl]

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
hX : X = X'
hY : Y = Y'
⊢ X' ⟶ Y'

Tactic:
subst hX hY

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f : X ⟶ Y
⊢ X ⟶ Y
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f g : X ⟶ Y
h : homOfEq f hX hY = homOfEq g hX hY
⊢ f = g

Tactic:
subst hX hY

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
f' : X' ⟶ Y'
e : homOfEq f hX hY = f'
⊢ f ≍ f'

Tactic:
subst hX hY

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : homOfEq f ⋯ ⋯ = f'
⊢ f ≍ f'
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
⊢ homOfEq f hX hY = g ↔ f = homOfEq g ⋯ ⋯

Tactic:
subst hX hY

Goal state after:
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ = g ↔ f = homOfEq g ⋯ ⋯
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f = homOfEq g hX hY ↔ homOfEq f ⋯ ⋯ = g

Tactic:
subst hX hY

Goal state after:
V : Type u_1
inst✝ : Quiver V
X' Y' : V
g f : X' ⟶ Y'
⊢ f = homOfEq g ⋯ ⋯ ↔ homOfEq f ⋯ ⋯ = g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
h : diag x = diag y
⊢ x = y

Tactic:
by
  cases Sym2.exact h <;> rfl

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

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

Tactic:
rw [h₁, h₂]
          first | done | constructor

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

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

Tactic:
rw [h₁, h₂]
          first | done | constructor

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

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
X' Y' : U
hX : X = X'
hY : Y = Y'
⊢ F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
subst hX hY

Goal state after:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]
    dsimp
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
eq1 : X = X'
eq2 : Y = Y'
eq3 : Z = Z'
H1 : f ≍ f'
H2 : g ≍ g'
⊢ f ≫ g ≍ f' ≫ g'

Tactic:
by
  congr!

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

Goal state before:
pp: case mpr
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾f)

Tactic:
refine fun H => ⟨fun g g' h =>  ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.injective_comp_right ?_) x⟩
    ext y
    exact ConcreteCategory.congr_hom h y

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

Tactic:
exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (MorphismProperty.isomorphisms C).RespectsIso

Tactic:
apply RespectsIso.mk <;>
    · intro X Y Z e f
      simp only [isomorphisms.iff]
      intro
      exact IsIso.comp_isIso

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ α.hom ≫ f ≫ 𝟙 Y₁ = f

Tactic:
α.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ f ≫ 𝟙 Y₁ = f
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ fst) ≫ f = (i₂ ≫ fst) ≫ f

Tactic:
simpa using congr_arg (fun f => f ≫ prod.fst) h

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
e : f ≅ g
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left

Tactic:
by
  simp [← Over.comp_left]

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
e : f ≅ g
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left

Tactic:
by
  simp [← Over.comp_left]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ f = 0

Tactic:
by
  rw [← zero_comp, cancel_mono] at h
  exact h

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)
  apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
  refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ 0 ≫ Fork.ι (KernelFork.ofι 0 ⋯) = s.ι

Tactic:
rw [hf _ _ (KernelFork.condition s), zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ (F.mapBiproduct f).hom ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = F.map (desc g)

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ F.map (desc g) = F.map (desc g)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (F.mapBiprod X Y).hom ≫ (F.mapBiprod X Y).inv ≫ F.map (desc f g) = F.map (desc f g)

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ F.map (desc f g) = F.map (desc f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
m : c.pt ⟶ Z'✝
hm : (e.hom ≫ Cofork.π c) ≫ m = s
⊢ Cofork.π c ≫ m = Cofork.π c ≫ hc.desc (ofπ (e.inv ≫ s) ⋯)

Tactic:
by simpa [← cancel_epi e.hom] using hm

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁶ : Category.{uC', uC} C
inst✝⁵ : HasZeroMorphisms C
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
P Q : C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ F.map (X✝.inr ≫ F.preimage t.hom) = F.map Y✝.inr

Tactic:
simpa using! t.winr

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

Goal state before:
pp: case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ map' f g) ≫ fst

Tactic:
simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_left]

Goal state after:
case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫ f =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }