case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), replicate = replicateTR
α : Type u
β : Type v
γ : Type w
⊢ @replicate = @replicateTR
apply funext
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ replicate = replicateTR
case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), replicate = replicateTR
intro α
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : Nat), replicate x = replicateTR x
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ replicate = replicateTR
apply funext
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
⊢ replicate n = replicateTR n
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : Nat), replicate x = replicateTR x
intro n
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
⊢ ∀ (x : α), replicate n x = replicateTR n x
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
⊢ replicate n = replicateTR n
apply funext
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
a : α
⊢ replicate n a = replicateTR n a
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
⊢ ∀ (x : α), replicate n x = replicateTR n x
intro a
no goals
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : Nat
a : α
⊢ replicate n a = replicateTR n a
exact (replicateTR_loop_replicate_eq _ 0 n).symm