case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
⊢ m ≤ n

case refine_2
α : Type u_1
m n : Nat
a : α
h : m ≤ n
⊢ replicate m a <+ replicate n a
α : Type u_1
m n : Nat
a : α
⊢ replicate m a <+ replicate n a ↔ m ≤ n
refine ⟨fun h => ?_, fun h => ?_⟩
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : length (replicate m a) ≤ length (replicate n a)
⊢ m ≤ n
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
⊢ m ≤ n
have := h.length_le
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : m ≤ n
⊢ m ≤ n
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : length (replicate m a) ≤ length (replicate n a)
⊢ m ≤ n
simp only [length_replicate] at this ⊢
no goals
case refine_1
α : Type u_1
m n : Nat
a : α
h : replicate m a <+ replicate n a
this : m ≤ n
⊢ m ≤ n
exact this
no goals
case refine_2
α : Type u_1
m n : Nat
a : α
h : m ≤ n
⊢ replicate m a <+ replicate n a
induction h with
| refl => apply Sublist.refl
| step => simp [*, replicate, Sublist.cons]
no goals
case refine_2.refl
α : Type u_1
m n : Nat
a : α
⊢ replicate m a <+ replicate m a
apply Sublist.refl
no goals
case refine_2.step
α : Type u_1
m n : Nat
a : α
m✝ : Nat
a✝ : Nat.le m m✝
a_ih✝ : replicate m a <+ replicate m✝ a
⊢ replicate m a <+ replicate (succ m✝) a
simp [*, replicate, Sublist.cons]