mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
      (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
      ↑(TensorProduct.rid R M)

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
          (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        x✝)
      1 =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
          ↑(TensorProduct.rid R M))
        x✝)
      1
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ (comap e.symm).comp (comap e) = OrderHom.id

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal S
x✝ : S
⊢ x✝ ∈ ((comap e.symm).comp (comap e)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ (comap e).comp (comap e.symm) = OrderHom.id

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ ((comap e).comp (comap e.symm)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
⊢ (comap f) ((comap g) I) = (comap (g.comp f)) I

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x✝ : R
⊢ x✝ ∈ (comap f) ((comap g) I) ↔ x✝ ∈ (comap (g.comp f)) I
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case mem
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
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
x : R
hx : x ∈ s
⊢ x ∈ J

Tactic:
exact hJ hx

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

Goal state before:
pp: 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 := (RingHom.fst R S).toAlgebra
⊢ IsIdempotentElem (1, 0)

Tactic:
ext

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.Jacobson.Radical

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ jacobson R (M ⧸ jacobson R M) = ⊥

Tactic:
jacobson_quotient_of_le le_rfl,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ map (jacobson R M).mkQ (jacobson R M) = ⊥
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: 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 := (RingHom.snd R S).toAlgebra
⊢ IsIdempotentElem (0, 1)

Tactic:
ext

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.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ (TwoSidedIdeal.asIdeal I).toTwoSided = I

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided ↔ x✝ ∈ I
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ TwoSidedIdeal.asIdeal I.toTwoSided = I

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ TwoSidedIdeal.asIdeal I.toTwoSided ↔ x✝ ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I → ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.jacobson = I ↔ ⊥.jacobson = ⊥

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.jacobson = I → ⊥.jacobson = ⊥

case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.jacobson = ⊥ → I.jacobson = I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson → ⊥.radical = ⊥.jacobson

case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.radical = ⊥.jacobson → I.radical = I.jacobson
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ asIdeal I.jacobson = (asIdeal I).jacobson

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 4 → 1 := fun h ↦ ⟨fun x => not_imp_not.1 (@h x)⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝ : IsLocalHom f
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝¹ : IsLocalHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J

Tactic:
constructor

Goal state after:
case left
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ 1 ∉ maximalIdeal R

case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ (Units.map ↑f) ⋯.unit = a

Tactic:
ext

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ↑((Units.map ↑f) ⋯.unit) = ↑a
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : IsLocalRing R
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalHom f := IsLocalHom.of_surjective f hf
⊢ Ideal.map f (maximalIdeal R) = maximalIdeal S

Tactic:
← maximalIdeal_comap f,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : IsLocalRing R
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalHom f := IsLocalHom.of_surjective f hf
⊢ Ideal.map f (Ideal.comap f (maximalIdeal S)) = maximalIdeal S
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
              naturality := ⋯ } } =
    𝟙 (limit F)

Tactic:
ext

Goal state after:
case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
        limit.lift F
          { pt := F.1 i,
            π :=
              { app := fun j ↦ if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j),
                naturality := ⋯ } }) ≫
      limit.π F j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case e_y
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
hm : m < 0
⊢ Submonoid.pow x (n.natAbs + m.natAbs) = Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs

Tactic:
ext

Goal state after:
case e_y
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
hm : m < 0
⊢ ↑(Submonoid.pow x (n.natAbs + m.natAbs)) = ↑(Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs)
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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
constructor

Goal state after:
case mp
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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b → selfZPow x B m * mk' B a 1 = selfZPow x B d * b

case mpr
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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b → selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ ((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom =
    (α_ X X X).hom ≫ X ◁ ((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom

Tactic:
by simpa [← id_tensorHom, ← tensorHom_id,
      -associator_conjugation, associator_naturality_assoc] using
      congr(((e.inv ⊗ₘ e.inv) ⊗ₘ e.inv) ≫ $(MonObj.mul_assoc M) ≫ e.hom)

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: 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
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
i j : ↥s
h : integerMultiple M s f i = integerMultiple M s f j
⊢ f ↑i = f ↑j

Tactic:
← (IsLocalization.smul_bijective S (commonDenom M s f)).injective.eq_iff,

Goal state after:
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
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
i j : ↥s
h : integerMultiple M s f i = integerMultiple M s f j
⊢ commonDenom M s f • f ↑i = commonDenom M s f • f ↑j
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: 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
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach = commonDenomOfFinset M s • ↑s

Tactic:
ext

Goal state after:
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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach ↔ x✝ ∈ commonDenomOfFinset M s • ↑s
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: 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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach ↔ x✝ ∈ commonDenomOfFinset M s • ↑s

Tactic:
constructor

Goal state after:
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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach → x✝ ∈ commonDenomOfFinset M s • ↑s

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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s → x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach
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
b : Basis ι R M
⊢ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) = ⇑f '' Set.range ⇑b

Tactic:
ext

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
b : Basis ι R M
x✝ : Mₛ
⊢ x✝ ∈ Set.range ⇑(ofIsLocalizedModule Rₛ S f b) ↔ x✝ ∈ ⇑f '' Set.range ⇑b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ f = { hom := η, isMonHom_hom := ⋯ }

Tactic:
ext

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ f.hom = { hom := η, isMonHom_hom := ⋯ }.hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O X : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
ext

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
M N O X : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Mon C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝ y✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (x✝ + y✝) =
    extendScalarsOfIsLocalization S A x✝ + extendScalarsOfIsLocalization S A y✝

Tactic:
ext

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
x✝¹ y✝ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (x✝¹ + y✝)) x✝ =
    (extendScalarsOfIsLocalization S A x✝¹ + extendScalarsOfIsLocalization S A y✝) x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝ : M →ₗ[R] N
⊢ extendScalarsOfIsLocalization S A (m✝ • x✝) = (RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝

Tactic:
ext

Goal state after:
R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
m✝ : A
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (extendScalarsOfIsLocalization S A (m✝ • x✝¹)) x✝ = ((RingHom.id A) m✝ • extendScalarsOfIsLocalization S A x✝¹) x✝