Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
import Mathlib.Tactic.Linarith.Frontend
import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.ClearExcept
import Mathlib.Data.List.Basic
import Mathlib.Data.String.Lemmas

/-!
## Basic lemmas about built-in types
-/

lemma 
List.fold_max_max_eq_max_fold_max: βˆ€ {xs : List β„•} {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
List.fold_max_max_eq_max_fold_max : 
    βˆ€ {
a: β„•
a 
b: β„•
b : 
β„•: Type
β„•}, 
List.foldl: {Ξ± : Type ?u.82} β†’ {Ξ² : Type ?u.81} β†’ (Ξ± β†’ Ξ² β†’ Ξ±) β†’ Ξ± β†’ List Ξ² β†’ Ξ±
List.foldl 
max: {Ξ± : Type ?u.85} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max (
max: {Ξ± : Type ?u.117} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max 
a: β„•
a 
b: β„•
b) 
xs: ?m.72
xs = 
max: {Ξ± : Type ?u.133} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max 
a: β„•
a (
List.foldl: {Ξ± : Type ?u.137} β†’ {Ξ² : Type ?u.136} β†’ (Ξ± β†’ Ξ² β†’ Ξ±) β†’ Ξ± β†’ List Ξ² β†’ Ξ±
List.foldl 
max: {Ξ± : Type ?u.140} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max 
b: β„•
b 
xs: ?m.72
xs) := 
Goals accomplished! πŸ™
xs: List β„•

βˆ€ {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
xs: List β„•

βˆ€ {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
xs: List β„•

βˆ€ {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
nil
βˆ€ {a b : β„•}, foldl max (max a b) [] = max a (foldl max b [])
head✝: β„•

tail✝: List β„•

tail_ih✝: βˆ€ {a b : β„•}, foldl max (max a b) tail✝ = max a (foldl max b tail✝)

cons
βˆ€ {a b : β„•}, foldl max (max a b) (head✝ :: tail✝) = max a (foldl max b (head✝ :: tail✝))
xs: List β„•

βˆ€ {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
βˆ€ {a b : β„•}, foldl max (max a b) [] = max a (foldl max b [])
Goals accomplished! πŸ™
xs: List β„•

βˆ€ {a b : β„•}, foldl max (max a b) xs = max a (foldl max b xs)
head✝: β„•

tail✝: List β„•

ih: βˆ€ {a b : β„•}, foldl max (max a b) tail✝ = max a (foldl max b tail✝)

βˆ€ {a b : β„•}, foldl max (max a b) (head✝ :: tail✝) = max a (foldl max b (head✝ :: tail✝))
Goals accomplished! πŸ™
Goals accomplished! πŸ™


lemma 
List.get_index_eq: βˆ€ {Ξ± : Type u_1} {xs : List Ξ±} {i j : β„•} (hi : i < length xs),
  i = j β†’ βˆƒ hj, get xs { val := i, isLt := hi } = get xs { val := j, isLt := hj }
List.get_index_eq {
xs: List Ξ±
xs : 
List: Type ?u.23539 β†’ Type ?u.23539
List 
Ξ±: ?m.23536
Ξ±} {
i: β„•
i 
j: β„•
j : 
β„•: Type
β„•} (
hi: i < length xs
hi : 
i: β„•
i < 
xs: List Ξ±
xs.
length: {Ξ± : Type ?u.23547} β†’ List Ξ± β†’ β„•
length) (
h: i = j
h : 
i: β„•
i = 
j: β„•
j) : 
    βˆƒ (
hj: j < length xs
hj : 
j: β„•
j < 
xs: List Ξ±
xs.
length: {Ξ± : Type ?u.23567} β†’ List Ξ± β†’ β„•
length), 
xs: List Ξ±
xs.
get: {Ξ± : Type ?u.23575} β†’ (as : List Ξ±) β†’ Fin (length as) β†’ Ξ±
get ⟨
i: β„•
i, 
hi: i < length xs
hi⟩ = 
xs: List Ξ±
xs.
get: {Ξ± : Type ?u.23585} β†’ (as : List Ξ±) β†’ Fin (length as) β†’ Ξ±
get ⟨
j: β„•
j, 
hj: j < length xs
hj⟩ := 
Goals accomplished! πŸ™
Ξ±: Type u_1

xs: List Ξ±

i, j: β„•

hi: i < length xs

h: i = j

βˆƒ hj, get xs { val := i, isLt := hi } = get xs { val := j, isLt := hj }
Ξ±: Type u_1

xs: List Ξ±

i, j: β„•

hi✝: i < length xs

h: i = j

hi: j < length xs

βˆƒ hj, get xs { val := i, isLt := hi✝ } = get xs { val := j, isLt := hj }
Ξ±: Type u_1

xs: List Ξ±

i, j: β„•

hi: i < length xs

h: i = j

βˆƒ hj, get xs { val := i, isLt := hi } = get xs { val := j, isLt := hj }
Ξ±: Type u_1

xs: List Ξ±

i, j: β„•

hi✝: i < length xs

h: i = j

hi: j < length xs

get xs { val := i, isLt := hi✝ } = get xs { val := j, isLt := hi }
Ξ±: Type u_1

xs: List Ξ±

i, j: β„•

hi: i < length xs

h: i = j

βˆƒ hj, get xs { val := i, isLt := hi } = get xs { val := j, isLt := hj }
Goals accomplished! πŸ™


lemma 
List.get_zero_eq_head: βˆ€ {Ξ± : Type u_1} {xs : List Ξ±} (hn : xs β‰  []), get xs { val := 0, isLt := (_ : 0 < length xs) } = head xs hn
List.get_zero_eq_head {
xs: List Ξ±
xs : 
List: Type ?u.24015 β†’ Type ?u.24015
List 
Ξ±: ?m.24012
Ξ±} (
hn: xs β‰  []
hn : 
xs: List Ξ±
xs β‰  
[]: List ?m.24021
[]) :
    
xs: List Ξ±
xs.
get: {Ξ± : Type ?u.24026} β†’ (as : List Ξ±) β†’ Fin (length as) β†’ Ξ±
get ⟨
0: ?m.24037
0, 
Goals accomplished! πŸ™
Ξ±: Type ?u.24015

xs: List Ξ±

hn: xs β‰  []

0 < length xs
Ξ±: Type ?u.24015

xs: List Ξ±

hn: xs β‰  []

0 < length xs
Ξ±: Type ?u.24015

xs: List Ξ±

hn: xs β‰  []

0 < length xs
Ξ±: Type ?u.24015

hn: [] β‰  []

nil
0 < length []
Ξ±: Type ?u.24015

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
0 < length (head✝ :: tail✝)
Ξ±: Type ?u.24015

hn: [] β‰  []

nil
0 < length []
Ξ±: Type ?u.24015

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
0 < length (head✝ :: tail✝)
Ξ±: Type ?u.24015

xs: List Ξ±

hn: xs β‰  []

0 < length xs
Ξ±: Type ?u.24015

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
0 < length (head✝ :: tail✝)
Ξ±: Type ?u.24015

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
0 < length (head✝ :: tail✝)
Ξ±: Type ?u.24015

xs: List Ξ±

hn: xs β‰  []

0 < length xs
Goals accomplished! πŸ™
Goals accomplished! πŸ™
⟩ = 
xs: List Ξ±
xs.
head: {Ξ± : Type ?u.24048} β†’ (as : List Ξ±) β†’ as β‰  [] β†’ Ξ±
head 
hn: xs β‰  []
hn := 
Goals accomplished! πŸ™
Ξ±: Type u_1

xs: List Ξ±

hn: xs β‰  []

get xs { val := 0, isLt := (_ : 0 < length xs) } = head xs hn
Ξ±: Type u_1

hn: [] β‰  []

nil
get [] { val := 0, isLt := (_ : 0 < length []) } = head [] hn
Ξ±: Type u_1

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
get (head✝ :: tail✝) { val := 0, isLt := (_ : 0 < length (head✝ :: tail✝)) } = head (head✝ :: tail✝) hn
Ξ±: Type u_1

hn: [] β‰  []

nil
get [] { val := 0, isLt := (_ : 0 < length []) } = head [] hn
Ξ±: Type u_1

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
get (head✝ :: tail✝) { val := 0, isLt := (_ : 0 < length (head✝ :: tail✝)) } = head (head✝ :: tail✝) hn
Ξ±: Type u_1

xs: List Ξ±

hn: xs β‰  []

get xs { val := 0, isLt := (_ : 0 < length xs) } = head xs hn
Ξ±: Type u_1

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
get (head✝ :: tail✝) { val := 0, isLt := (_ : 0 < length (head✝ :: tail✝)) } = head (head✝ :: tail✝) hn
Ξ±: Type u_1

head✝: α

tail✝: List α

hn: head✝ :: tail✝ β‰  []

cons
get (head✝ :: tail✝) { val := 0, isLt := (_ : 0 < length (head✝ :: tail✝)) } = head (head✝ :: tail✝) hn
Ξ±: Type u_1

xs: List Ξ±

hn: xs β‰  []

get xs { val := 0, isLt := (_ : 0 < length xs) } = head xs hn
Goals accomplished! πŸ™


lemma 
Nat.not_lt_of_lt: βˆ€ {a b : β„•}, a < b β†’ Β¬b < a
Nat.not_lt_of_lt {
a: β„•
a 
b: β„•
b : 
β„•: Type
β„•} (
h: a < b
h : 
a: β„•
a < 
b: β„•
b): Β¬ 
b: β„•
b < 
a: β„•
a := 
Goals accomplished! πŸ™
a, b: β„•

h: a < b

Β¬b < a
Goals accomplished! πŸ™


lemma 
Nat.mul_lt_mulβ‚€: βˆ€ {a b c d : β„•}, a < c β†’ b < d β†’ a * b < c * d
Nat.mul_lt_mulβ‚€ {
a: β„•
a 
b: β„•
b 
c: β„•
c 
d: β„•
d : 
Nat: Type
Nat} (
h1: a < c
h1 : 
a: β„•
a < 
c: β„•
c) (
h2: b < d
h2 : 
b: β„•
b < 
d: β„•
d) : 
a: β„•
a * 
b: β„•
b < 
c: β„•
c * 
d: β„•
d := 
  match 
b: β„•
b with 
  | 
0: β„•
0 => 
    match 
c: β„•
c with 
    | 
0: β„•
0 => match 
h1: a < 0
h1 with .
    | 
c: β„•
c+1 => 
Goals accomplished! πŸ™
a, b, c✝, d: β„•

h2: 0 < d

c: β„•

h1: a < c + 1

a * 0 < (c + 1) * d
Goals accomplished! πŸ™

  | 
b: β„•
b+1 => 
Nat.mul_lt_mul: βˆ€ {a c b d : β„•}, a < c β†’ b ≀ d β†’ 0 < b β†’ a * b < c * d
Nat.mul_lt_mul 
h1: a < c
h1 (
Nat.le_of_lt: βˆ€ {n m : β„•}, n < m β†’ n ≀ m
Nat.le_of_lt 
h2: b + 1 < d
h2) (
Goals accomplished! πŸ™
a, b✝, c, d: β„•

h1: a < c

b: β„•

h2: b + 1 < d

0 < b + 1
Goals accomplished! πŸ™
)

lemma 
Nat.sub_lt_sub_right: βˆ€ {a b c : β„•}, a < b β†’ c ≀ a β†’ a - c < b - c
Nat.sub_lt_sub_right {
a: β„•
a 
b: β„•
b 
c: β„•
c : 
Nat: Type
Nat} (
h0: a < b
h0 : 
a: β„•
a < 
b: β„•
b) (
h1: c ≀ a
h1 : 
c: β„•
c ≀ 
a: β„•
a) : 
    
a: β„•
a - 
c: β„•
c < 
b: β„•
b - 
c: β„•
c := 
Goals accomplished! πŸ™
a, b, c: β„•

h0: a < b

h1: c ≀ a

a - c < b - c
a, b, c: β„•

h0: a < b

h1: c ≀ a

a - c < b - c
a, b, c: β„•

h0: a < b

h1: c ≀ a

a - c < b - c
a, b: β„•

h0: a < b

h1: zero ≀ a

zero
a - zero < b - zero
a, b: β„•

h0: a < b

n✝: β„•

n_ih✝: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

succ
a - succ n✝ < b - succ n✝
a, b, c: β„•

h0: a < b

h1: c ≀ a

a - c < b - c
a, b: β„•

h0: a < b

h1: zero ≀ a

a - zero < b - zero
Goals accomplished! πŸ™
a, b, c: β„•

h0: a < b

h1: c ≀ a

a - c < b - c
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a - succ n✝ < b - succ n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

pred (a - n✝) < pred (b - n✝)
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a - succ n✝ < b - succ n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ β‰  0
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ < b - n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a - succ n✝ < b - succ n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ β‰  0
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ < b - n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
n✝ < a
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ β‰  0
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ < b - n✝
Goals accomplished! πŸ™
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a - succ n✝ < b - succ n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ < b - n✝
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
n✝ ≀ a
a, b: β„•

h0: a < b

n✝: β„•

ih: n✝ ≀ a β†’ a - n✝ < b - n✝

h1: succ n✝ ≀ a

a
a - n✝ < b - n✝
Goals accomplished! πŸ™
Goals accomplished! πŸ™


lemma 
Nat.sub_sub_eq: βˆ€ {a b c : β„•}, a ≀ b β†’ c + a - b = c - (b - a)
Nat.sub_sub_eq {
a: β„•
a 
b: β„•
b 
c: β„•
c : 
Nat: Type
Nat} (
h: a ≀ b
h : 
a: β„•
a ≀ 
b: β„•
b) : 
c: β„•
c + 
a: β„•
a - 
b: β„•
b = 
c: β„•
c - (
b: β„•
b - 
a: β„•
a) := 
Goals accomplished! πŸ™
a, b, c: β„•

h: a ≀ b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

k: β„•

h': a + k = b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

k: β„•

h': a + k = b

c + a - b = c - (b - a)
a, b, c: β„•

h: a ≀ b

k: β„•

h': a + k = b

c + a - (a + k) = c - (a + k - a)
a, b, c: β„•

h: a ≀ b

k: β„•

h': a + k = b

c + a - (a + k) = c - (a + k - a)
a, b, c: β„•

h: a ≀ b

c + a - b = c - (b - a)
Goals accomplished! πŸ™
Goals accomplished! πŸ™