-- Mathlib/RingTheory/Henselian.lean
theorem isLocalHom_of_le_jacobson_bot {R : Type*} [CommRing R] (I : Ideal R)
    (h : I ≤ Ideal.jacobson ⊥) : IsLocalHom (Ideal.Quotient.mk I)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : a * b - 1 ∈ I
⊢ a * b - 1 ∈ ⊥.jacobson

Tactic:
exact h hb

Result:
no goals

Proof state:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) y = 1
h2 : (Ideal.Quotient.mk ⊥.jacobson) y * (Ideal.Quotient.mk ⊥.jacobson) a = 1
⊢ IsUnit a

Tactic:
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
  Ideal.mem_jacobson_bot] at h1 h2

Result:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a

Proof state:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
this : IsUnit ((Ideal.Quotient.mk ⊥.jacobson) a)
⊢ IsUnit a

Tactic:
obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this

Result:
case map_nonunit.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R ⧸ ⊥.jacobson
h1 : (Ideal.Quotient.mk ⊥.jacobson) a * y = 1
h2 : y * (Ideal.Quotient.mk ⊥.jacobson) a = 1
⊢ IsUnit a

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) b = 1

Tactic:
rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢

Result:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : a * b - 1 ∈ I
⊢ a * b - 1 ∈ ⊥.jacobson

Proof state:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Tactic:
exact h1.1

Result:
no goals

Proof state:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
⊢ IsUnit a

Tactic:
have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) := by
  rw [isUnit_iff_exists_inv] at *
  obtain ⟨b, hb⟩ := h
  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
  use Ideal.Quotient.mk _ b
  rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
  exact h hb

Result:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
this : IsUnit ((Ideal.Quotient.mk ⊥.jacobson) a)
⊢ IsUnit a

Proof state:
case map_nonunit.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R ⧸ ⊥.jacobson
h1 : (Ideal.Quotient.mk ⊥.jacobson) a * y = 1
h2 : y * (Ideal.Quotient.mk ⊥.jacobson) a = 1
⊢ IsUnit a

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Result:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) y = 1
h2 : (Ideal.Quotient.mk ⊥.jacobson) y * (Ideal.Quotient.mk ⊥.jacobson) a = 1
⊢ IsUnit a

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
⊢ IsUnit ((Ideal.Quotient.mk ⊥.jacobson) a)

Tactic:
rw [isUnit_iff_exists_inv] at *

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : ∃ b, (Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a : R
b : R ⧸ I
hb : (Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Tactic:
obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Proof state:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a

Tactic:
simp? at h1 says simp only [mul_one, sub_add_cancel, IsUnit.mul_iff] at h1

Result:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Tactic:
use Ideal.Quotient.mk _ b

Result:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) b = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ IsLocalHom (Ideal.Quotient.mk I)

Tactic:
constructor

Result:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ ∀ (a : R), IsUnit ((Ideal.Quotient.mk I) a) → IsUnit a

Proof state:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a

Tactic:
simp only [mul_one, sub_add_cancel, IsUnit.mul_iff] at h1

Result:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Proof state:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ ∀ (a : R), IsUnit ((Ideal.Quotient.mk I) a) → IsUnit a

Tactic:
intro a h

Result:
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
⊢ IsUnit a

Proof state:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a

Tactic:
specialize h1 1

Result:
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : ∃ b, (Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1

Tactic:
obtain ⟨b, hb⟩ := h

Result:
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a : R
b : R ⧸ I
hb : (Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, (Ideal.Quotient.mk ⊥.jacobson) a * b = 1