Theorem: List.remap_remap (MLIR/Util/List.lean)

State before:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
h_g : ∀ (n : ℕ), n < length (remap l f h_f) → g n < length (remap l f h_f)
n : ℕ
h : n < length l
⊢ Function.comp f g n < length l
Tactic:
simp [Function.comp] at *
State after:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ f (g n) < length l

State before:
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ f (g n) < length l
Tactic:
apply h_f
State after:
case a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ g n < length l

State before:
case a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ g n < length l
Tactic:
apply h_g
State after:
case a.a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ n < length l

State before:
case a.a
α : Type ?u.31376
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
n : ℕ
h : n < length l
h_g : ∀ (n : ℕ), n < length l → g n < length l
⊢ n < length l
Tactic:
apply h
State after:
no goals

State before:
α : Type u_1
l : List α
f : ℕ → ℕ
h_f : ∀ (n : ℕ), n < length l → f n < length l
g : ℕ → ℕ
h_g : ∀ (n : ℕ), n < length (remap l f h_f) → g n < length (remap l f h_f)
⊢ remap (remap l f h_f) g h_g = remap l (f ∘ g) (_ : ∀ (n : ℕ), n < length l → Function.comp f g n < length l)
Tactic:
apply extF <;> simp
State after:
no goals