-- Mathlib/Order/Atoms.lean
theorem isAtom_iff_eq_single [DecidableEq ι] [∀ i, PartialOrder (π i)]
    [∀ i, OrderBot (π i)] {f : ∀ i, π i} :
    IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h : IsAtom f
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Tactic:
have ⟨i, h, hbot⟩ := isAtom_iff.1 h

Result:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Proof state:
case mpr
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f

Tactic:
case mpr =>
  rintro ⟨i, a, h, rfl⟩
  exact isAtom_single h

Result:
no goals

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Tactic:
constructor

Result:
case mp
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

case mpr
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Tactic:
refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩

Result:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
j : ι
hij : ¬j = i
⊢ f j = Function.update ⊥ i (f i) j

Proof state:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
a : π i
h : IsAtom a
⊢ IsAtom (Function.update ⊥ i a)

Tactic:
exact isAtom_single h

Result:
no goals

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
j : ι
hij : j = i
⊢ f j = Function.update ⊥ j (f j) j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f

Tactic:
rintro ⟨i, a, h, rfl⟩

Result:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
a : π i
h : IsAtom a
⊢ IsAtom (Function.update ⊥ i a)

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Tactic:
intro h

Result:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h : IsAtom f
⊢ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Proof state:
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
h✝ : IsAtom f
i : ι
h : IsAtom (f i)
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
j : ι
hij : ¬j = i
⊢ f j = Function.update ⊥ i (f i) j

Tactic:
rw [Function.update_of_ne hij, hbot _ hij, bot_apply]

Result:
no goals

Proof state:
case mp
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

case mpr
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f

Tactic:
case mp =>
  intro h
  have ⟨i, h, hbot⟩ := isAtom_iff.1 h
  refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩
  rw [Function.update_of_ne hij, hbot _ hij, bot_apply]

Result:
case mpr
ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f