-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem chain_apply [∀ x, PartialOrder (β x)] {c : (∀ x, β x) → Prop} (hc : chain c) (x : α) :
    chain (fun y => ∃ f, c f ∧ f x = y)

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
⊢ chain fun y => ∃ f, c f ∧ f x = y

Tactic:
intro _ _ ⟨f, hf, hfeq⟩ ⟨g, hg, hgeq⟩

Result:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
x✝ y✝ : β x
f : (x : α) → β x
hf : c f
hfeq : f x = x✝
g : (x : α) → β x
hg : c g
hgeq : g x = y✝
⊢ x✝ ⊑ y✝ ∨ y✝ ⊑ x✝

Proof state:
case h
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : g ⊑ f
⊢ g x ⊑ f x

Tactic:
apply h x

Result:
no goals

Proof state:
case inl
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : f ⊑ g
⊢ f x ⊑ g x ∨ g x ⊑ f x

case inr
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : g ⊑ f
⊢ f x ⊑ g x ∨ g x ⊑ f x

Tactic:
next h => left; apply h x

Result:
case inr
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : g ⊑ f
⊢ f x ⊑ g x ∨ g x ⊑ f x

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : g ⊑ f
⊢ f x ⊑ g x ∨ g x ⊑ f x

Tactic:
right

Result:
case h
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : g ⊑ f
⊢ g x ⊑ f x

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
y✝ : β x
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
hgeq : g x = y✝
⊢ f x ⊑ y✝ ∨ y✝ ⊑ f x

Tactic:
subst hgeq

Result:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
⊢ f x ⊑ g x ∨ g x ⊑ f x

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
⊢ f x ⊑ g x ∨ g x ⊑ f x

Tactic:
cases hc f g hf hg

Result:
case inl
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : f ⊑ g
⊢ f x ⊑ g x ∨ g x ⊑ f x

case inr
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : g ⊑ f
⊢ f x ⊑ g x ∨ g x ⊑ f x

Proof state:
case h
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : f ⊑ g
⊢ f x ⊑ g x

Tactic:
apply h x

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : f ⊑ g
⊢ f x ⊑ g x ∨ g x ⊑ f x

Tactic:
left

Result:
case h
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h : f ⊑ g
⊢ f x ⊑ g x

Proof state:
case inr
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
h✝ : g ⊑ f
⊢ f x ⊑ g x ∨ g x ⊑ f x

Tactic:
next h => right; apply h x

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
x✝ y✝ : β x
f : (x : α) → β x
hf : c f
hfeq : f x = x✝
g : (x : α) → β x
hg : c g
hgeq : g x = y✝
⊢ x✝ ⊑ y✝ ∨ y✝ ⊑ x✝

Tactic:
subst hfeq

Result:
α : Sort u
β : α → Sort v
inst✝ : (x : α) → PartialOrder (β x)
c : ((x : α) → β x) → Prop
hc : chain c
x : α
y✝ : β x
f : (x : α) → β x
hf : c f
g : (x : α) → β x
hg : c g
hgeq : g x = y✝
⊢ f x ⊑ y✝ ∨ y✝ ⊑ f x