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 ι
ih : (i : ι) → F₁ i → F₂ i
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)
z : DirectLimit F₁ f₁
j k : ι
h : j ≤ k
x : F₁ j
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f₂ j i hji) (ih j x) = (f₂ k i hki) (ih k ((f₁ j k h) x))

Tactic:
compat,

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 ι
ih : (i : ι) → F₁ i → F₂ i
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)
z : DirectLimit F₁ f₁
j k : ι
h : j ≤ k
x : F₁ j
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) x) = ih i ((f₁ k i hki) ((f₁ j k h) x))
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
⊢ ↑(lift₂Aux f₁ f₂ ih compat x✝⁵ x✝⁴) = ↑(lift₂Aux f₁ f₂ ih compat x✝³ x✝²)

Tactic:
by
      have ⟨i, hji, hki⟩ := exists_ge_ge j k
      simp_rw [(lift₂Aux ..).2 _ (hx.trans hji) (hyk.trans hki),
        (lift₂Aux ..).2 _ (hyj.trans hji) (hz.trans hki),
        ← map_map' _ hx hji, jeq, ← map_map' _ hz hki, ← keq, map_map']

Goal state after:
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 ι
ih : (i : ι) → F₁ i → F₂ i → F i
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)
j k : ι
h : j ≤ k
x : F₁ j
y : F₂ j
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) (ih j x y) = (f k i hki) (ih k ((f₁ j k h) x) ((f₂ j k h) y))

Tactic:
compat,

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 ι
ih : (i : ι) → F₁ i → F₂ i → F i
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)
j k : ι
h : j ≤ k
x : F₁ j
y : F₂ j
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) x) ((f₂ j i hji) y) = ih i ((f₁ k i hki) ((f₁ j k h) x)) ((f₂ k i hki) ((f₂ j k h) y))
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
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : 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
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (fun l ↦ (equiv l) (↑t l)) x✝¹ = piLTProj h ((fun l ↦ (equiv l) (↑t l)) x✝)

Tactic:
simp_rw [← t.2 h]; apply nat

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)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g : (i : ι) → G i →+ 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)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → G i ≃+ G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i j : ι
h : i ≤ j
x : G' i
eq1 : ((e j).toAddMonoidHom.comp (f i j h)) ((e i).symm x) = ((f' i j h).comp ↑(e i)) ((e i).symm x)
⊢ ((↑(e j).symm).comp (f' i j h)) x = ((f i j h).comp ↑(e i).symm) x

Tactic:
simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, Function.comp_apply,
        AddMonoidHom.coe_coe, AddEquiv.apply_symm_apply] at eq1 ⊢

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g : (i : ι) → G i →+ 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)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → G i ≃+ G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i j : ι
h : i ≤ j
x : G' i
eq1 : (e j) ((f i j h) ((e i).symm x)) = (f' i j h) x
⊢ (e j).symm ((f' i j h) x) = (f i j h) ((e i).symm x)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M ι ∘ₗ lTensor M π)

Tactic:
exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
i : ι
x✝ : i ∈ t
hn : i ∉ s
⊢ g i ((↑s).mulIndicator f i) = 1

Tactic:
by simp [hn, hg]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ {i ∈ t | q i}, f i = g i

Tactic:
by simpa using h

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ (↑(Fintype.card ι))⁻¹ • ∑ j, (if i = j then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
ite_mul,

Goal state after:
ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ ((↑(Fintype.card ι))⁻¹ • ∑ x, if i = x then ↑(Fintype.card ι) * f x else 0 * f x) = f i
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
by simpa using h

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [MOD n]

Tactic:
aesop (add unsafe ModEq.add)

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [MOD n]

Tactic:
aesop (add unsafe ModEq.add)

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 <;> assumption

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

Goal state before:
pp: case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]

Tactic:
aesop (add unsafe ModEq.add)

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

Goal state before:
pp: case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [ZMOD n]

Tactic:
aesop (add unsafe ModEq.add)

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 <;> assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
      ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩) =
    ⟨i, ⟨m, hm⟩⟩

Tactic:
refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_
    · exact fun i ↦ Sym α (n - i)
    swap
    · exact Subtype.coe_injective
    refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)
    exacts [rfl, h ∘ mem_sym_iff.1 hm a]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ ∀ (Q : Type (max v₁ v₂ u_1)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module R Q]
    [inst_3 : IsScalarTower R R Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑e = g

Tactic:
intro Q I₁ I₂ I₃ I₄ g

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ ↑e = g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toFinset ↔ x ∈ z

Tactic:
by
  rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]

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

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f

Tactic:
apply h.inv'

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

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f

Tactic:
apply h.inv'

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ F.map ((L.objObjPreimageIso X✝).hom ≫ a₁✝ ≫ (L.objObjPreimageIso Y✝).inv) =
    F.map ((L.objObjPreimageIso X✝).hom ≫ a₂✝ ≫ (L.objObjPreimageIso Y✝).inv)

Tactic:
simp [hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
α.hom_inv_id_app

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
h₁ : f.left = g.left
h₂ : f.right = g.right
h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom ⋯
⊢ ∃ hX hY, f.hom = eqToHom hX ≫ g.hom ≫ eqToHom ⋯

Tactic:
by simp_all

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ p.unop ≫ l.l.unop = g.unop

Tactic:
rw [← unop_comp, l.fac_right]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f

Tactic:
by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h

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

Goal state before:
pp: X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y

Tactic:
by simp_all

Goal state after:
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 : Cone F
ht : ∀ (s : Cone F), ∃! l, ∀ (j : J), l ≫ t.π.app j = s.π.app j
⊢ IsLimit t

Tactic:
choose s hs hs' using ht

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 : Cone F
s : (s : Cone F) → s.pt ⟶ t.pt
hs : ∀ (s_1 : Cone F), (fun l ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) (s s_1)
hs' : ∀ (s_1 : Cone F) (y : s_1.pt ⟶ t.pt), (fun l ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) y → y = s s_1
⊢ IsLimit t
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
t : Cone F
h : IsLimit t
W : C
f : (const J).obj W ⟶ F
j : J
⊢ h.homEquiv.symm f ≫ t.π.app j = f.app j

Tactic:
by
  simp [homEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : coyoneda.obj (op X) ⟶ F
⊢ (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
      ((fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)) η) =
    η

Tactic:
ext Y (x : X ⟶ Y)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : coyoneda.obj (op X) ⟶ F
Y : C
x : X ⟶ Y
⊢ (ConcreteCategory.hom
          (((fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
                ((fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)) η)).app
            Y)).toFun
      x =
    (ConcreteCategory.hom (η.app Y)).toFun x
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ f = f'

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
this : Arrow.mk (F.map f) = Arrow.mk (G.map f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: 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
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]

Goal state after:
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
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape J C

Tactic:
have := HasLimitsOfSize.has_limits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
  exact hasLimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

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

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

Tactic:
exact
      ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
          (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
          (IsIso.eq_inv_comp _).mpr e⟩

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✝ : Over X
φ : f✝ ⟶ g✝
U V W : Over X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ (f ≫ g) ≫ W.hom = U.hom

Tactic:
by simp_all

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)

Tactic:
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi f
⊢ Epi (image.ι f)

Tactic:
← image.fac f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi f

Tactic:
← image.fac f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'

Tactic:
by
  apply image.ext
  subst h
  simp [asIso, image.eqToIso, image.eqToHom]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e.symm ≫ ↟↑e = 𝟙 (of R X₂)

Tactic:
ext; apply e.right_inv

Goal state after: