-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma iSup_iInf_eq (f : ∀ i, κ i → α) :
    let _ := minAx.toCompleteLattice
    ⨆ i, ⨅ j, f i j = ⨅ g : ∀ i, κ i, ⨆ i, f i (g i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Tactic:
refine le_trans ?_ (le_iSup _ a)

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨅ j, f a j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
b : κ a
⊢ ⨅ i, f (g i) (i (g i)) ≤ f a b

Tactic:
obtain ⟨h, rfl, rfl⟩ := ha b

Result:
case intro.intro
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (i : ι) → κ i
ha : ∀ (b : κ (g h)), ∃ f, ∃ (h_1 : g h = g f), h_1 ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ f (g h) (h (g h))

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
⊢ False

Tactic:
have := hh _ h rfl

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
this : ⋯ ▸ h (g h) ≠ h (g h)
⊢ False

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Tactic:
have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) := of_not_not fun h => by
  push_neg at h
  choose h hh using h
  have := hh _ h rfl
  contradiction

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
this : ⋯ ▸ h (g h) ≠ h (g h)
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨅ g, ⨆ i, f i (g i) ≤ ⨆ i, ⨅ j, f i j

Tactic:
rw [minAx.iInf_iSup_eq']

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨆ g, ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : ∀ (a : ι), ∃ b, ∀ (f : (i : ι) → κ i) (h : a = g f), h ▸ b ≠ f (g f)
⊢ False

Tactic:
choose h hh using h

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
⊢ False

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨆ g, ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Tactic:
refine iSup_le fun g => ?_

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : ¬∃ a, ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ False

Tactic:
push_neg at h

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : ∀ (a : ι), ∃ b, ∀ (f : (i : ι) → κ i) (h : a = g f), h ▸ b ≠ f (g f)
⊢ False

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
⊢ let x := minAx.toCompleteLattice;
  ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)

Tactic:
let _ := minAx.toCompleteLattice

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨅ j, f a j

Tactic:
refine le_iInf fun b => ?_

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
b : κ a
⊢ ⨅ i, f (g i) (i (g i)) ≤ f a b

Proof state:
case intro.intro
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : ((i : ι) → κ i) → ι
h : (i : ι) → κ i
ha : ∀ (b : κ (g h)), ∃ f, ∃ (h_1 : g h = g f), h_1 ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ f (g h) (h (g h))

Tactic:
exact iInf_le _ _

Result:
no goals

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)

Tactic:
refine le_antisymm iSup_iInf_le ?_

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨅ g, ⨆ i, f i (g i) ≤ ⨆ i, ⨅ j, f i j