mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ Rel Associated (factors (x * y)) (factors x + factors y)

Tactic:
refine
    factors_unique irreducible_of_factor
      (fun a ha =>
        (mem_add.mp ha).by_cases (irreducible_of_factor _) (irreducible_of_factor _))
      ((factors_prod (mul_ne_zero hx hy)).trans ?_)
  rw [prod_add]
  exact (Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
rw [pow_succ', succ_nsmul']
      refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_
      refine Rel.add ?_ <| factors_pow n
      exact rel_refl_of_refl_on fun y _ => Associated.refl _

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

Goal state before:
pp: case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ 0 ∈ q

Tactic:
rw [← prod_eq_zero_iff, eqc, hc, mul_zero]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Tactic:
← content_eq_zero_iff

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.inl
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
⊢ IsUnit q

Tactic:
have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
        contradiction

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝ : a ∈ p.roots.toFinset
⊢ map (algebraMap R (FractionRing R)) ((X - C a) ^ rootMultiplicity a p) ∣ map (algebraMap R (FractionRing R)) p

Tactic:
exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)

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

Goal state before:
pp: case right.inr.left
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
⊢ p.roots.card + q.natDegree = ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).natDegree

Tactic:
(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,

Goal state after:
case right.inr.left
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
⊢ p.roots.card + q.natDegree = (Multiset.map (fun a ↦ X - C a) p.roots).prod.natDegree + q.natDegree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
this : ↑(normUnit X) = C ↑(normUnit X.leadingCoeff)
⊢ normUnit X = 1

Tactic:
rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
⊢ ∀ (a : R[X]), a / 0 = 0

Tactic:
by simp [div_def]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1

Tactic:
contrapose hpu
    exact .of_mul_eq_one _ hpu

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors

Tactic:
rcases count_of_coprime ha hb hab hp with hz | hb0

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors

case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
p : R[X]
inst✝² : DecidableEq R
inst✝¹ : Field S
inst✝ : DecidableEq S
f : R →+* S
⊢ map f (normalize p) = normalize (map f p)

Tactic:
by
  by_cases hp : p = 0
  · simp [hp]
  · simp [normalize_apply, Polynomial.map_mul, normUnit, hp]

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    p.coeff 0 = 0 → a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
· intro p a hp ha _ih _ne_zero aeval_eq
    refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
    rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]

Goal state after:
case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
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, ih j x⟩.fst i hji) ⟨j, ih j x⟩.snd = (f₂ ⟨k, ih k ((f₁ j k h) x)⟩.fst i hki) ⟨k, ih k ((f₁ j k h) x)⟩.snd

Tactic:
simp_rw [compat, 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, ih j x y⟩.fst i hji) ⟨j, ih j x y⟩.snd =
    (f ⟨k, ih k ((f₁ j k h) x) ((f₂ j k h) y)⟩.fst i hki) ⟨k, ih k ((f₁ j k h) x) ((f₂ j k h) y)⟩.snd

Tactic:
simp_rw [compat, map_map']

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ q ⊗ₜ[R] h (p + p') - (q ⊗ₜ[R] h p + q ⊗ₜ[R] h p') ∈ (lTensor Q f).range

Tactic:
← TensorProduct.tmul_add,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ q ⊗ₜ[R] h (p + p') - q ⊗ₜ[R] (h p + h p') ∈ (lTensor Q f).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
⊢ 0 ∈ ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
apply zero_mem

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
⊢ 0 ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
apply zero_mem

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}
  have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
  simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]

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

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
⊢ map₀ f 1 = 1

Tactic:
map₀,

Goal state after:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
⊢ ⟦⟨Classical.arbitrary ι, 1 (Classical.arbitrary ι)⟩⟧ = 1
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : (i : ι) → Mul (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
r s : (i : ι) → G i
⊢ map₀ f (r * s) = map₀ f r * map₀ f s

Tactic:
map₀,

Goal state after:
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : (i : ι) → Mul (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
r s : (i : ι) → G i
⊢ ⟦⟨Classical.arbitrary ι, (r * s) (Classical.arbitrary ι)⟩⟧ =
    ⟦⟨Classical.arbitrary ι, r (Classical.arbitrary ι)⟩⟧ * ⟦⟨Classical.arbitrary ι, s (Classical.arbitrary ι)⟩⟧
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_4
inst✝² : Fintype α
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens

Tactic:
rw [← dens_union_of_disjoint (disjoint_filter_filter_not ..), filter_union_filter_not_eq]

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 : α
j : ℕ
hj : j ∈ Iio k
j' : ℕ
hj' : j' ∈ Iio k
hjj' :
  (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j'
⊢ j = j'

Tactic:
rw [mem_Iio] at hj hj'

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
j' : ℕ
hj' : j' < k
hjj' :
  (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j'
⊢ j = j'
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ f r = 0 r

Tactic:
rw [Pi.zero_apply, ← neg_eq_self, ← ho, he]

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 ∈ Iio (k + 1)
j' : ℕ
hj' : j' ∈ Iio (k + 1)
hjj' : j ≠ j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'

Tactic:
rw [mem_Iio] at hj hj'

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'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ x ∈ Ico 0 n, f x • g x =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x

Tactic:
rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ Ico 0 (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b c✝
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂

Tactic:
| cons q₁ f₁ ih =>

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: 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 : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
X : C
⊢ a₁✝.app X = a₂✝.app X

Tactic:
exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

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.counit.app Y) = 𝟙 (e.inverse.obj Y)

Tactic:
rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
  rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom,
    Iso.app_inv]
  slice_lhs 2 3 => rw [← e.unit_naturality]
  slice_lhs 1 2 => rw [← e.unit_naturality]
  slice_lhs 4 4 =>
    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
  slice_lhs 3 4 =>
    dsimp only [Functor.mapIso_hom, Iso.app_hom]
    rw [← map_comp e.inverse]
    dsimp
    rw [e.counit_naturality, e.counitIso.hom_inv_id_app]
    dsimp only [Functor.comp_obj]
    rw [map_id]
  dsimp only [comp_obj, id_obj]
  rw [id_comp]
  slice_lhs 2 3 =>
    dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]
  slice_lhs 3 4 => rw [e.unitInv_naturality]
  slice_lhs 4 5 =>
    rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]
  rw [id_comp]
  slice_lhs 3 4 => rw [← e.unitInv_naturality]
  slice_lhs 2 3 =>
    rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]
  simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : P f
⊢ ofHoms P.homFamily f

Tactic:
exact ⟨(⟨f, hf⟩ : P.toSet)⟩

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
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)

Tactic:
simp only [Equiv.symm_apply_apply, homEquiv_naturality_left_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ IsIso f ↔ a = b

Tactic:
by
  constructor
  · intro _
    exact (asIso f).to_eq
  · rintro rfl
    rw [Subsingleton.elim f (𝟙 _)]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = (ConcreteCategory.hom (f.app (op Y))) g

Tactic:
by
  rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ Skeletal (Skeleton C)

Tactic:
by
  rintro X Y ⟨h⟩
  have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
  simpa using! Quotient.sound this

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v', u'} D → EssentiallySmall.{w, v, u} C

Tactic:
· rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.trans f)

Goal state after:
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 : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.hom ≫ Y✝.π.app j) = G.map (X✝.π.app j)

Tactic:
by simpa using t.w j

Goal state after:
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
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)

Tactic:
constructor <;> intro <;> constructor <;> intro f g sq

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
⊢ sq.HasLift

case mpr
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 i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift
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:
← 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.Functor.EpiMono

Goal state before:
pp: 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 : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
s : SplitEpi (F.map f)
⊢ F.preimage s.section_ ≫ f = 𝟙 Y

Tactic:
apply F.map_injective
    simp only [map_comp, map_preimage, map_id]
    apply SplitEpi.id

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ (Iso.refl
          ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))).pt).hom ≫
      s.base =
    base
      ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))

Tactic:
simp [base, reindex, mk]

Goal state after: