mathlib-initiative/mathlib-tactics huggingface dataset:
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]

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
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.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
      μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
        G.map
          ((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) =
    (α_ X Y Z).hom ≫
      (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
        μ G (F.obj X) (F.obj (Y ⊗ Z)) ≫
          G.map
            (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)))
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✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.unit.app x✝ ≫ 𝟙 (G.obj (F.obj x✝)) ⊗ₘ
          adj.unit.app (𝟙_ C) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))) ≫
        μ G (F.obj x✝) (𝟙_ D)

Tactic:
simp [tensorHom_def, homEquiv_unit, homEquiv_counit]

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (desc F c) ((ι F j) x) = (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
dsimp [desc, ι]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F) (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x) =
    (ConcreteCategory.hom (c.ι.app j)) x
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).inv ≫
        (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
          μ F W X ▷ F.obj Y ▷ F.obj Z ≫
            μ F (W ⊗ X) Y ▷ F.obj Z ≫
              μ F ((W ⊗ X) ⊗ Y) Z ≫
                F.map ((α_ W X Y).hom ▷ Z) ≫
                  F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
Iso.hom_inv_id_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W ⊗ F.obj X) (F.obj Y) (F.obj Z)).inv ≫
      μ F W X ▷ F.obj Y ▷ F.obj Z ≫
        μ F (W ⊗ X) Y ▷ F.obj Z ≫
          μ F ((W ⊗ X) ⊗ Y) Z ≫
            F.map ((α_ W X Y).hom ▷ Z) ≫
              F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x + Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) + (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
exact congrArg toQuotient (e.map_add x y)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), ↑s x x_1 → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔ ∀ {x y : M}, ↑s x y → ↑t x y

Tactic:
mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le t.2) c.mk'_surjective

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

Goal state before:
pp: 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 : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]

Goal state after:
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 : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i + i) •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case zero
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)
⊢ (List.map (fun i ↦ x.fst ^ (0 - i) •> x.snd <• x.fst ^ i) (List.range (0 + 1))).sum =
    (x ^ 0).fst •> x.snd +
      (List.map (fun i ↦ x.fst ^ (Nat.pred 0 - i) •> x.snd <• x.fst ^ i) (List.range 0)).sum <• x.fst

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✝ : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n✝ + 1 - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1 + 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 [List.range_succ]

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✝ : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n✝ + 1 - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1 + 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
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.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ lTensor A comul ∘ₗ comul) x

Tactic:
← coassoc,

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
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.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
        ↑(TensorProduct.assoc R A A A) ∘ₗ rTensor A comul ∘ₗ comul)
      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.map (inr R A B) (TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ lTensor B comul ∘ₗ comul) x

Tactic:
← coassoc,

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
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.map (inr R A B) (TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
        ↑(TensorProduct.assoc R B B B) ∘ₗ rTensor B comul ∘ₗ comul)
      x
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.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor (A i) comul ∘ₗ comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ lTensor (A i) comul ∘ₗ comul

Tactic:
← coassoc,

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 : ι
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor (A i) comul ∘ₗ comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      ↑(TensorProduct.assoc R (A i) (A i) (A i)) ∘ₗ rTensor (A i) comul ∘ₗ comul
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ (map f) (inr x) = inr (f x)

Tactic:
rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]

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
i : ι
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
      TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor A comul ∘ₗ comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ lTensor A comul ∘ₗ comul

Tactic:
← coassoc,

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
i : ι
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
      TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor A comul ∘ₗ comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      ↑(TensorProduct.assoc R A A A) ∘ₗ rTensor A comul ∘ₗ comul
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
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
      map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) (LinearMap.single R A i✝) ∘ₗ
        rTensor (A i✝) comul ∘ₗ comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      lTensor (A i✝) comul ∘ₗ comul

Tactic:
← coassoc,

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
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
      map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) (LinearMap.single R A i✝) ∘ₗ
        rTensor (A i✝) comul ∘ₗ comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      ↑(TensorProduct.assoc R (A i✝) (A i✝) (A i✝)) ∘ₗ rTensor (A i✝) comul ∘ₗ comul
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: 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 S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ Bialgebra S (A ⊗[R] B)

Tactic:
have hcounit := congr(DFunLike.coe $(counit_eq_algHom_toLinearMap R S A B))
  have hcomul := congr(DFunLike.coe $(comul_eq_algHom_toLinearMap R S A B))
  refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_) <;>
  simp_all only [AlgHom.toLinearMap_apply] <;>
  simp only [map_one, map_mul]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (ε ⊗ₘ f) = f ≫ (λ_ Z).inv

Tactic:
leftUnitor_inv_naturality,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (ε ⊗ₘ f) = (λ_ M).inv ≫ 𝟙_ C ◁ f
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ = LinearMap.lTensor M (LinearMap.lTensor M f) ∘ₗ LinearMap.lTensor M δ ∘ₗ δ

Tactic:
← coassoc,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ = LinearMap.lTensor M (LinearMap.lTensor M f) ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
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
Q : Type u_4
inst✝¹⁵ : CommSemiring Q
inst✝¹⁴ : Algebra P Q
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ (↑↑(map Aₚ Bₚ f.toRingHom a)).toFun ((algebraMap R Aₚ) r) = (algebraMap R Bₚ) r

Tactic:
dsimp only [AlgHom.toRingHom_eq_coe, map, RingHom.coe_coe, OneHom.toFun_eq_coe]
    rw [IsScalarTower.algebraMap_apply R A Aₚ, IsScalarTower.algebraMap_eq R B Bₚ]
    simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
x z : R
y : S
inst✝⁵ : Away x S
T : Type u_4
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : Away y T
h : Associated ((algebraMap R S) z) y
⊢ Away (x * z) T

Tactic:
have : Away (algebraMap R S z) T := by rwa [iff_of_associated h]
  exact .mul' S _ _ _

Goal state after:
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 : R
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
b : R
x : S
c : R
m : ℕ
e : f c = f a ^ m * x
⊢ f (b ^ m * c) = f (a * b) ^ m * x

Tactic:
by simp [mul_pow, e, mul_assoc, mul_left_comm]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ∀ i ∈ {J | K ≤ J ∧ J.IsMaximal}, sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f i

Tactic:
intro J

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
⊢ J ∈ {J | K ≤ J ∧ J.IsMaximal} → sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J
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
    rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx
    rcases hx with ⟨u, rfl⟩
    simpa using I.mul_mem_left (↑u⁻¹) H

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Mon C
f : F.mapMon.obj X ⟶ F.mapMon.obj Y
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ F.map (μ ≫ g) = F.map ((g ⊗ₘ g) ≫ μ)

Tactic:
simpa [← hg, cancel_epi] using IsMonHom.mul_hom f.hom

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
⊢ IsLimit (t₂.pasteHoriz t₁ hi₂)

Tactic:
by
  apply PullbackCone.isLimitAux'
  intro s
  -- Obtain the lift from lifting from both the small squares consecutively.
  obtain ⟨l₂, hl₂, hl₂'⟩ := PullbackCone.IsLimit.lift' H (s.fst ≫ g₁) s.snd
    (by rw [← s.condition, Category.assoc])
  obtain ⟨l₁, hl₁, hl₁'⟩ := PullbackCone.IsLimit.lift' H' s.fst l₂ (by rw [← hl₂, hi₂])
  refine ⟨l₁, hl₁, by simp [reassoc_of% hl₁', hl₂'], ?_⟩
  -- Uniqueness also follows from the universal property of both the small squares.
  intro m hm₁ hm₂
  apply PullbackCone.IsLimit.hom_ext H' (by simpa [hl₁] using hm₁)
  apply PullbackCone.IsLimit.hom_ext H
  · dsimp at hm₁
    rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
  · simpa [hl₁', hl₂'] using hm₂

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • a.2 • b.1 = (↑u * ↑b.2) • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2

Tactic:
← hu,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = (↑u * ↑b.2) • a.1 ∧ ↑(u * a.2) * ↑b.2 = ↑u * ↑b.2 * ↑a.2
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : Localization M
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))) x

Tactic:
obtain ⟨x, y, rfl⟩ := IsLocalization.exists_mk'_eq M x

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] IsLocalization.mk' (Localization M) x y) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)