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

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) ((f x✝².fst j hx) x✝².snd) = (f z✝.fst i ⋯) z✝.snd

Tactic:
← map_map' _ hz hki,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) ((f x✝².fst j hx) x✝².snd) = (f k i hki) ((f z✝.fst k hz) z✝.snd)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝³.fst j hyj) x✝³.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ x✝².fst i ⋯) x✝².snd)

Tactic:
← map_map' _ hz hki,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝³.fst j hyj) x✝³.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ k i hki) ((f₂ x✝².fst k hz) x✝².snd))
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i ↦ G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x + (f j k hjk) y) = Quotient.mk'' (p + q)

Tactic:
by
          rw [map_add, of_f, of_f, ihx, ihy]
          rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
inst✝⁸ : (i : ι) → AddCommMonoid (G i)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ LinearMap.id

Tactic:
comp_id

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
inst✝⁸ : (i : ι) → AddCommMonoid (G i)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ LinearMap.id

Tactic:
comp_id

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x y : G i
this : Nonempty ι
h✝ : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
j : ι
h : ∃ (hx : ⟨i, x⟩.fst ≤ j) (hy : ⟨i, y⟩.fst ≤ j), (f ⟨i, x⟩.fst j hx) ⟨i, x⟩.snd = (f ⟨i, y⟩.fst j hy) ⟨i, y⟩.snd
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
exact ⟨j, h.1, h.2.2⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ (globalEquiv equivSucc equivLim i) (f h x) = piLTProj h ((globalEquiv equivSucc equivLim j) x)

Tactic:
refine (DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)
  exact pEquivOn_apply_eq ((isLowerSet_Iic _).inter <| isLowerSet_Iic _)

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
a✝ : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
exact eq_of_smul_eq_smul

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 : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
· have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
    grind

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

Goal state before:
pp: case pos
α : 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 : 0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2

Tactic:
simp only [natCast_zero, intervalGapsWithin_zero_fst]
      simp [show 0 = last k by grind, hab]

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

Goal state before:
pp: case cons.inl
α : 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 ++ xs.sym2).dedup = xs.sym2.dedup

pp: case cons.inl
α : 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.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset

Goal state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ xs.sym2.dedup = xs.sym2.dedup

case cons.inl
α : 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

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = Quot.mk (Rel α) ((Quot.out e).1, (Quot.out e).2)

Tactic:
e.out_eq

Goal state after:
α : Type u_1
e : Sym2 α
⊢ e = e
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ diagSet ⊆ fromRel hr ↔ Std.Refl r

Tactic:
by
  simp [Set.subset_def, Sym2.forall, refl_def]

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
f : X ⟶ Z
g : Y ⟶ Z
H : f = α.hom ≫ g
⊢ α.inv ≫ f = g

Tactic:
simp [H]

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
f : Z ⟶ Y
g : Z ⟶ X
H : f = g ≫ α.hom
⊢ f ≫ α.inv = g

Tactic:
simp [H]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
comp_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ f = α.inv ↔ f = α.inv
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_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF h₁ h₂ : F.FullyFaithful
this : F.Faithful
⊢ h₁ = h₂

Tactic:
cases h₁ with

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

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rintro X Y f
    simp only [Prefunctor.comp_map]
    apply eq_of_heq
    iterate 2 apply (cast_heq _ _).trans
    simp

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p

Tactic:
simp [H]

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p

Tactic:
simp [H]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
Z : C
hZ : P Z
f : X ≅ Z
⊢ P.isoClosure Y

Tactic:
exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom ≫ 𝟙 (R'.obj X.right)

Tactic:
comp_id

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom = L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑p j' = ↑p j ≫ 𝟙 W

Tactic:
comp_id

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 a ◁ (λ_ f).hom ▷ g = 𝟙 a ◁ (α_ (𝟙 a) f g).hom ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom

Tactic:
← cancel_epi (α_ _ _ _).hom,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (𝟙 a) (𝟙 a ≫ f) g).hom ≫ 𝟙 a ◁ (λ_ f).hom ▷ g =
    (α_ (𝟙 a) (𝟙 a ≫ f) g).hom ≫ 𝟙 a ◁ (α_ (𝟙 a) f g).hom ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (𝟙 a) (𝟙 a) f).hom ▷ g ≫ (α_ (𝟙 a) (𝟙 a ≫ f) g).hom ≫ 𝟙 a ◁ (λ_ f).hom ▷ g =
    (α_ (𝟙 a) (𝟙 a) f).hom ▷ g ≫ (α_ (𝟙 a) (𝟙 a ≫ f) g).hom ≫ 𝟙 a ◁ (α_ (𝟙 a) f g).hom ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom

Tactic:
pentagon_assoc,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (𝟙 a) (𝟙 a) f).hom ▷ g ≫ (α_ (𝟙 a) (𝟙 a ≫ f) g).hom ≫ 𝟙 a ◁ (λ_ f).hom ▷ g =
    (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (α_ (𝟙 a) (𝟙 a) (f ≫ g)).hom ≫ 𝟙 a ◁ (λ_ (f ≫ g)).hom
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ 𝟙 a ◁ (λ_ (𝟙 a)).hom = 𝟙 a ◁ (ρ_ (𝟙 a)).hom

Tactic:
← cancel_epi (α_ _ _ _).hom,

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
⊢ (α_ (𝟙 a) (𝟙 a) (𝟙 a)).hom ≫ 𝟙 a ◁ (λ_ (𝟙 a)).hom = (α_ (𝟙 a) (𝟙 a) (𝟙 a)).hom ≫ 𝟙 a ◁ (ρ_ (𝟙 a)).hom
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t

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

Goal state before:
pp: X : Type u
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).toCatHom.toFunctor =
    (𝟙 (Cat.of (Discrete X))).toFunctor

Tactic:
simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.id_toFunctor]

Goal state after:
X : Type u
⊢ Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X))) = 𝟭 (Discrete X)
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✝ : J ⥤ C
G F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
K : J ⥤ C
⊢ ∀ {A B : Cone K} (f : A ⟶ B) [IsIso ((functoriality K F).map f)], IsIso f

Tactic:
intro A B f _

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 : Type u₅
inst✝² : Category.{v₅, u₅} E
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift

Tactic:
rw [← sq.left_adjoint_hasLift_iff adj]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
⊢ Mono f

Tactic:
have := t.isSplitMono_from f; infer_instance

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

Goal state before:
pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
m :
  (mk c.pt fun x ↦
        match x with
        | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
x✝¹ : Discrete α
a : α
x✝ : Discrete (β a)
b : β a
⊢ (mk (X a) (π a)).ι.app { as := b } ≫ c.ι.app { as := a } ≫ m =
    (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := b }

Tactic:
simpa using! h ⟨a, b⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)

Tactic:
· rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
    refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
    rw [Category.comp_id]
    have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
    rwa [Category.assoc, Category.id_comp] at e

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
⊢ m = desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)

Tactic:
refine Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_

Goal state after:
case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
i : ι
⊢ c'.inj i ≫ m = c'.inj i ≫ desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ IsIso (pushout.inl f g)

Tactic:
refine ⟨⟨pushout.desc (𝟙 _) (inv g ≫ f) (by simp), by simp, ?_⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)