Theorem: List.getD_ext (One.lean)

State before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ a = b
Tactic:
apply List.ext
State after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ ∀ (n : ℕ), get? a n = get? b n

State before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ ∀ (n : ℕ), get? a n = get? b n
Tactic:
intro n
State after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
⊢ get? a n = get? b n

State before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
⊢ get? a n = get? b n
Tactic:
have h:= Q n
State after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : getD a n d = getD b n d
⊢ get? a n = get? b n

State before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : getD a n d = getD b n d
⊢ get? a n = get? b n
Tactic:
unfold getD at h
State after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
⊢ get? a n = get? b n

State before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
⊢ get? a n = get? b n
Tactic:
cases hlt: decide (n < List.length a) with
| true => 
  simp only [decide_eq_true_eq] at hlt
  have hltb: n < length b := by rw [← P]; exact hlt
  simp_all only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hltb, get?_eq_get, Option.getD_some, gt_iff_lt, P] 
| false =>
   simp only [decide_eq_false_iff_not, not_lt] at hlt
   have hltb: n ≥ length b := by rw [← P]; exact hlt
   simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2, hltb]
State after:
no goals

State before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : decide (n < length a) = true
⊢ get? a n = get? b n
Tactic:
simp only [decide_eq_true_eq] at hlt
State after:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ get? a n = get? b n

State before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ get? a n = get? b n
Tactic:
have hltb: n < length b := by rw [← P]; exact hlt
State after:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
hltb : n < length b
⊢ get? a n = get? b n

State before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
hltb : n < length b
⊢ get? a n = get? b n
Tactic:
simp_all only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hltb, get?_eq_get, Option.getD_some, gt_iff_lt, P]
State after:
no goals

State before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length b
Tactic:
rw [← P]
State after:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length a

State before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length a
Tactic:
exact hlt
State after:
no goals

State before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : decide (n < length a) = false
⊢ get? a n = get? b n
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at hlt
State after:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ get? a n = get? b n

State before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ get? a n = get? b n
Tactic:
have hltb: n ≥ length b := by rw [← P]; exact hlt
State after:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
hltb : n ≥ length b
⊢ get? a n = get? b n

State before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
hltb : n ≥ length b
⊢ get? a n = get? b n
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2, hltb]
State after:
no goals

State before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length b
Tactic:
rw [← P]
State after:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length a

State before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length a
Tactic:
exact hlt
State after:
no goals