mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
⊢ ((fun i ↦ DFinsupp.single (p i) (m i)) i) (q i) = 0

Tactic:
simp_rw [DFinsupp.single_eq_of_ne hpqi]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (zero.add x) = descFunLift F s x

Tactic:
dsimp; rw [zero_add]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (zero.add x) = descFunLift F s x

Tactic:
dsimp; rw [zero_add]

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

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : h' ∉ H'
h'' : ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T mY = T mX
⊢ ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ insert h' H' → f ≫ T mY = T mX

Tactic:
obtain ⟨X, Y, mX, mY, f⟩ := h'
    obtain ⟨S', T', w'⟩ := h''
    refine ⟨coeq (f ≫ T' mY) (T' mX), fun mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX), ?_⟩
    intro X' Y' mX' mY' f' mf'
    rw [← Category.assoc]
    by_cases h : X = X' ∧ Y = Y'
    · rcases h with ⟨rfl, rfl⟩
      grind [coeq_condition]
    · rw [@w' _ _ mX' mY' f' _]
      apply Finset.mem_of_mem_insert_of_ne mf'
      contrapose h
      obtain ⟨rfl, h⟩ := h
      trivial

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
⊢ (hom (t.ι.app j ≫ ↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun y = (hom (s.ι.app j)).toFun y

Tactic:
have h := congr_hom (s.ι.naturality g) (f (t.ι.app j y))

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
h :
  (hom (F.map g ≫ s.ι.app k)) (f ((hom (t.ι.app j)) y)) =
    (hom (s.ι.app (α ((hom (t.ι.app j)) y)) ≫ ((Functor.const J).obj s.pt).map g)) (f ((hom (t.ι.app j)) y))
⊢ (hom (t.ι.app j ≫ ↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun y = (hom (s.ι.app j)).toFun y
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := ⋯
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ i.castSucc < k.succ

Tactic:
rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) → ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, (hom (F.map f)) x = (hom (F.map f)) y) → ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y

Tactic:
· rintro ⟨k, f, g, h⟩
    refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
    conv_rhs => rw [IsFiltered.coeq_condition]
    simp [h]

Goal state after:
case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, (hom (F.map f)) x = (hom (F.map f)) y) → ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = 0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]

Goal state after:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ blockDiagonal M (σ (k, x)) (k, x) = 0
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c✝ : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
f : c.pt ⟶ c✝.pt
hf : ∀ (j : J), f ≫ c✝.π.app j = c.π.app j
y : c.pt
⊢ (hom f).toFun y = (hom (↾x c)).toFun y

Tactic:
exact (hx c y).2 (f y) (fun j ↦ congr_hom (hf j) y)

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (F.map f.1).app X✝.2 ≫ (F.map g.1).app X✝.2 ≫ (F.obj Z✝.1).map f.2 ≫ (F.obj Z✝.1).map g.2 =
    (F.map f.1).app X✝.2 ≫ (F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2 ≫ (F.obj Z✝.1).map g.2

Tactic:
slice_lhs 2 3 => rw [← NatTrans.naturality]

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (F.map f.1).app X✝.2 ≫ ((F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2) ≫ (F.obj Z✝.1).map g.2 =
    (F.map f.1).app X✝.2 ≫ (F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2 ≫ (F.obj Z✝.1).map g.2
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯) = s.ι.app i

Tactic:
by
    ext
    dsimp only [hom_comp, directLimitCocone, hom_ofHom, LinearMap.comp_apply]
    apply DirectLimit.lift_of

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.inv ⊗ₘ g.inv) ≫ (f.hom ⊗ₘ g.hom) = 𝟙 (Y ⊗ Y')

Tactic:
by simp [Iso.inv_hom_id, Iso.inv_hom_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j ↦ X ⊗ f j) j

Tactic:
by
  classical
  cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp,
    biproduct.ι_π, whiskerLeft_dite, comp_dite]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)

Tactic:
rw [Functor.Monoidal.map_whiskerRight]

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ Functor.OplaxMonoidal.δ F X Z ≫ F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z = F.map (r • f ▷ Z)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
by
  rw [← ih_η]
  apply Iso.ext
  simp [← whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

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.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneUnopOfCocone s)).op

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
    simpa only [Quiver.Hom.unop_op, IsLimit.fac] using! w (op j)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasColimit F
j : Jᵒᵖ
⊢ (limitOpIsoOpColimit F).inv ≫ limit.π F.op j = (colimit.ι F (unop j)).op

Tactic:
by
  simp [limitOpIsoOpColimit]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫ cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ =
    𝟙 (of (↑H ⧸ (Hom.hom f).range))

Tactic:
by
    ext x
    dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk',
      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id]
    exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective ⇑(c.lift f h) ∧ Surjective ⇑(c.lift f h) ↔ c = ker f ∧ Surjective ⇑f

Tactic:
simp only [lift_injective_iff, lift_surjective_iff]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1 - 0) •> x.snd <• x.fst ^ 0 +
      (List.map (fun i ↦ x.fst ^ (n✝ + 1 - i.succ) •> x.snd <• x.fst ^ i.succ) (List.range (n✝ + 1))).sum =
    (x ^ (n✝ + 1)).fst •> x.snd +
      (List.map (fun i ↦ x.fst ^ ((n✝ + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1))).sum <• x.fst

Tactic:
simp only [pow_zero, op_one, Nat.sub_zero, one_smul, Nat.succ_sub_succ_eq_sub, fst_pow,
          Nat.pred_succ, List.smul_sum, List.map_map, Function.comp_def]

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> x.snd <• x.fst ^ i.succ) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> x.snd <• x.fst ^ x_1 <• x.fst) (List.range (n✝ + 1))).sum
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ map counit counit ∘ₗ comul = comul ∘ₗ counit

Tactic:
ext
      simp only [LinearMap.coe_comp, Function.comp_apply, CommSemiring.comul_apply,
        ← LinearMap.lTensor_comp_rTensor, rTensor_counit_comul, LinearMap.lTensor_tmul]

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

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : ↑Y
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (r • y))) 1 =
    (RingHom.id R) r • ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
rw [← map_smul]
      simp [ModuleCat.restrictScalars.smul_def (M := ModuleCat.of S S)]

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

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ (f r * s) • y = f r • s • y

Tactic:
mul_smul

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ f r • s • y = f r • s • y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
r : R
s : S
y : ↑Y
⊢ (f r * s) • y = f r • s • y

Tactic:
mul_smul

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
r : R
s : S
y : ↑Y
⊢ f r • s • y = f r • s • y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f = Counit.map f ≫ (𝟭 (ModuleCat S)).map g

Tactic:
let m1 : Module R S := Module.compHom S f
    let m2 : Module R Y := Module.compHom Y f
    let m2 : Module R Y' := Module.compHom Y' f
    ext z
    induction z using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero]
    | tmul s' y =>
      dsimp
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [Counit.map_hom_apply]
      rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
      set s' : S := s'
      change s' • g y = g (s' • y)
      rw [map_smul]
    | add _ _ ih₁ ih₂ => rw [map_add, map_add]; congr 1

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

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalarsId R₂).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (RingHom.id R₂)).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    1 ⊗ₜ[R₁] m

Tactic:
extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m,

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalarsId R₂).hom.app ((extendScalars f₁₂).obj M))) (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)) = 1 ⊗ₜ[R₁] m
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : AsBoolAlg α
⊢ ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ofBoolAlg a + ofBoolAlg b

Tactic:
exact of_boolalg_symmDiff_aux _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ F.obj A ◁ (F.map ε ≫ η F) = (ρ_ (F.obj A)).inv

Tactic:
by
    simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
      right_unitality, ← F.map_comp_assoc, comul_counit]

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ ∏ᶠ (p : R), p ^ count p (normalizedFactors x) ~ᵤ x

Tactic:
← Multiset.prod_map_eq_finprod,

Goal state after:
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ (map (fun p ↦ p) (normalizedFactors x)).prod ~ᵤ x
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
repeat rw [IsScalarTower.algebraMap_apply R S T] at h
    obtain ⟨n, hn⟩ := exists_of_eq (algebraMap R S y) h
    simp only [← map_pow, ← map_mul, ← map_mul] at hn
    obtain ⟨m, hm⟩ := exists_of_eq x hn
    use n + m
    convert_to y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))
    · ring
    · ring
    · rw [hm]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (LinearMap.toSpanSingleton R R e) (x - y) = 0 ↔ e * x = e * y

Tactic:
LinearMap.toSpanSingleton_apply,

Goal state after:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (x - y) • e = 0 ↔ e * x = e * y
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
push Not at hx

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem✝ : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
⊢ (algebraMap R (Away ↑a)) r = f a

Tactic:
classical
    have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩
    exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)

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

Goal state before:
pp: case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

Tactic:
apply (H _ h).hom_ext

Goal state after: