mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ m • ↑(p / ↑n) ≠ 0

Tactic:
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬↑(↑m * (p / ↑n)) = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ⟨↑(↑↑m₁ / ↑n * p), ⋯⟩ = ⟨↑(↑↑m₂ / ↑n * p), ⋯⟩
⊢ ↑m₁ = ↑m₂

Tactic:
[

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ⟨↑(↑↑m₁ / ↑n * p), ⋯⟩ = ⟨↑(↑↑m₂ / ↑n * p), ⋯⟩
⊢ ↑m₁ = ↑m₂
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
[

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
[

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot] (equivIccQuot p a).toFun

Tactic:
[

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot] (equivIccQuot p a).toFun
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (fst X X + snd X X) ▷ X ≫ (fst X X + snd X X) = (α_ X X X).hom ≫ X ◁ (fst X X + snd X X) ≫ (fst X X + snd X X)

Tactic:
simp [add_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case i.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Submodule.comap (Hom.hom S.arrow).range.subtype (Hom.hom S.arrow).range = ⊤

pp: case i.right.hf
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range

Tactic:
Submodule.comap_subtype_self

Goal state after:
case i.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ⊤ = ⊤

case i.right.hf
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s ↦ (r • g).sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s ↦ (r • g).sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)
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
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂

Tactic:
this

Goal state after:
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
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ x₂ = x₂
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
[

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))
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
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
X : D
⊢ ((adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit).app X = (𝟙 (𝟭 D)).app X

Tactic:
exact (adj.toComonad.transport j).right_counit X

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

Goal state before:
pp: case zero.succ.succ.succ.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
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

pp: case zero.succ.succ.succ.succ
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
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
· simp [Fin.le_def] at hjk

Goal state after:
case zero.succ.succ.succ.succ
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
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

Tactic:
[

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
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 j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

Tactic:
obtain ⟨i, hi⟩ := i
  obtain ⟨j, hj⟩ := j
  obtain ⟨k, hk⟩ := k
  cases i
  · obtain _ | _ | j := j
    · dsimp
      rw [id_comp]
    · obtain _ | _ | k := k
      · simp at hjk
      · simp
      · rfl
    · obtain _ | _ | k := k
      · simp [Fin.ext_iff] at hjk
      · simp [Fin.le_def] at hjk
      · dsimp
        rw [assoc, ← F.map_comp, homOfLE_comp]
  · obtain _ | j := j
    · simp [Fin.ext_iff] at hij
    · obtain _ | k := k
      · simp [Fin.ext_iff] at hjk
      · dsimp
        rw [← F.map_comp, homOfLE_comp]

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

Goal state before:
pp: case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : I.fst (y, x) ≫ c.π y = I.snd (y, x) ≫ c.π x
⊢ (h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x = (h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y

Tactic:
this

Goal state after:
case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : I.fst (y, x) ≫ c.π y = I.snd (y, x) ≫ c.π x
⊢ (h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x = (h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m = c.π i ≫ hc.desc (s.ofLinearOrder h)

Tactic:
this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m = (s.ofLinearOrder h).π i
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p

Tactic:
have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁

Goal state after:
case one
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: 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 • y) • z = x • y • z

Tactic:
[

Goal state after:
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 • y) • z = x • y • z
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:
[

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

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

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
s : Set α
t : Set β
⊢ s • -t = -(s • 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:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ -a • t = -(a • t)
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

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

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ -s • t = -(s • t)
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
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ p ↔ (algebraMap A B) x ∈ P

Tactic:
P.over_def p

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ under A P ↔ (algebraMap A B) x ∈ P
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
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤

Tactic:
P.over_def p

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ under A P = ⊤
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:
[

Goal state after:
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 𝔓
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
⊢ algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B 1) ⋯ = 1

Tactic:
by
    ext ⟨x⟩
    exact congrArg (Ideal.Quotient.mk P) (one_smul G x)

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 T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
⊢ x✝¹ ∈ S ⊓ T ∨ ∃ n, r✝ ^ n • ⊤ ≤ S ⊓ T

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
⊢ x✝¹ ∈ S ⊓ T ∨ ∃ n, r✝ ^ n • ⊤ ≤ S ⊓ T
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert.inl
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 i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (∅.inf f).IsPrimary
hi : i ∈ insert a ∅
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((insert a ∅).inf f).IsPrimary

Tactic:
simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs

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
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
x y : R
x✝ : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical

Tactic:
[

Goal state after:
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
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
x y : R
x✝ : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).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 ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
[

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 ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥
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 • map S.mkQ ⊤ = ⊥

Tactic:
[

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' : Submodule R M
m : M
hm : m ∈ ↑M'
⊢ f m ∈ ↑(localized' S p f M')

Tactic:
exact ⟨m, hm, 1, by simp⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ colon I Set.univ = I

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ colon I Set.univ = I
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ IsReduced S

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ IsReduced S
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ (Ideal.span {y}).IsRadical

Tactic:
[

Goal state after:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ (Ideal.span {y}).IsRadical
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R = ⊥ ↔ IsReduced R

Tactic:
[

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R = ⊥ ↔ IsReduced R