case intro
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
⊢ f b ≤ g b
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ f b ≤ g b
obtain ⟨c, hc⟩ : g b ∈ Set.range f := by
  rw [hfg]
  exact Set.mem_range_self b
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hcb : c < b
⊢ f b ≤ g b

case intro.inr
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ g b
case intro
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
⊢ f b ≤ g b
cases' lt_or_le c b with hcb hbc
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range g
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range f
rw [hfg]
no goals
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range g
exact Set.mem_range_self b
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : c < b
⊢ f b ≤ g b
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hcb : c < b
⊢ f b ≤ g b
rw [H c hcb] at hc
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : b < b
⊢ f b ≤ g b
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : c < b
⊢ f b ≤ g b
rw [hg.injective hc] at hcb
no goals
case intro.inl
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : b < b
⊢ f b ≤ g b
exact hcb.false.elim
case intro.inr
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ f c
case intro.inr
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ g b
rw [← hc]
no goals
case intro.inr
α : Type ?u.3596
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type u_2
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ f c
exact hf.monotone hbc