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

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1) =
    1 +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1

Tactic:
((isAddUnit_detp_smul_mul_adjp hAB).add
      ((isAddUnit_detp_mul_detp hAB).smul_right _)).add_left_inj

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : B * A = 1
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ Set.InjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ

Tactic:
intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x

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

Goal state before:
pp: case convert_2.inr
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    ∑ x ∈ s, f fun j ↦ if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j

Tactic:
apply sum_congr rfl
    grind

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₁₂FunctorObj F₁₂).obj G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₁₂FunctorObj F₁₂').obj G).map f

Tactic:
by
        ext X₂ X₃
        dsimp
        simp only [← NatTrans.comp_app, NatTrans.naturality, ← G.map_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ 𝟙 X✝ ▷ Y✝ = 𝟙 (X✝ ⊗ Y✝)

Tactic:
simp [← tensorHom_id, id_tensorHom_id]

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

Goal state before:
pp: case h₂
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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ (μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y)).2 = (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).2

Tactic:
simp only [prod_comp_snd, prod'_μ_snd, prod'_app_snd,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

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

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
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ LaxMonoidal.μ F₂ X Y = (𝟙 (F₂.obj X) ⊗ₘ 𝟙 (F₂.obj Y)) ≫ LaxMonoidal.μ F₂ X Y

Tactic:
tensorHom_id,

Goal state after:
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
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ LaxMonoidal.μ F₂ X Y = 𝟙 (F₂.obj X) ▷ F₂.obj Y ≫ LaxMonoidal.μ F₂ X Y
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ (equivalenceTransported e).inverse.Monoidal

Tactic:
dsimp +instances only [Transported.instMonoidalCategory]
  infer_instance

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
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
classical
  cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp]

Goal state after:
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (forget₂ (ModuleCat R) AddCommGrpCat).map
        (homMk
          (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
          ⋯)

Tactic:
erw [colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F✝ : J ⥤ AddCommGrpCat
inst✝ : Small.{w, u} J
F : J ⥤ AddCommGrpCat
⊢ HasColimit F

Tactic:
classical
  exact hasColimit_of_small_quot F inferInstance

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

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
⊢ inl ↑0 = 0

Tactic:
simp [Nat.cast]

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

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).fst = (inl ↑x✝ + 1).fst

Tactic:
simp [Nat.cast]

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).snd = (inl ↑x✝ + 1).snd

Tactic:
simp [Nat.cast]

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

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a⁻¹.fst

Tactic:
fst_inv

Goal state after:
case h1
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ b.fst⁻¹ * a.fst⁻¹ = b.fst⁻¹ * a.fst⁻¹
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul

Tactic:
ext : 1
  · rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, snd_comp_inl, TensorProduct.map_zero_left, zero_comp]
  · rw [comp_assoc, snd_comp_inr, comp_id, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, snd_comp_inr, TensorProduct.map_id, id_comp]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst ≠ 0

Tactic:
fst_inv

Goal state after:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x.fst⁻¹ ≠ 0
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
⊢ TensorProduct.map (inl R A B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

Tactic:
← rTensor_comp_lTensor,

Goal state after:
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
⊢ (rTensor R (inl R A B) ∘ₗ lTensor A counit) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B
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
⊢ TensorProduct.map (inr R A B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
← rTensor_comp_lTensor,

Goal state after:
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 R (inr R A B) ∘ₗ lTensor B counit) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
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)
i✝ : ι
⊢ TensorProduct.map (lsingle i✝) counit ∘ₗ comul = (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝

Tactic:
← rTensor_comp_lTensor,

Goal state after:
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)
i✝ : ι
⊢ (rTensor R (lsingle i✝) ∘ₗ lTensor (A i✝) counit) ∘ₗ comul =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝
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
a✝ : ι
⊢ TensorProduct.map (lsingle a✝) counit ∘ₗ comul = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝

Tactic:
← rTensor_comp_lTensor,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ (rTensor R (lsingle a✝) ∘ₗ lTensor A counit) ∘ₗ comul = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ map (LinearMap.single R A i✝) counit ∘ₗ comul =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝

Tactic:
← rTensor_comp_lTensor,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (rTensor R (LinearMap.single R A i✝) ∘ₗ lTensor (A i✝) counit) ∘ₗ comul =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝
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:
by subst hf; rfl

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
A : Mon Cᵒᵖ
⊢ μ.unop ≫ η.unop ▷ unop A.X = (λ_ (unop A.X)).inv

Tactic:
rw [← unop_whiskerRight, ← unop_comp, MonObj.one_mul]; rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
hg : IsUnit (g x)
y : ↥(powers x)
⊢ IsUnit (g ↑y)

Tactic:
obtain ⟨n, hn⟩ := y.2

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
hg : IsUnit (g x)
y : ↥(powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ↑y)
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
⊢ IsAddUnit (g ↑y)

Tactic:
obtain ⟨n, hn⟩ := y.2

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g ↑y)
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g ↑y)

Tactic:
← hn

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g ((fun i ↦ i • x) n))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
⊢ IsUnit (g ↑y)

Tactic:
obtain ⟨n, hn⟩ := y.2

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ↑y)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f (a ^ (0 + n) * c) = f (a ^ (0 + (n + m)) * b ^ m) * s

Tactic:
by simp [e, pow_add]; ring

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
⊢ IsUnit r

Tactic:
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h
  rw [mem_bot, sub_eq_zero, mul_comm] at hs
  exact .of_mul_eq_one _ hs

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

Goal state before:
pp: case of
carrier✝ : Type u_1
commRing✝ : CommRing carrier✝
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of carrier✝)) (Localization.Away 1)))

Tactic:
exact localization_unit_isIso _

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

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| ((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| η ⊗ₘ η ⊗ₘ η

Tactic:
tensorHom_id,

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (λ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| η ⊗ₘ η ⊗ₘ η
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| 𝟙_ C ◁ μ ≫ (λ_ M).hom

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| tensorμ (𝟙_ C) M (𝟙_ C) M

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (λ_ (𝟙_ C)).hom ▷ (M ⊗ M)

Tactic:
rw [leftUnitor_naturality]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (λ_ (M ⊗ M)).hom ≫ μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| tensorμ (𝟙_ C) M (𝟙_ C) M

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (λ_ (𝟙_ C)).hom ▷ (M ⊗ M)