Theorem: isSolutionModel_solveOneModel (One.lean)

State before:
⊢ isSolutionModel solveOneModel
Tactic:
unfold isSolutionModel
State after:
⊢ ∀ (elves : List (List ℤ)) (elf : List ℤ), elf ∈ elves → solveOneModel elves ≥ List.sum elf

State before:
⊢ ∀ (elves : List (List ℤ)) (elf : List ℤ), elf ∈ elves → solveOneModel elves ≥ List.sum elf
Tactic:
intro elves elf elfin
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ solveOneModel elves ≥ List.sum elf

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ solveOneModel elves ≥ List.sum elf
Tactic:
unfold solveOneModel
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
have hsumin: List.sum elf ∈ (List.map List.sum) elves := by apply List.mem_map'.2; exists elf
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
have z:=  List.le_maximum_of_mem' hsumin
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ WithBot.unbot' 0 (List.maximum (List.map List.sum elves)) ≥ List.sum elf
Tactic:
apply WithBot.coe_le_coe.1
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ ↑(List.sum elf) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ ↑(List.sum elf) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Tactic:
apply le_trans z
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ List.maximum (List.map List.sum elves) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
hsumin : List.sum elf ∈ List.map List.sum elves
z : ↑(List.sum elf) ≤ List.maximum (List.map List.sum elves)
⊢ List.maximum (List.map List.sum elves) ≤ ↑(WithBot.unbot' 0 (List.maximum (List.map List.sum elves)))
Tactic:
apply WithBot.le_coe_unbot'
State after:
no goals

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ List.sum elf ∈ List.map List.sum elves
Tactic:
apply List.mem_map'.2
State after:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ ∃ a, a ∈ elves ∧ List.sum a = List.sum elf

State before:
elves : List (List ℤ)
elf : List ℤ
elfin : elf ∈ elves
⊢ ∃ a, a ∈ elves ∧ List.sum a = List.sum elf
Tactic:
exists elf
State after:
no goals