Theorem: Weight.dom_of_pair_le (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ w ≤ w'
Tactic:
rw [dom_iff, f_le_iff]
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
Tactic:
intro a
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
⊢ f w a ≤ f w' a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
⊢ f w a ≤ f w' a
Tactic:
by_cases H : 0 ≤ pair' w (v a)
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a

case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : ¬0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a
Tactic:
have h' := h a H
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
⊢ f w a ≤ f w' a

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Tactic:
have H' : 0 ≤ pair' w' (v a) := H.trans h'
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ f w a ≤ f w' a

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Tactic:
zify
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ ↑(f w a) ≤ ↑(f w' a)

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ ↑(f w a) ≤ ↑(f w' a)
Tactic:
rw [f_apply_eq_pair'_v_of_nonneg H, f_apply_eq_pair'_v_of_nonneg H']
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) + 1 ≤ pair' w' (v a) / (↑n + 1) + 1

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) + 1 ≤ pair' w' (v a) / (↑n + 1) + 1
Tactic:
simp only [add_le_add_iff_right]
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) ≤ pair' w' (v a) / (↑n + 1)

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) ≤ pair' w' (v a) / (↑n + 1)
Tactic:
exact Int.ediv_le_ediv (by linarith) h'
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ 0 < ↑n + 1
Tactic:
linarith
State after:
no goals

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : ¬0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a
Tactic:
push_neg at H
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ f w a ≤ f w' a

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ f w a ≤ f w' a
Tactic:
rw [f_apply_eq_zero_of_neg_pair'_v H]
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ 0 ≤ f w' a

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ 0 ≤ f w' a
Tactic:
exact Nat.zero_le _
State after:
no goals