mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ (X : WalkingMulticospan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)

Tactic:
rintro (_ | _) <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
⊢ ∀ (X : WalkingMultispan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.left a✝, 𝟙 (WalkingMultispan.left a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.left a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝, 𝟙 (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    𝟙
      (match WalkingMultispan.right a✝ with
      | WalkingMultispan.left a => I.left a
      | WalkingMultispan.right b => I.right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
⊢ ∀ (X : WalkingMultispan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)

Tactic:
rintro (_ | _) <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
d : Cofan I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.sndSigmaMapOfIsColimit d hc = I.snd i ≫ d.inj (J.snd i)

Tactic:
by
  simp [sndSigmaMapOfIsColimit]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair), f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app j = (Multifork.toPiFork hc hd K₁).π.app j

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero

case one
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMulticospan J), f.hom ≫ (Multifork.ofPiFork K₂).π.app j = (Multifork.ofPiFork K₁).π.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.L
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.left a✝) =
    (Multifork.ofPiFork K₁).π.app (WalkingMulticospan.left a✝)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a✝ : J.R
⊢ f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.right a✝) =
    (Multifork.ofPiFork K₁).π.app (WalkingMulticospan.right a✝)
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
⊢ { l //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
by
    have h₁ : s.ι.f ≫ (T : C ⥤ C).map X.a = s.ι.f ≫ T.δ.app X.A :=
      congr_arg Comonad.Coalgebra.Hom.f s.condition
    have h₂ : s.pt.a ≫ (T : C ⥤ C).map s.ι.f = s.ι.f ≫ T.δ.app X.A := s.ι.h
    refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
    · dsimp
      rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]
      dsimp
      rw [Category.comp_id, Category.assoc, ← T.counit_naturality,
        reassoc_of% h₁, Comonad.left_counit]
      simp
    · ext
      simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using! h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A)
    · intro m hm
      ext
      dsimp only
      rw [← hm]
      simp [beckCoalgebraFork, X.counit]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Multifork I
⊢ ∀ (j : WalkingMulticospan J),
    ((𝟭 (Multifork I)).obj K).π.app j =
      (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫ ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Multifork I
a✝ : J.L
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.left a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.left a✝)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K : Multifork I
a✝ : J.R
⊢ ((𝟭 (Multifork I)).obj K).π.app (WalkingMulticospan.right a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.right 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
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ ∀ (j : WalkingMultispan J), K.ι.app j ≫ f = K.ι.app j ≫ g

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a✝ : J.L
⊢ K.ι.app (WalkingMultispan.left a✝) ≫ f = K.ι.app (WalkingMultispan.left a✝) ≫ g

case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a✝ : J.R
⊢ K.ι.app (WalkingMultispan.right a✝) ≫ f = K.ι.app (WalkingMultispan.right a✝) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair),
    (Multicofork.toSigmaCofork hc hd K₁).ι.app j ≫ f.hom = (Multicofork.toSigmaCofork hc hd K₂).ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero

case one
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMultispan J), (Multicofork.ofSigmaCofork K₁).ι.app j ≫ f.hom = (Multicofork.ofSigmaCofork K₂).ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
a✝ : J.L
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.left a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.left a✝)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
a✝ : J.R
⊢ (Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.right a✝) ≫ f.hom =
    (Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.right 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
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Multicofork I
⊢ ∀ (j : WalkingMultispan J),
    ((𝟭 (Multicofork I)).obj K).ι.app j ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
      ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Multicofork I
a✝ : J.L
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.left a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.left a✝)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K : Multicofork I
a✝ : J.R
⊢ ((𝟭 (Multicofork I)).obj K).ι.app (WalkingMultispan.right a✝) ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.right a✝)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

Tactic:
· dsimp
        rw [← F.map_comp, homOfLE_comp]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯) ≫ app' (eqToIso h).hom 0 ⋯ =
    (eqToIso h₀).hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
dsimp [app']

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯) ≫ (eqToHom h).app 0 = eqToHom h₀ ≫ G.map (homOfLE ⋯)
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
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
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm n • x = n • x

Tactic:
by
  rw [← (inertiaEquiv I e he).apply_symm_apply n, inertiaEquiv_apply_smul,
    (inertiaEquiv I e he).apply_symm_apply]

Goal state after:
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:
ext ⟨x⟩

Goal state after:
case mk
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
a✝ : B ⧸ P
x : B
⊢ (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B 1) ⋯) (Quot.mk (⇑(quotientRel P)) x) =
    1 (Quot.mk (⇑(quotientRel P)) x)
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
g h : ↥(MulAction.stabilizer G P)
⊢ algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B (g * h)) ⋯ =
    algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B g) ⋯ * algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B h) ⋯

Tactic:
ext ⟨x⟩

Goal state after:
case mk
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
g h : ↥(MulAction.stabilizer G P)
a✝ : B ⧸ P
x : B
⊢ (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B (g * h)) ⋯) (Quot.mk (⇑(quotientRel P)) x) =
    (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B g) ⋯ *
        algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B h) ⋯)
      (Quot.mk (⇑(quotientRel P)) x)
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
⊢ Ideal.comap φ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ Ideal.comap φ I → x ∈ Ideal.comap φ I ∨ y ∈ (Ideal.comap φ I).radical

Tactic:
refine hI.imp (comap_ne_top φ) fun h ↦ ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ ∀ {x y : R}, x * y ∈ Ideal.comap φ I → x ∈ Ideal.comap φ I ∨ y ∈ (Ideal.comap φ 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 • ⊤ ≤ comap S.mkQ ⊥

Tactic:
comap_bot,

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 • ⊤ ≤ S.mkQ.ker
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
P : Submodule R M
r s : R
hr : r ∈ N.colon ↑P
p : M
hp : p ∈ (r * s) • ↑P
⊢ p ∈ ↑N

Tactic:
obtain ⟨p, hp, rfl⟩ := hp
    exact hr ⟨_, P.smul_mem _ hp, (mul_smul ..).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: 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⁻¹
⊢ (Ideal.Quotient.mk I) (x * y) = (Ideal.Quotient.mk I) 1

Tactic:
rw [map_one, map_mul, hy, IsUnit.mul_val_inv]

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)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
⊢ m ∈ N

Tactic:
let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)

Goal state after:
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)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N
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
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
⊢ m ∈ N

Tactic:
let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N
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
I I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' →
    I ≤ I'

pp: case mpr
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 I' : { p // p.IsPrime }
⊢ I ≤ I' →
    { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I'

Tactic:
· exact fun h => show I.val ≤ I'.val from map_under M S I.val ▸
        map_under M S I'.val ▸ Ideal.map_mono h

Goal state after:
case mpr
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 I' : { p // p.IsPrime }
⊢ I ≤ I' →
    { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I'