Theorem: List.length_prod (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
β : Type u_2
x✝ : List β
⊢ length (prod [] x✝) = length [] * length x✝
Tactic:
simp [prod, length]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
x : α
xs : List α
⊢ length (prod (x :: xs) []) = length (x :: xs) * length []
Tactic:
simp [prod, length]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
Tactic:
simp only [prod]
State after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length ((x, y) :: prod [x] ys) = length [x] * length (y :: ys)

State before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length ((x, y) :: prod [x] ys) = length [x] * length (y :: ys)
Tactic:
unfold length
State after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] ys) + 1 = (length [] + 1) * (length ys + 1)

State before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] ys) + 1 = (length [] + 1) * (length ys + 1)
Tactic:
rw [ih]
State after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length [x] * length ys + 1 = (length [] + 1) * (length ys + 1)

State before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length [x] * length ys + 1 = (length [] + 1) * (length ys + 1)
Tactic:
simp only [length]
State after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ (0 + 1) * length ys + 1 = (0 + 1) * (length ys + 1)

State before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ (0 + 1) * length ys + 1 = (0 + 1) * (length ys + 1)
Tactic:
rw [Nat.one_mul, Nat.one_mul]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
Tactic:
apply Nat.add_lt_add_of_lt
State after:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 < Nat.succ (Nat.succ (length xs))

State before:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 < Nat.succ (Nat.succ (length xs))
Tactic:
apply Nat.succ_lt_succ $ Nat.succ_pos (length xs)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
Tactic:
apply Nat.add_lt_add_of_lt
State after:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) < Nat.succ (Nat.succ (length xs))

State before:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) < Nat.succ (Nat.succ (length xs))
Tactic:
apply Nat.succ_lt_succ
State after:
case a.a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ length xs < length xs + 1

State before:
case a.a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ length xs < length xs + 1
Tactic:
apply Nat.lt.base
State after:
no goals

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod (x :: x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
unfold prod
State after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length
      (let_fun h₁ := (_ : Nat.succ 0 + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      let_fun h₂ := (_ : Nat.succ (length xs) + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) =
    length (x :: x' :: xs) * length (y :: ys)

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length
      (let_fun h₁ := (_ : Nat.succ 0 + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      let_fun h₂ := (_ : Nat.succ (length xs) + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) =
    length (x :: x' :: xs) * length (y :: ys)
Tactic:
simp only
State after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
rw [List.length_append, ih₁, ih₂]
State after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length [x] * length (y :: ys) + length (x' :: xs) * length (y :: ys) = length (x :: x' :: xs) * length (y :: ys)

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length [x] * length (y :: ys) + length (x' :: xs) * length (y :: ys) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
simp only [length]
State after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ (0 + 1) * (length ys + 1) + (length xs + 1) * (length ys + 1) = (length xs + 1 + 1) * (length ys + 1)

State before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ (0 + 1) * (length ys + 1) + (length xs + 1) * (length ys + 1) = (length xs + 1 + 1) * (length ys + 1)
Tactic:
rw [←Nat.add_mul, Nat.zero_add, Nat.add_comm 1]
State after:
no goals