mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
by
  rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]
  simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]
  refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i
  · simp only [Fin.prod_univ_succ, Matrix.det_apply, Finset.mul_sum,
      Equiv.Perm.decomposeFin_symm_apply_zero, Fin.val_zero, one_mul,
      Equiv.Perm.decomposeFin.symm_sign, Equiv.swap_self, if_true, id,
      Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succAbove_zero, Equiv.coe_refl, pow_zero,
      mul_smul_comm, of_apply]
  -- `univ_perm_fin_succ` gives a different embedding of `Perm (Fin n)` into
  -- `Perm (Fin n.succ)` than the determinant of the submatrix we want,
  -- permute `A` so that we get the correct one.
  have : (-1 : R) ^ (i : ℕ) = (Perm.sign i.cycleRange) := by simp [Fin.sign_cycleRange]
  rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),
    ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]
  -- now we just need to move the corresponding parts to the same place
  refine Finset.sum_congr rfl fun σ _ => ?_
  rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]
  calc
    ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =
        (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *
          ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]
    _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •
        ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
simp only [det_succ_row_zero, submatrix_apply, Fin.succ_zero_eq_one, submatrix_submatrix,
    det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, Fin.sum_univ_succ,
    Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,
    Fin.succ_succAbove_zero, sum_singleton, Fin.succ_succAbove_one]

Goal state after:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ (-1) ^ 0 * A 0 0 * ((-1) ^ 0 * A 1 1 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 1) +
      ((-1) ^ (0 + 1) * A 0 1 * ((-1) ^ 0 * A 1 0 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 0) +
        (-1) ^ (0 + 1 + 1) * A 0 2 * ((-1) ^ 0 * A 1 0 * A 2 1 + (-1) ^ (0 + 1) * A 1 1 * A 2 0)) =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: case a.a
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 g.1).app X✝.2 ≫ (F.obj Z✝.1).map f.2

pp: case a.a
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.obj Z✝.1).map g.2

pp: case a
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

Tactic:
rw [← NatTrans.naturality]

Goal state after:
case a.a
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.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2

case a.a
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.obj Z✝.1).map g.2

case a
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
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case refine_2
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ update x i (c • x i) j ∈ p j

Tactic:
rw [update_of_ne hij]
      exact hx j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
⊢ ((flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom).app k =
    ((limitIsoFlipCompLim F).symm.hom ≫ lim.map η).app k

Tactic:
apply limit_obj_ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    ((flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom).app k ≫
        (limit.π G j).app k =
      ((limitIsoFlipCompLim F).symm.hom ≫ lim.map η).app k ≫ (limit.π G j).app k
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
⊢ (((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom).app k =
    ((limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η).app k

Tactic:
apply limit_obj_ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    (((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom).app k ≫
        (limit.π ((flipFunctor K J C).obj G) j).app k =
      ((limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η).app k ≫
        (limit.π ((flipFunctor K J C).obj G) j).app k
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        (x + y) =
      (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          x +
        (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          y

Tactic:
intro x y
    simp [← equivShrink_add]
    rfl

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

Goal state before:
pp: case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y
    simp [← equivShrink_add]
    rfl

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

Goal state before:
pp: case intro
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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j).hom ≫
      biproduct.π (fun j ↦ X ⊗ Y ⊗ f j) j✝ =
    ((α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)).hom ≫
      biproduct.π (fun j ↦ X ⊗ Y ⊗ f j) j✝

Tactic:
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum,
    id_tensor_comp, tensorIso_hom, leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
    biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero]

Goal state after:
case intro
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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        (𝟙 X ⊗ₘ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ₘ biproduct.ι (fun j ↦ Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j ↦ Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv

Tactic:
rw [μIso_inv, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_inv]

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ δ F x✝¹ x✝
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePullbacks Cᵒᵖ ↔ HasWidePushouts C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePullbacks Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape (WidePushoutShape ι) C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePushouts Cᵒᵖ ↔ HasWidePullbacks C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePushouts Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape (WidePullbackShape ι) C
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj (X ⊗ Y) ⊗ F.obj Z)).symm
          ((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
        (adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm,
      Equiv.apply_symm_apply, Equiv.apply_symm_apply, assoc, assoc]
    conv_lhs =>
      rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]
      dsimp
      rw [← comp_whiskerRight_assoc]
    conv_rhs =>
      rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]
      dsimp
      rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
by
  rw [Iso.inv_ext]
  rw [braiding_tensorUnit_left]
  monoidal

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

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B)) (inl R A B)) ((rTensor A comul) (comul x))) =
    ↑(TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B)) (inl R A B)) ((rTensor A comul) (comul x)))

Tactic:
LinearEquiv.coe_coe

Goal state after:
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
f g : A →ₗc[R] R
x : A
hf : counit (f x) = counit x
⊢ f x = g x

Tactic:
have hg := CoalgHomClass.counit_comp_apply g x

Goal state after:
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
f g : A →ₗc[R] R
x : A
hf : counit (f x) = counit x
hg : counit (g x) = counit x
⊢ f x = g x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
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
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inr R A B) (inr R A B)) (inr R A B)) ((rTensor B comul) (comul x))) =
    ↑(TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inr R A B) (inr R A B)) (inr R A B)) ((rTensor B comul) (comul x)))

Tactic:
LinearEquiv.coe_coe

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

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
· rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

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

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : (i : ι) → Coalgebra R (A i)
inst✝ : ∀ (i : ι), IsCocomm R (A i)
⊢ ↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ comul = comul

Tactic:
by ext; simp [← TensorProduct.map_comm]

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

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsCocomm R A
⊢ ↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) ∘ₗ comul = comul

Tactic:
by ext; simp [← TensorProduct.map_comm]

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

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat R
r : R
x : ↑((restrictScalars f).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj M)) (r • x) = r • (AddEquiv.refl ↑((restrictScalars f).obj M)) x

Tactic:
subst hf

Goal state after:
R : Type u₁
inst✝ : Ring R
M : ModuleCat R
r : R
x : ↑((restrictScalars (RingHom.id R)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) x
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)

Tactic:
simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)

Tactic:
simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
ι : Type u_3
s : Finset ι
f : ι → R
h : IsUnit (∑ i ∈ s, f i)
⊢ ∃ i ∈ s, IsUnit (f i)

Tactic:
contrapose! h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
ι : Type u_3
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ¬IsUnit (f i)
⊢ ¬IsUnit (∑ i ∈ s, f i)
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)

Tactic:
by rw [h, sub_zero]; exact isUnit_one

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset 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
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ r a * ↑b ^ N = r b * ↑a ^ N

Tactic:
rw [pow_add, mul_mul_mul_comm, ← mul_pow, eq2,
      mul_comm a.1, mul_pow, mul_mul_mul_comm, ← pow_add]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J

Tactic:
intro I x _ hx H

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
H : x ∈ I
⊢ 1 ∈ I
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
⊢ X ⨯ I ≅ I

Tactic:
by
  have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
  exact asIso prod.snd

Goal state after: