mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).degree < ↑n ∨ (p * q).natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
natDegree_mul p0 q0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).degree < ↑n ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
⊢ Associates.mk a ⊓ Associates.mk b ≤ Associates.mk a

Tactic:
exact inf_le_left

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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ r.cancelLeads s
⊢ r ∣ s.primPart

Tactic:
cancelLeads,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs :
  r ∣ C r.leadingCoeff * X ^ (r.natDegree - s.natDegree) * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
⊢ r ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors

Tactic:
by
  rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount h₁]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible (C x)
hf : C x = f
hx : x = 0
⊢ False

Tactic:
hx,

Goal state after:
case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible (C 0)
hf : C x = f
hx : x = 0
⊢ False
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
h : IsAlgebraic R x
⊢ IsAlgebraic R ⅟x

Tactic:
obtain ⟨p, hp, hp'⟩ := h
  refine ⟨p.reverse, by simpa using hp, ?_⟩
  rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]

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
⊢ Injective ⇑(lTensor.inverse Q hfg hg)

Tactic:
exact (lTensor.equiv Q hfg hg).symm.injective

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

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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum + (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum

Tactic:
hx,

Goal state after:
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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum + y =
    (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum + (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case h
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
hx,

Goal state after:
case h
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (Sx.sum fun m n ↦ m ⊗ₜ[R] n) + y = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = x ^ nilpotencyClass x

Tactic:
hx,

Goal state after:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = x ^ 1
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (s.disjUnion t h).dens = s.dens + t.dens

Tactic:
dens_disjUnion

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ s.dens + t.dens = s.dens + t.dens
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t ∪ s ∩ t).dens = s.dens

Tactic:
sdiff_union_inter

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ s.dens = s.dens
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 ((↑s).mulIndicator f i)

Tactic:
prod_subset h fun i _ hn ↦ by simp [hn, hg]

Goal state after:
ι : 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) = ∏ x ∈ t, g x ((↑s).mulIndicator f x)
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 ∈ s | p i} = {i ∈ t | q i}

Tactic:
by rw [hst, filter_inj'.2 hpq]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = -(f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, smul_neg]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f * g)

Tactic:
intro a
  simp only [Pi.mul_apply, hf a, hg a, mul_neg]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| ∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i -
    ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i

Tactic:
rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
    ∑ x ∈ Ico m (n - 1), (f x • ∑ i ∈ range (x + 1), g i - f (x + 1) • ∑ i ∈ range (x + 1), g i)
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
        ∑ x ∈ Ico m (n - 1), -((f (x + 1) - f x) • ∑ i ∈ range (x + 1), g i)) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
sum_neg_distrib,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
        -∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • ∑ i ∈ range (x + 1), g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • ∑ i ∈ range (x + 1), g i
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ x y : S ⊗[R] M
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • x) + (IsTensorProduct.equiv h) (r • y) =
    r • (IsTensorProduct.equiv h) x + r • (IsTensorProduct.equiv h) y

Tactic:
hx,

Goal state after:
case refine_3
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ x y : S ⊗[R] M
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ r • (IsTensorProduct.equiv h) x + (IsTensorProduct.equiv h) (r • y) =
    r • (IsTensorProduct.equiv h) x + r • (IsTensorProduct.equiv h) y
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ s(x', x') :: (map (fun y ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
cases h with
    | head =>
      exact (sublist_append_left _ _).cons_cons _
    | tail _ h =>
      refine .cons _ ?_
      rw [← singleton_append]
      refine .append ?_ (ih h)
      rw [singleton_sublist, mem_map]
      exact ⟨_, h, Sym2.eq_swap⟩

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
⊢ IsBaseChange S f

Tactic:
obtain ⟨g, hg, -⟩ :=
    h (ULift.{v₂} <| S ⊗[R] M)
      (ULift.moduleEquiv.symm.toLinearMap.comp <| TensorProduct.mk R S M 1)

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
⊢ IsBaseChange S f
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ f' (s • x) + f' (s • y) = s • f' x + s • f' y

Tactic:
hx,

Goal state after:
case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ s • f' x + f' (s • y) = s • f' x + s • f' y
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ (↑R q' ∘ₗ ↑R h) ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f

Tactic:
show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq',

Goal state after:
case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ ↑R r ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f
Module: Mathlib.Combinatorics.Quiver.Push

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

Tactic:
simp only [Prefunctor.comp_map]

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) = ⋯ ▸ ⋯ ▸ φ.map f
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X

Tactic:
Φ₀

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ τ X = τ X
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn ⋯
      (Eq.recOn ⋯
        ({ obj := Φ.obj,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ Φ.obj X ⟶ Φ.obj Y) fun X Y f ↦
                  ⋯.mpr (⋯.mpr ((of σ ⋙q Φ).map f)) }.map
          (PushQuiver.arrow f✝)))

Tactic:
simp only [Prefunctor.comp_map]

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) = ⋯.mpr (⋯.mpr (Φ.map ((of σ).map f✝)))
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f = g ≫ eqToHom ⋯
⊢ f ≫ eqToHom p = g

Tactic:
simp [eq_whisker h (eqToHom p)]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

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

Tactic:
simp only [op_comp, Category.assoc]

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ (f.hom ≫ f.inv) i = 𝟙 (X i)

Tactic:
Iso.hom_inv_id,

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 X i = 𝟙 (X i)
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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) ≫
      Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) =
    𝟙 t.pt

Tactic:
apply hom_ext Q

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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := ⋯
⊢ ∀ (j : K),
    (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) ≫
          Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s)) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j
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 : CoreUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
by
    have := adj.left_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.left_triangle] using this X

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
apply yonedaEquiv.injective
  simp [yonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
this : Setoid C := isIsomorphicSetoid C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X

Tactic:
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩

Goal state after: