mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ IsPullback t l r b ↔
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
constructor

Goal state after:
case mp
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ IsPullback t l r b →
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

case mpr
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ (t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃),
          (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃) →
    IsPullback t l r b
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
⊢ Function.Bijective ⇑(hom φ)

Tactic:
constructor

Goal state after:
case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Injective ⇑(hom φ)

case right
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Surjective ⇑(hom φ)
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: 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
⊢ Mono f ↔ Mono ((forget₂ C Ab).map f)

Tactic:
constructor

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
⊢ Mono f → Mono ((forget₂ C Ab).map f)

case mpr
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
⊢ Mono ((forget₂ C Ab).map f) → Mono f
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: 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:
constructor

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
⊢ Epi f → Epi ((forget₂ C Ab).map f)

case mpr
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 ((forget₂ C Ab).map f) → Epi f
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: 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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom (D.φ₁ ≫ D.L₂.f)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
φ₁_L₂_f

Goal state after:
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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.φ₂) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (ConcreteCategory.hom D.L₂.f) x₁
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f = 0

Tactic:
ext

Goal state after:
R : Type u
inst✝⁴ : Ring R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : ↑(ModuleCat.of R ↥f.ker)
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f)) x✝ = (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ (CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A)).f = (𝟙 (T.cofree.obj X.A)).f
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ (CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A)).f = (𝟙 (T.cofree.obj X.A)).f
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ } ≫ (beckCoalgebraFork X).ι = s.ι

Tactic:
ext

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ ({ f := s.ι.f ≫ T.ε.app X.A, h := ⋯ } ≫ (beckCoalgebraFork X).ι).f = s.ι.f
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }

Tactic:
ext

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }.f
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

Tactic:
obtain ⟨_ | _, hi⟩ := i

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
⊢ map F f ⟨0, hi⟩ ⟨0, hi⟩ ⋯ = 𝟙 (obj F X ⟨0, hi⟩)

case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨n✝ + 1, hi⟩ ⋯ = 𝟙 (obj F X ⟨n✝ + 1, hi⟩)
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
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X ≫ h.unit.app (R.obj (L.obj X))) = L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))

Tactic:
← Adjunction.unit_naturality,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X ≫ R.map (L.map (h.unit.app X))) = L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
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
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesLimit (F ⋙ R) (monadicLeftAdjoint R)

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cone (F ⋙ R)} (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
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
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ IsLimit ((monadicLeftAdjoint R).mapCone c)
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
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cocone (F ⋙ R)} (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
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
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ IsColimit ((comonadicRightAdjoint R).mapCocone c)
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: case e_f
M : Type u_1
N : Type u_2
R : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R
inst✝³ : MulSemiringAction M R
inst✝² : MulSemiringAction N R
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N R
x : M
y : N
z : Ideal R
⊢ MulSemiringAction.toRingHom N R (x • y) = (MulSemiringAction.toRingHom M R x).comp (MulSemiringAction.toRingHom N R y)

Tactic:
ext

Goal state after:
case e_f
M : Type u_1
N : Type u_2
R : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R
inst✝³ : MulSemiringAction M R
inst✝² : MulSemiringAction N R
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N R
x : M
y : N
z : Ideal R
x✝ : R
⊢ (MulSemiringAction.toRingHom N R (x • y)) x✝ =
    ((MulSemiringAction.toRingHom M R x).comp (MulSemiringAction.toRingHom N R y)) x✝
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
ext

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ x✝ ∈ (a • S).toAddSubmonoid ↔ x✝ ∈ a • S.toAddSubmonoid
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
⊢ Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S

Tactic:
ext

Goal state after:
M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ x✝ ∈ Submodule.toAddSubgroup (a • S) ↔ x✝ ∈ a • Submodule.toAddSubgroup S
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
⊢ a • S = comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Tactic:
ext

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ a • S ↔ x✝ ∈ comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
a : A
⊢ a ∈ under A (g • P) ↔ a ∈ under A P

Tactic:
rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]

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

Goal state before:
pp: case e_f
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
⊢ (algebraMap A B).comp ↑(RingEquiv.symm ((MulSemiringAction.toRingAut G A) g)) =
    (↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) g))).comp (algebraMap A B)

Tactic:
ext

Goal state after:
case e_f
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
x✝ : A
⊢ ((algebraMap A B).comp ↑(RingEquiv.symm ((MulSemiringAction.toRingAut G A) g))) x✝ =
    ((↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) g))).comp (algebraMap A B)) x✝
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
⊢ under A (under B 𝔓) = under A 𝔓

Tactic:
by
  simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I ≠ ⊤

case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • S.mkQ.range = ⊥

Tactic:
← map_top

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ = ⊥
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 : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ IsLocalizedModule.mk' f (r • m) s = r • x

Tactic:
rw [IsLocalizedModule.mk'_smul, hx]

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'' : Submodule R M
r : R
x : N
⊢ x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x} →
    r • x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}

Tactic:
rintro ⟨m, hm, s, hx⟩
    exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
⊢ (map N.mkQ P).annihilator = N.colon ↑P

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ x✝ ∈ (map N.mkQ P).annihilator ↔ x✝ ∈ N.colon ↑P
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) → IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulLeft R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) → IsNilpotent a

case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulRight R a)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ J ∈ {I.radical}

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I.radical}

case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ {I.radical} → J ∈ I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ ↔ I = ⊤

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ → I = ⊤

case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → I.minimalPrimes = ∅
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = 0

Tactic:
ext

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : ⟨(f ^ n) ↑⟨x, ⋯⟩, ⋯⟩ = 0
⊢ ↑⟨(f ^ n) ↑⟨x, hx⟩, ⋯⟩ = ↑0