mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: case mp
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi f → Epi ((forget₂ C Ab).map f)

Tactic:
intro

Goal state after:
case mp
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget₂ C Ab).map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case inl
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
⊢ ∃ i y_1, (hom (ι f i)) y_1 = (hom (head f)) y

Tactic:
inhabit α
    use default, f _ y
    simp only [← arrow_ι _ default, ConcreteCategory.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: case mp
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget₂ C Ab).map f)

Tactic:
infer_instance

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

Goal state before:
pp: case pos
J : MultispanShape
a : J.L
⊢ Subsingleton (left a ⟶ left a)

Tactic:
infer_instance

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

Goal state before:
pp: case neg
J : MultispanShape
a b : J.L
h : ¬a = b
this : IsEmpty (left a ⟶ left b)
⊢ Subsingleton (left a ⟶ left b)

Tactic:
infer_instance

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

Goal state before:
pp: case pos
J : MultispanShape
a : J.R
⊢ Subsingleton (right a ⟶ right a)

Tactic:
infer_instance

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

Goal state before:
pp: case neg
J : MultispanShape
a b : J.R
h : ¬a = b
this : IsEmpty (right a ⟶ right b)
⊢ Subsingleton (right a ⟶ right b)

Tactic:
infer_instance

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

Goal state before:
pp: case left.left
J : MultispanShape
l l' : J.L
⊢ Small.{t, max w w'} (left l ⟶ left l')

Tactic:
infer_instance

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

Goal state before:
pp: case right.left
J : MultispanShape
r : J.R
l' : J.L
⊢ Small.{t, max w w'} (right r ⟶ left l')

Tactic:
infer_instance

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

Goal state before:
pp: case right.right
J : MultispanShape
r r' : J.R
⊢ Small.{t, max w w'} (right r ⟶ right r')

Tactic:
infer_instance

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

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a✝ : J.R
⊢ (((Functor.const (WalkingMulticospan J)).obj a.pt).map (WalkingMulticospan.Hom.snd a✝) ≫
      match WalkingMulticospan.right a✝ with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
    (match WalkingMulticospan.left (J.snd a✝) with
      | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
      | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

Tactic:
dsimp; rw [a.condition_assoc]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (whiskerRight ((reflector R).whiskerLeft (reflectorAdjunction R).counit) R)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
this : IsReflexivePair f g := IsReflexivePair.mk' r rf rg
⊢ HasCoequalizer f g

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
⊢ IsIso (whiskerRight ((coreflector R).whiskerLeft (coreflectorAdjunction R).unit) R)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
this : IsCoreflexivePair f g := IsCoreflexivePair.mk' r fr gr
⊢ HasEqualizer f g

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasCoequalizers C
A B : C
f g : A ⟶ B
x✝ : IsReflexivePair f g
⊢ HasCoequalizer f g

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasEqualizers C
A B : C
f g : A ⟶ B
x✝ : IsCoreflexivePair f g
⊢ HasEqualizer f g

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A

Tactic:
rw [Adjunction.unit_naturality_assoc,
    Adjunction.right_triangle_components, comp_id]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
⊢ ∀ (j_1 : WalkingMultispan J), colimit.ι I.multispan j_1 ≫ i = colimit.ι I.multispan j_1 ≫ j

Tactic:
rintro (a | b)

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ colimit.ι I.multispan (WalkingMultispan.left a) ≫ i = colimit.ι I.multispan (WalkingMultispan.left a) ≫ j

case right
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ colimit.ι I.multispan (WalkingMultispan.right b) ≫ i = colimit.ι I.multispan (WalkingMultispan.right b) ≫ j
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ PreservesLimit (parallelPair (F.map f) (F.map g)) (comonadicRightAdjoint F ⋙ F)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ PreservesLimit
    (parallelPair (F.map ((comonadicRightAdjoint F).map (F.map f))) (F.map ((comonadicRightAdjoint F).map (F.map g))))
    (comonadicRightAdjoint F ⋙ F)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((comparisonAdjunction adj).counit.app X).f

Tactic:
rw [comparisonAdjunction_counit_f]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((beckEqualizer X).lift (counitFork X))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso
    ((limit.isLimit
            (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).conePointUniqueUpToIso
        ?m.215).inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
x✝ : F.IsCosplitPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) :=
  main_pair_F_cosplit adj ((comparison adj).obj Y)
⊢ ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : PreservesColimitsOfShape J T.toFunctor
⊢ {K : J ⥤ T.Algebra} → CreatesColimit K T.forget

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : PreservesColimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor
⊢ {J : Type u} → [inst : Category.{v, u} J] → CreatesColimitsOfShape J T.forget

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
inst✝ : F.IsCosplitPair f✝ g✝
⊢ PreservesLimit (parallelPair f✝ g✝) F

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝ : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
inst✝ : F.IsCosplitPair f✝ g✝
⊢ ReflectsLimit (parallelPair f✝ g✝) F

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((comparisonAdjunction adj).counit.app X).f

Tactic:
rw [comparisonAdjunction_counit_f]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((beckEqualizer X).lift (counitFork X))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso
    ((limit.isLimit
            (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).conePointUniqueUpToIso
        ?m.194).inv

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ Flat R ↑M

Tactic:
infer_instance

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

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (lambda c t ≫ T.ε.app c.pt) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc]
    simp [Coalgebra.counit (D.obj j)]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ g.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_364✝

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]

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

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
T : Comonad C
inst✝ : PreservesLimitsOfShape J T.toFunctor
⊢ {K : J ⥤ T.Coalgebra} → CreatesLimit K T.forget

Tactic:
infer_instance

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

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
T : Comonad C
inst✝ : PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor
⊢ {J : Type u} → [inst : Category.{v, u} J] → CreatesLimitsOfShape J T.forget

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_452✝

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
a : α
t : Set β
⊢ a • -t = -(a • t)

Tactic:
← image_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
a : α
t : Set β
⊢ (fun x ↦ a • x) '' (-t) = -(fun x ↦ a • x) '' t
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ -a • t = -(a • t)

Tactic:
← image_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ (fun x ↦ -a • x) '' t = -(fun x ↦ a • x) '' t
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
r : S
x : N
x✝ : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
y : R
t : ↥p
hyt : IsLocalization.mk' S y t = r
⊢ r • x ∈ (localized₀ p f M').carrier

Tactic:
exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
⊢ J.IsPrime

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ localized' S p f M' ≤ N'

Tactic:
by
    rw [localized'_eq_span, span_le]; apply map_le_iff_le_comap.mpr h

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

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ mk' S x y * (algebraMap R S) ↑y ∈ I

Tactic:
mul_comm

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) ↑y * mk' S x y ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ IsUnit x

Tactic:
have : x * (y * (2 - x * y)) = 1 := by
      rw [eq_comm, ← sub_eq_zero, ← this]
      ring

Goal state after:
case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
this✝¹ : x * y - 1 ∈ I
this✝ : (x * y - 1) ^ 2 = 0
this : x * (y * (2 - x * y)) = 1
⊢ IsUnit x
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submonoid R
φ : M →ₗ[R] N
⊢ Function.Surjective ⇑((LocalizedModule.map S) φ) ↔ Subsingleton (LocalizedModule S (N ⧸ φ.range))

Tactic:
by
  simp [(localizedQuotientEquiv S φ.range).symm.subsingleton_congr,
    LinearMap.localized'_range_eq_range_localizedMap (Localization S) S
      (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N),
    LinearMap.range_eq_top, LocalizedModule.map, mapExtendScalars]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ Subsingleton M

Tactic:
by
  rw [subsingleton_iff_forall_eq 0]
  intro x
  exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

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

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
inst✝ : IsLocalization M S
I : Ideal R
⊢ Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical

Tactic:
refine (I.map_radical_le (algebraMap R S)).antisymm ?_

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ (Ideal.map (algebraMap R S) I).radical ≤ Ideal.map (algebraMap R S) I.radical