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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Tactic:
rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]
  refine ⟨fun h ↦ ⟨h 0 (by simp), h 1 (by simp)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩
  obtain (_ | _ | m) := m
  exacts [h0, h1, by lia]

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

Goal state before:
pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ q.roots = 0

Tactic:
replace he := congr_arg roots he.symm

Goal state after:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).roots = p.roots
⊢ q.roots = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < q.degree

Tactic:
rw [← degree_mul_leadingCoeff_inv q hq]

Goal state after:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p.degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq0]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
x : R
⊢ ¬Irreducible (C x)

Tactic:
by_cases H : x = 0
  · rw [H, C_0]
    exact not_irreducible_zero
  · exact fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a

Tactic:
simp_rw [Transcendental, isAlgebraic_algebraMap_iff h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
obtain ⟨p, hp0, hp⟩ := hRs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ ⟨(aeval s) r, ht⟩ ∈ (aeval ⟨s, ⋯⟩).range

Tactic:
exact ⟨r, by ext; simp⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
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 → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : DirectLimit.lift f ih compat ⟦⟨i, x⟩⟧ = DirectLimit.lift f ih compat ⟦⟨i, y⟩⟧
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧

Tactic:
simp_rw [lift_def] at eq; rw [h i eq]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
hN : N.FG
x y : ↥N ⊗[R] M
eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
by
  lift N to {N : Submodule R P // N.FG} using hN
  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
  apply_fun directLimitLeft _ _ at eq
  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
  exact ⟨_, N'.2, le, eq⟩

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
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i j : ι
h : i ≤ j
⊢ (f'' i j h ∘ₗ g₂ i) ∘ₗ g₁ i = f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i

Tactic:
LinearMap.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)
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
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i j : ι
h : i ≤ j
⊢ f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i = f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i
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
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ∀ (x : F j),
    ((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨k, hk⟩) (f h x) =
      piLTProj h (((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨j, hj⟩) x)

Tactic:
rw [piLTLim_symm_apply]

Goal state after:
ι✝ : 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
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ∀ (x : F j),
    (↑⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ?k ⟨↑⟨k, hk⟩, ?hl⟩) (f h x) =
      piLTProj h (((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨j, hj⟩) x)

case k
ι✝ : 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
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ↑(Iio i)

case hl
ι✝ : 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
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ↑⟨k, hk⟩ < ↑?k
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
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
inst✝ : InverseSystem f
equivLim : F i ≃ ↑(limit f i)
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
i✝ : ι
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i✝
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [piEquivLim, piSplitLE_lt (hi.succ_lt <| (succ_le_iff_of_not_isMax hj).mp hsj)]
    apply (pEquivOnGlue hi e).compat

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
P : Submodule R M
hP : P.FG
⊢ Small.{u, u_2} ↥P

Tactic:
fg_iff_exists_fin_generating_family

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
P : Submodule R M
hP : ∃ n s, span R (Set.range s) = P
⊢ Small.{u, u_2} ↥P
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case zero
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (0 • s) = restrictSupport R s ^ 0

Tactic:
simp [add_smul, restrictSupport_add, *, pow_succ]

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

Goal state before:
pp: case succ
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
n✝ : ℕ
a✝ : restrictSupport R (n✝ • s) = restrictSupport R s ^ n✝
⊢ restrictSupport R ((n✝ + 1) • s) = restrictSupport R s ^ (n✝ + 1)

Tactic:
simp [add_smul, restrictSupport_add, *, pow_succ]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective ⇑(Finsupp.linearCombination S fun x ↦ 1 ⊗ₜ[R] v x)

Tactic:
← LinearMap.coe_restrictScalars R,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective ⇑(↑R (Finsupp.linearCombination S fun x ↦ 1 ⊗ₜ[R] v x))
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s : Finset α
inst✝ : Nonempty α
⊢ s.dens = 1 ↔ s = univ

Tactic:
by
  simp [dens, div_eq_one_iff_eq, card_eq_iff_eq_univ]

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 ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)

Tactic:
calc
    _ = ∏ i ∈ s, g i (mulIndicator ↑s f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
    _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst✝ : DecidableEq ι
m : κ → ι
hm : Set.InjOn m ↑t
⊢ 𝔼 i ∈ image m t, f i = 𝔼 i ∈ t, f (m i)

Tactic:
simp_rw [expect, card_image_of_injOn hm, sum_image hm]

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

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n = 0 + n % a + a * (n / a)

Tactic:
by simp [hn]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t

Tactic:
simpa using congr(s(x, x) ∈ $h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
⊢ fromRel ⋯ = map f '' fromRel hr

Tactic:
ext ⟨a, b⟩
  simp only [fromRel_prop, Relation.Map, Set.mem_image, Sym2.exists, map_mk, Sym2.eq,
    rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, and_or_left, exists_or, iff_self_or,
    forall_exists_index, and_imp]
  exact fun c d hcd hc hd ↦ ⟨d, c, symm hcd, hd, hc⟩

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

Goal state before:
pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

pp: case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

Tactic:
· exfalso
          simp at hy

Goal state after:
case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z ↔ X = Z ∨ Y = Z

Tactic:
by
  constructor
  · rintro ⟨_ | _⟩ <;> tauto
  · rintro (rfl | rfl); exacts [⟨Sum.inl .unit⟩, ⟨Sum.inr .unit⟩]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝

Tactic:
← NatIso.naturality_1 α.symm,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ α.symm.inv.app X✝ ≫ F'.map a₁✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a x✝ b✝ : V
p : Path a b✝
a✝ : b✝ ⟶ x✝
⊢ (nil.comp p).cons a✝ = p.cons a✝

Tactic:
nil_comp p

Goal state after:
V : Type u
inst✝ : Quiver V
a x✝ b✝ : V
p : Path a b✝
a✝ : b✝ ⟶ x✝
⊢ p.cons a✝ = p.cons a✝
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
rintro ⟨rfl, rfl⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (((e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))) ≫
            e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 3 4 => rw [e.unitInv_naturality]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        ((e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Opposites

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

Tactic:
← op_comp_unop,

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

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

Tactic:
← op_comp_unop,

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f = f'

Tactic:
apply Functor.ext; rotate_left
  · intro X
    ext i
    specialize h i
    have := congr_obj h X
    simpa
  · intro X Y g
    funext i
    specialize h i
    have := congr_hom h g
    simpa

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

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

Tactic:
refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩

Goal state after:
case mpr
X Y : Type u
f : X → Y
H : Function.Injective f
Z✝ : Type u
g g' : Z✝ ⟶ X
h : g ≫ ↾f = g' ≫ ↾f
x : Z✝
⊢ (fun x ↦ f ∘ x) ⇑(ConcreteCategory.hom g) = (fun x ↦ f ∘ x) ⇑(ConcreteCategory.hom g')
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f

Tactic:
let e : X ≃+* Y := { ff, i.toEquiv with }

Goal state after:
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f

Tactic:
let e : X ≃+* Y := { ff, i.toEquiv with }

Goal state after:
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f

Tactic:
let e : X ≃+* Y := { ff, i.toEquiv with }

Goal state after:
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
⊢ IsIso f

Tactic:
let e : X ≃+* Y := { ff, i.toEquiv with }

Goal state after:
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := Hom.hom f
e : ↑X ≃+* ↑Y :=
  let __src := i.toEquiv;
  { toFun := (↑↑ff).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f
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
ι : F ⟶ (const J).obj W
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (fun j ↦ ι.app j) j' = (fun j ↦ ι.app j) j

Tactic:
convert! ← ι.naturality f

Goal state after:
case e'_3
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
ι : F ⟶ (const J).obj W
j j' : J
f : j ⟶ j'
e_1✝ : (F.obj j ⟶ ((const J).obj W).obj j') = (F.obj j ⟶ W)
⊢ ι.app j ≫ ((const J).obj W).map f = (fun j ↦ ι.app j) j
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
⊢ Function.RightInverse
    (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) fun η ↦
    (ConcreteCategory.hom (η.app (op X))) (𝟙 X)

Tactic:
intro ξ

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
ξ : F.obj (op X)
⊢ (fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X))
      ((fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) ξ) =
    ξ