mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
finset_eq : ∃ t, ↑t = s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

pp: case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
·

Goal state after:
case refine_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
·

Goal state after:
case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal} → x ∈ I

Tactic:
exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪

pp: case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
·

Goal state after:
case pos
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪
Module: Mathlib.RingTheory.Jacobson.Ideal

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
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
⊢ I.jacobson = I ↔ ⊥.jacobson = ⊥

Tactic:
by
  have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
  constructor
  · intro h
    replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
    rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
    simpa using h
  · intro h
    replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
    rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
    simpa using h

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

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

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

Tactic:
·

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
Module: Mathlib.RingTheory.Jacobson.Ideal

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

Tactic:
·

Goal state after:
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.LocalRing.MaximalIdeal.Basic

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

pp: 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

Tactic:
·

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
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
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J

Tactic:
·

Goal state after:
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: 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
tfae_1_to_5 : IsLocalHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
tfae_5_to_4 : Ideal.comap f (maximalIdeal S) = maximalIdeal R → 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_finish

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

Goal state before:
pp: case refine_1
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)
⊢ (X : J) → ((Functor.const J).obj (F.1 i)).obj X ⟶ F.obj X

pp: case refine_2
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)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj (F.1 i)).map f ≫ ?refine_1 Y = ?refine_1 X ≫ F.map f

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 := ?refine_1, naturality := ?refine_2 } } = 𝟙 (limit F)

pp: case refine_4
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.lift F { pt := F.1 i, π := { app := ?refine_1, naturality := ?refine_2 } } ≫ limit.π F i = 𝟙 (F.obj i)

Tactic:
·

Goal state after:
case refine_1
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)
⊢ (X : J) → ((Functor.const J).obj (F.1 i)).obj X ⟶ F.obj X
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
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)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f

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 := ?refine_2 } } =
    𝟙 (limit F)

pp: case refine_4
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.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 := ?refine_2 } } ≫
      limit.π F i =
    𝟙 (F.obj i)

Tactic:
·

Goal state after:
case refine_2
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)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
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 : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

pp: case neg
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 : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
·

Goal state after:
case pos
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 : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
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 : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
·

Goal state after:
case neg
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 : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos
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 k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f

pp: case neg
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 k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

pp: case pos
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 k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

pp: case neg
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 k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
·

Goal state after:
case pos
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 k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map f
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
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 : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

pp: case neg
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 : ℕ
h : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
·

Goal state after:
case pos
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 : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
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 : ℕ
h : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
·

Goal state after:
case neg
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 : ℕ
h : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case neg
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 k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

pp: case pos
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 k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) = eqToHom ⋯ ≫ F.map f

pp: case neg
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 k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ (H k h).from (((Functor.const J).obj (F.1 i)).obj k) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
·

Goal state after:
case neg
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 k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl.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
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inl.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 : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.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 : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.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
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
·

Goal state after:
case inl.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
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl.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 : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.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 : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

pp: case inr.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
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
·

Goal state after:
case inl.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 : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m