-- Mathlib/Order/Atoms.lean
theorem isAtom_iff {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] :
    IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ j, j ≠ i → f j = ⊥

Proof state:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < f k
hki : ¬i = k
⊢ False

Tactic:
rw [hbot _ (Ne.symm hki)] at hgfk

Result:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < ⊥
hki : ¬i = k
⊢ False

Proof state:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : k = j
⊢ Function.update ⊥ j (f j) k ≤ f k

case neg
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : ¬k = j
⊢ Function.update ⊥ j (f j) k ≤ f k

Tactic:
{ subst h; simp }

Result:
case neg
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : ¬k = j
⊢ Function.update ⊥ j (f j) k ≤ f k

Proof state:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

Tactic:
constructor

Result:
case mp
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f → ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

case mpr
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ (∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥) → IsAtom f

Proof state:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
k : ι
hgfk : g k < f k
⊢ g j = ⊥

Tactic:
obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk; simp at hgfk

Result:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
⊢ g j = ⊥

Proof state:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this :
  (∀ (i_1 : ι), Function.update ⊥ i b i_1 ≤ f i_1) →
    ∀ (x : ι), Function.update ⊥ i b x < f x → ∀ (i_1 : ι), Function.update ⊥ i b i_1 = ⊥
j : ι
h : j = i
⊢ Function.update ⊥ i b j ≤ f j

Tactic:
subst h

Result:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
j : ι
hbot : f j ≠ ⊥
b : π j
hb : b < f j
this :
  (∀ (i : ι), Function.update ⊥ j b i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j b x < f x → ∀ (i : ι), Function.update ⊥ j b i = ⊥
⊢ Function.update ⊥ j b j ≤ f j

Proof state:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
⊢ b = ⊥

Tactic:
have := h (Function.update ⊥ i b)

Result:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
b : π i
hb : b < f i
this : Function.update ⊥ i b < f → Function.update ⊥ i b = ⊥
⊢ b = ⊥

Proof state:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h✝ : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
j : ι
hj : j ≠ i
this :
  (∀ (i : ι), Function.update ⊥ j (f j) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ j (f j) x < f x → ∀ (i : ι), Function.update ⊥ j (f j) i = ⊥
k : ι
h : k = j
⊢ Function.update ⊥ j (f j) k ≤ f k

Tactic:
subst h

Result:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
k : ι
hj : k ≠ i
this :
  (∀ (i : ι), Function.update ⊥ k (f k) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ k (f k) x < f x → ∀ (i : ι), Function.update ⊥ k (f k) i = ⊥
⊢ Function.update ⊥ k (f k) k ≤ f k

Proof state:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
⊢ IsAtom f

Tactic:
refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩

Result:
case intro.intro.intro
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf : g < f
j : ι
⊢ g j = ⊥

Proof state:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
i : ι
hbot : ∀ (j : ι), j ≠ i → f j = ⊥
hfi : f i ≠ ⊥
hlt : ∀ b < f i, b = ⊥
g : (i : ι) → π i
hgf✝ : g < f
j : ι
hgf : g ≤ f
hgfk : g i < f i
hij : ¬j = i
⊢ g j = ⊥

Tactic:
exact eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))

Result:
no goals

Proof state:
case pos
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
k : ι
hj : k ≠ i
this :
  (∀ (i : ι), Function.update ⊥ k (f k) i ≤ f i) →
    ∀ (x : ι), Function.update ⊥ k (f k) x < f x → ∀ (i : ι), Function.update ⊥ k (f k) i = ⊥
⊢ Function.update ⊥ k (f k) k ≤ f k

Tactic:
simp

Result:
no goals

Proof state:
case intro
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

Tactic:
refine ⟨i, ⟨hbot, ?c⟩, ?d⟩

Result:
case c
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ b < f i, b = ⊥

case d
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
hbot✝ : f ≠ ⊥
h : ∀ b < f, b = ⊥
i : ι
hbot : f i ≠ ⊥
⊢ ∀ (j : ι), j ≠ i → f j = ⊥