mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single 1 r)

pp: case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑X✝),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single m 1)

Tactic:
<;>

Goal state after:
case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single 1 r)

case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑X✝),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single m 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
r✝ : ↑R
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single 1 r✝)

pp: case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m✝ : ↑X✝
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single m✝ 1)

Tactic:
<;>

Goal state after:
case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
r✝ : ↑R
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m✝ : ↑X✝
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single m✝ 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
G : CommMonCat
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r)

pp: case h_of
R : CommRingCat
G : CommMonCat
⊢ ∀ (m : ↑G),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single m 1) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m 1)

Tactic:
<;>

Goal state after:
case h₁
R : CommRingCat
G : CommMonCat
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r)

case h_of
R : CommRingCat
G : CommMonCat
⊢ ∀ (m : ↑G),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single m 1) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
G : CommMonCat
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r✝)

pp: case h_of
R : CommRingCat
G : CommMonCat
m✝ : ↑G
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m✝ 1)

Tactic:
<;>

Goal state after:
case h₁
R : CommRingCat
G : CommMonCat
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
G : CommMonCat
m✝ : ↑G
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m✝ 1)
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
| comap f (sInf {m | IsCoatom m})

Tactic:
sInf_eq_iInf',

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
| comap f (⨅ a, ↑a)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
by
  have h_left' {x y} (hy : y ∈ closure s) : x * y ∈ closure s := by
    have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
    refine closure_mono ?_ this
    rintro - ⟨y, hy, rfl⟩
    exact h_left x y hy
  have h_right' {y x} (hy : y ∈ closure s) : y * x ∈ closure s := by
    have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
    refine closure_mono ?_ this
    rintro - ⟨y, hy, rfl⟩
    exact h_right y x hy
  let I : TwoSidedIdeal R := .mk' (closure s) (AddSubgroup.zero_mem _)
    (AddSubgroup.add_mem _) (AddSubgroup.neg_mem _) h_left' h_right'
  suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]
  rw [mem_span_iff]
  -- Suppose that for every ideal `J` with `s ⊆ J`, then `z ∈ J`. Apply this to `I` to get `z ∈ I`.
  refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩
  case mem_closure_of_forall => simpa only [I, SetLike.mem_coe, mem_mk'] using subset_closure hx
  /- Conversely, suppose that `z ∈ I` and that `J` is any ideal containing `s`. Then by the
  induction principle for `AddSubgroup`, we must also have `z ∈ J`. -/
  case mem_ideal_of_subset =>
    simp only [I, SetLike.mem_coe, mem_mk'] at hz
    induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ ⨅ a, ↑a
| map f (sInf {m | IsCoatom m})

Tactic:
sInf_eq_iInf',

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ ⨅ a, ↑a
| map f (⨅ a, ↑a)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
· refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
        simp [mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case fst
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).1 = (1, 0).1

pp: case snd
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).2 = (1, 0).2

Tactic:
<;>

Goal state after:
case fst
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).1 = (1, 0).1

case snd
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).2 = (1, 0).2
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case fst
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).1 = (0, 1).1

pp: case snd
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).2 = (0, 1).2

Tactic:
<;>

Goal state after:
case fst
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).1 = (0, 1).1

case snd
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝⁵ : CommSemiring S✝
inst✝⁴ : Algebra R✝ S✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).2 = (0, 1).2
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ sInf {m | IsCoatom m} ≤ ⨅ i, comap (LinearMap.proj i) (sInf {m | IsCoatom m})

Tactic:
sInf_eq_iInf',

Goal state after:
R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ ⨅ a, ↑a ≤ ⨅ i, comap (LinearMap.proj i) (⨅ a, ↑a)
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * a) → IsUnit a

pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * b) → IsUnit b

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * a) → IsUnit a

R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * b) → IsUnit b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b x : R
hx : f x = 0
n : ℕ
hn : a ^ n * x = 0
⊢ ∃ n, (a * b) ^ n * x = 0

Tactic:
exact ⟨n, by simp [mul_pow, mul_assoc, mul_left_comm (a ^ n), hn]⟩

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : ¬¬IsUnit x
H : x ∈ I
⊢ 1 ∈ I

Tactic:
Classical.not_not

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
⊢ 1 ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZPow x B (-d) * selfZPow x B d = 1

Tactic:
rw [mul_comm, selfZPow_mul_neg x B d]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv ≫ (M ⊗ N) ◁ (η ⊗ₘ η) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (ρ_ (M ⊗ N)).hom

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_right]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv ≫ (tensorμ M N (𝟙_ C) (𝟙_ C) ≫ (M ◁ η ⊗ₘ N ◁ η)) ≫ (μ ⊗ₘ μ) = (ρ_ (M ⊗ N)).hom
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ∑ x, f (fg (Sum.inl ↑x) • v ↑x) = ∑ x, f (fg (Sum.inr ↑x) • v ↑x)
⊢ g₁ i = g₂ i

Tactic:
← map_sum,

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : f (∑ x, fg (Sum.inl ↑x) • v ↑x) = f (∑ x, fg (Sum.inr ↑x) • v ↑x)
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
⊢ ∃ w, LinearIndependent R w

Tactic:
use fun i ↦ (sec (v i)).1

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
⊢ LinearIndependent R fun i ↦ (sec (v i)).1