mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)

Tactic:
simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
by
  by_cases H : x = 0
  · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
  · classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p

Tactic:
have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 ↦ absurd hp1 (by simp [hp0]))
  exact (normalize_associated _).prime this

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ IsCoprime (X - C a) (f /ₘ (X - C a))

Tactic:
refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
⊢ p₁ % q = p₂ % q

Tactic:
by
  obtain rfl | hq := eq_or_ne q 0
  · simpa [sub_eq_zero] using h
  simp_rw [Polynomial.mod_def]
  apply Polynomial.modByMonic_eq_of_dvd_sub (by simp [Polynomial.Monic.def, hq])
  rw [mul_comm]
  exact (Polynomial.C_mul_dvd (by simpa using hq)).mpr h

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 ι
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 : (i : ι) × F₁ i
w : (i : ι) × F₂ i
j : ι
hzj : z.fst ≤ j
hwj : w.fst ≤ j
k : ι
hzk : z.fst ≤ k
hwk : w.fst ≤ k
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih j ((f₁ z.fst j hzj) z.snd) ((f₂ w.fst j hwj) w.snd) = ih k ((f₁ z.fst k hzk) z.snd) ((f₂ w.fst k hwk) w.snd)

Tactic:
simp_rw [compat _ _ hji, compat _ _ hki, map_map']

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
g₁ : (i : ι) → G i →+ G' i
g₂ : (i : ι) → G' i →+ G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
← AddMonoidHom.comp_assoc,

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
g₁ : (i : ι) → G i →+ G' i
g₂ : (i : ι) → G' i →+ G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ ((g₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict).range = (lTensor Q g.range.subtype).range

Tactic:
apply range_comp_of_range_eq_top

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (lTensor Q g.rangeRestrict).range = ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (rTensor Q g.range.subtype ∘ₗ rTensor Q g.rangeRestrict).range = (rTensor Q g.range.subtype).range

Tactic:
apply range_comp_of_range_eq_top

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (rTensor Q g.rangeRestrict).range = ⊤
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : Monoid C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
n : ℕ
i : ι
x : G i
⊢ (g i) (x ^ n) = (g i) x ^ n

Tactic:
map_pow (g i)

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₁
inst✝ : Module.Flat R N₂
⊢ Function.Injective ⇑(hf.map hg i₁ i₂)

Tactic:
by
  have h : hf.map hg i₁ i₂ = hg.equiv ∘ TensorProduct.map i₁ i₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using map_injective_of_flat_flat' i₁ i₂ h₁ h₂

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧ * ⟦⟨i, x✝⟩⟧ = 1

Tactic:
by
    simp_rw [map_def, mul_def, inv_mul_cancel, one_def i]

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
⊢ ((F.orderEmbOfFin h) ⟨j - 1, ⋯⟩).2 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
intervalGapsWithin_snd_of_lt (hj := by omega)

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
⊢ ((F.orderEmbOfFin h) ⟨j - 1, ⋯⟩).2 ≤ ((F.orderEmbOfFin h) ⟨j, ⋯⟩).1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℤ → α
l u : ℤ
h : l ≤ u
⊢ ∏ m ∈ Icc l u, f m = (∏ m ∈ Ico l u, f m) * f u

Tactic:
simp [Icc_eq_cons_Ico h, mul_comm]

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.orderEmbOfFin h) ⟨j, ⋯⟩).1 ≤ (F.intervalGapsWithin h a b ↑(j' - 1)).2

Tactic:
intervalGapsWithin_snd_of_lt (hj := by omega)

Goal state after:
α : 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.orderEmbOfFin h) ⟨j, ⋯⟩).1 ≤ ((F.orderEmbOfFin h) ⟨j' - 1, ⋯⟩).1
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : a = x ∧ b = x ∨ a = x ∧ b = x
⊢ a = x ∨ a ∈ xs

Tactic:
← and_or_left

Goal state after:
case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs

Tactic:
by
  induction xs with
  | nil => simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]
  | cons x xs ih =>
    rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ [] ++ List.sym (n + 1) xs <+ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝

Tactic:
apply Sublist.append (nil_sublist _)

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) l₂✝
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)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ ↑e = g

Tactic:
have : I₂ = I₃ := by
    ext r q
    change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
    dsimp
    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]

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
this : I₂ = I₃
⊢ ∃! 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.toMultiset

Tactic:
Sym2.toFinset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset.toFinset ↔ x ∈ z.toMultiset
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ inv f ≫ f = inv f ≫ g

Tactic:
inv_hom_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ 𝟙 Y = inv f ≫ g
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.length ≠ 0 ↔ ∃ c p' e, p = p'.cons e

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · cases p with
    | nil => simp at h
    | cons p' e => exact ⟨_, p', e, rfl⟩
  · rintro ⟨c, p', e, rfl⟩
    simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y

Tactic:
e.hom.naturality f,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
subst h
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟙 (unop Y✝) ≫ f.unop).op = f

Tactic:
id_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.op = f
Module: Mathlib.CategoryTheory.Types.Basic

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

Tactic:
constructor
  · rintro ⟨H⟩
    refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_
    rw [← Equiv.ulift.{u}.symm.injective.comp_left.eq_iff]
    apply TypeCat.homEquiv.symm.injective
    apply H
    apply ConcreteCategory.hom_ext
    intro x
    simp [dsimp% congrFun hg x]
  · 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.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| f ≫ (e Y✝ (F_obj Z✝)) (𝟙 (F_obj Y✝) ≫ (e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))

Tactic:
id_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| f ≫ (e Y✝ (F_obj Z✝)) ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X✝ : C
Y✝ : D
f✝ : X' ⟶ X✝
g✝ : X✝ ⟶ G.obj Y✝
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g

Tactic:
rw [Equiv.symm_apply_eq, he]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X✝ : C
Y✝ : D
f✝ : X' ⟶ X✝
g✝ : X✝ ⟶ G.obj Y✝
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (e X Y) ((e X Y).symm f) ≫ G.map g
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)

Tactic:
inv_hom_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ 𝟙 h = 𝟙 (f ≫ h)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ (η.inv ≫ η.hom) ▷ h = 𝟙 (g ≫ h)

Tactic:
inv_hom_id,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ 𝟙 g ▷ h = 𝟙 (g ≫ h)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Basic

Goal state before:
pp: case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom ⋯ ▷ h = eqToHom ⋯

Tactic:
simp only [id_whiskerRight, eqToHom_refl]

Goal state after:
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
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i

Tactic:
by rw [← sq.w_assoc, Category.assoc, RetractArrow.i_w]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f

Tactic:
hI.hom_ext f (hI.to X)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (c.π.app X)

Tactic:
change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j) ∧
    colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
refine ⟨?_, by ext; simp⟩
    simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
      Functor.const_obj_obj, IsInitial.to_self]
    grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ X✝.coprodObj.map k ≫ homMk (coprod.map (Hom.left k✝) (𝟙 g.left)) ⋯ =
    homMk (coprod.map (Hom.left k✝) (𝟙 f.left)) ⋯ ≫ Y✝.coprodObj.map k

Tactic:
ext
        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
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj f = f

Tactic:
rw [eq_mk f]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l

Tactic:
h₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ (span f g).map fst ≫ t.inl ≫ l = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
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 : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj f = f

Tactic:
rw [eq_mk f]
  simp

Goal state after: