mathlib-initiative/mathlib-tactics huggingface dataset:
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 β
⊢ ε F ≫ ((prod' α β).app (𝟙_ C)).1 = (ε (G.prod' K)).1

Tactic:
prod'_ε_fst,

Goal state after:
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 β
⊢ ε F ≫ ((prod' α β).app (𝟙_ C)).1 = ε G
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit (limitCone F)

Tactic:
refine IsLimit.ofFaithful (forget SemiRingCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_ })
    (fun s => rfl)

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

case refine_2
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, ⋯⟩

case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) 0, ⋯⟩ =
    0

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, ⋯⟩
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
⊢ ε F = ε F

Tactic:
rw [← cancel_mono (εIso _).inv]
    rw [εIso_inv, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_inv]
    exact congr(_ ≫ ($eq.symm).η)

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ⊗ i ⟶ f ⊗ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (f ◁ᵢ α).hom ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : epimorphisms C f
hg : epimorphisms C g
⊢ epimorphisms C (f ≫ g)

Tactic:
rw [epimorphisms.iff] at hf hg ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit c.op → IsColimit c

Tactic:
· intro h
    exact (IsColimit.equivIsoColimit c.opUnopIso).toFun
      (((IsLimit.postcomposeHomEquiv _ _).invFun
        ((IsLimit.whiskerEquivalenceEquiv _).toFun h)).unop)

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₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ₘ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂)

Tactic:
convert! tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1 <;> simp

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)
i j : J
f : i ⟶ j
⊢ F.map f ≫ homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j) ⋯ =
    homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i) ⋯ ≫
      ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f

Tactic:
apply (forget₂ _ AddCommGrpCat).map_injective

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)
i j : J
f : i ⟶ j
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map
      (F.map f ≫ homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j) ⋯) =
    (forget₂ (ModuleCat R) AddCommGrpCat).map
      (homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i) ⋯ ≫
        ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)
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
j : J
⊢ (colimitCocone F).ι.app j ≫
      homMk (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
        ⋯ =
    s.ι.app j

Tactic:
apply (forget₂ _ AddCommGrpCat).map_injective

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
j : J
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map
      ((colimitCocone F).ι.app j ≫
        homMk
          (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
          ⋯) =
    (forget₂ (ModuleCat R) AddCommGrpCat).map (s.ι.app j)
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
j : J
⊢ (colimitCocone F).ι.app j ≫
      homMk (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
        ⋯ =
    s.ι.app j

Tactic:
apply (forget₂ _ AddCommGrpCat).map_injective
    exact colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j

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
⊢ m =
    homMk (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)) ⋯

Tactic:
apply (forget₂ _ AddCommGrpCat).map_injective

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
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    (forget₂ (ModuleCat R) AddCommGrpCat).map
      (homMk
        (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)) ⋯)
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
x : Quot F
| x

Tactic:
← AddMonoidHom.id_apply _ x

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
| (AddMonoidHom.id (Quot F)) x
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
x : Quot (F ⋙ uliftFunctor)
| x

Tactic:
← AddMonoidHom.id_apply _ x

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
| (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) x
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ ↑(FreeAlgebra.ι R (x + y)) = ↑(FreeAlgebra.ι R x) + ↑(FreeAlgebra.ι R y)

Tactic:
rw [← RingCon.coe_add]
      exact Quotient.sound <| RingConGen.Rel.of _ _ Rel.add

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))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) + (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))

Tactic:
simp only [map_zero, add_zero]

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))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))
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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
rw [ExtendScalars.smul_tmul, mul_one]

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ _root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
        (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ∘ₗ
      comul =
    comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap

Tactic:
ext x y
    dsimp
    simp only [← CoalgHomClass.map_comp_comul_apply]
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    simp

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

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [coassoc_simps]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a + 1 + a = 1

Tactic:
add_comm a 1,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 + a + a = 1
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
by
  monoidal_coherence

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv

Tactic:
by
  monoidal_coherence

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
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
      rw [← hn]
      dsimp
      rw [g.map_nsmul]
      exact IsAddUnit.map (nsmulAddMonoidHom n : C →+ C) hg

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
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x ↦ e ^ x) n, ⋯⟩)

Tactic:
simp [show algebraMap R S e = 1 by rw [← (algebraMap R S).map_one, H, mul_one, he]]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
        ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
      · exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩
      · exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
      · exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩
      · refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
        simp [mul_assoc]

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

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ (algebraMap R S) (r ^ n) • Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) (RingHom.ker (algebraMap S T))) ≤
    ⊥

Tactic:
← Ideal.map_pointwise_smul,

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Ideal.map (algebraMap R S) (r ^ n • Ideal.comap (algebraMap R S) (RingHom.ker (algebraMap S T))) ≤ ⊥
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; exact (nonunitsAddSubmonoid R).sum_mem h

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥

Tactic:
· refine Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_
        exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥
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 J : Ideal S
⊢ J ∈ {J | K ≤ J ∧ J.IsMaximal} → sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Tactic:
hJ

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
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl.inl
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 : ℤ
hn : 0 ≤ n
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = (algebraMap R B) x ^ n.natAbs * selfZPow x B m

Tactic:
selfZPow_of_nonneg _ _ hm,

Goal state after:
case inl.inl
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 : ℤ
hn : 0 ≤ n
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = (algebraMap R B) x ^ n.natAbs * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
selfZPow_of_nonneg _ _ hm,

Goal state after:
case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ η = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ

pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ = η

Tactic:
· simp [tensorHom_def, H, ← unitors_equal]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ = η
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (μ ⊗ₘ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M).hom = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ

Tactic:
rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (𝟙 (M ⊗ M) ⊗ₘ (λ_ (𝟙_ C)).hom) ≫ (μ ⊗ₘ 𝟙 (𝟙_ C))) ≫ (ρ_ M).hom =
    ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ l, l ≫ fst = a ∧ l ≫ snd = b
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))

Tactic:
let l (s : PullbackCone f g) := exists_lift _ _ s.condition

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ l, l ≫ fst = a ∧ l ≫ snd = b
l : ∀ (s : PullbackCone f g), ∃ l, l ≫ fst = s.fst ∧ l ≫ snd = s.snd :=
  fun s ↦ exists_lift s.fst s.snd (PullbackCone.condition s)
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))