case h
α : Type ?u.4618
β : 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
a : β
⊢ f a = g a
α : Type ?u.4618
β : 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
⊢ f = g
funext a
case h
α : Type ?u.4618
β : 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
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
case h
α : Type ?u.4618
β : 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
a : β
⊢ f a = g a
apply h.induction a
no goals
case h
α : Type ?u.4618
β : 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
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
exact fun b H =>
  le_antisymm (eq_strictMono_iff_eq_range_aux hf hg hfg H)
    (eq_strictMono_iff_eq_range_aux hg hf hfg.symm fun a hab => (H a hab).symm)