mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ 1 + 1 ≤ 5

Tactic:
valid

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app zero = (𝟙 F).app zero

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app one = (𝟙 F).app one

Tactic:
simp

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✝
⊢ 2 + 1 ≤ 5

Tactic:
valid

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app zero = (𝟙 G).app zero

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app one = (𝟙 G).app one

Tactic:
simp

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✝
⊢ 3 + 1 ≤ 5

Tactic:
valid

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app zero = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app zero

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app one = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app one

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
by
  rw [Cocone.w G left, Cocone.w G right]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
simp

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✝
⊢ 4 + 1 ≤ 5

Tactic:
valid

Goal state after:
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
x✝ : R
⊢ (MulSemiringAction.toRingHom N R (x • y)) x✝ =
    ((MulSemiringAction.toRingHom M R x).comp (MulSemiringAction.toRingHom N R y)) x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
            (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).ι.app
      WalkingParallelPair.one =
    G.ι.app zero

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f ↦ F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }.ι.app
        WalkingParallelPair.one =
    G.π

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ HasColimit F ↔ HasCoequalizer (F.map left) (F.map right)

Tactic:
by
  simpa only [hasColimit_iff_hasInitial_cocone]
    using Equivalence.hasInitial_iff (reflexiveCoforkEquivCofork F)

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' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.inv = app₄.inv ≫ f.map' 4 5 _proof_453✝ _proof_454✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₄ app₅ w₄]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 5
⊢ X.map' 0 1 homMk₁._proof_4 _proof_450 =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 0 1
          homMk₁._proof_4 _proof_450 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
R : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
N : Type u_4
inst✝¹ : Group N
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
x✝¹ x✝ : ↥(MulAction.stabilizer M I)
⊢ ((↑e).subtypeEquiv ⋯).toFun (x✝¹ * x✝) = ((↑e).subtypeEquiv ⋯).toFun x✝¹ * ((↑e).subtypeEquiv ⋯).toFun x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 5
⊢ X.map' 1 2 _proof_246 _proof_451 =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 1 2 _proof_246
          _proof_451 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 5
⊢ X.map' 2 3 _proof_299 _proof_452 =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 2 3 _proof_299
          _proof_452 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 5
⊢ X.map' 3 4 _proof_364 _proof_453 =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 3 4 _proof_364
          _proof_453 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
R✝ : Type u_3
inst✝⁷ : Group M
inst✝⁶ : Semiring R✝
inst✝⁵ : MulSemiringAction M R✝
N : Type u_4
inst✝⁴ : Group N
inst✝³ : MulSemiringAction N R✝
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
⊢ ∀ (x y : ↥(inertia M I)),
    ((↑e).subtypeEquiv ⋯).toFun (x * y) = ((↑e).subtypeEquiv ⋯).toFun x * ((↑e).subtypeEquiv ⋯).toFun y

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ComposableArrows C 5
⊢ X.map' 4 5 _proof_453 _proof_454 =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 4 5 _proof_453
          _proof_454 ≫
        eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
hi : 0 < n + 1
⊢ mapSucc ⟨0, hi⟩ =
    ((fun i ↦
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨0, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' 0 (0 + 1) ⋯ hi ≫
        ((fun i ↦
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨0 + 1, ⋯⟩).hom

Tactic:
simp

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

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : ↑p = ⇑(algebraMap A C) ⁻¹' ↑𝔓
⊢ ↑(Submonoid.map (algebraMap A C) { carrier := (⇑(algebraMap A C) ⁻¹' ↑𝔓)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }) ⊆ (↑𝔓)ᶜ

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i + 1 < n + 1
⊢ i < n

Tactic:
valid

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ F e, ∀ (i : ℕ) (hi : i < n + 1), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Tactic:
obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp
    · exact h i (by valid)

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ a ∈ insert a s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Submodule R M
hI : S.IsPrimary
⊢ S ≠ ⊤ → (S.colon Set.univ).radical ≠ ⊤

Tactic:
simp

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
⊢ IsLocalizedModule.mk' f 0 1 = 0

Tactic:
simp

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' : Submodule R M
m : M
hm : m ∈ ↑M'
⊢ IsLocalizedModule.mk' f m 1 = f m

Tactic:
simp

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' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ f m = IsLocalizedModule.mk' f m 1

Tactic:
simp

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 : localized' S p f M' ≤ N'
m : M
hm : m ∈ M'
⊢ IsLocalizedModule.mk' f m 1 = f m

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (fun q ↦ q.IsPrime ∧ ⊥ ≤ q) = Ideal.IsPrime

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
a✝ b✝ : R
ha : a✝ ∈ {r | r • S ⊆ ↑N}
hb : b✝ ∈ {r | r • S ⊆ ↑N}
⊢ ↑N + ↑N = ↑N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
⊢ 0 ⊆ ↑N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.colon {0} = ⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.colon ↑⊥ = ⊤

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
⊢ r • 0 ∈ N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
S : Set R
⊢ colon I ↑(Ideal.span S) = colon I S

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
r : R
⊢ r ∈ N.colon ↑(R ∙ x) ↔ r • x ∈ N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x r : R
⊢ r ∈ colon I ↑(Ideal.span {x}) ↔ r * x ∈ I

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

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

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
IsLocalizedModule.mk'_smul

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r 1 = (algebraMap R S) r

Tactic:
simp

Goal state after: