Theorem: Vec.le_div_iff (CvxLean/Lib/Math/Data/Vec.lean)

State before:
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c ↔ a * c ≤ b
Tactic:
constructor
State after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c → a * c ≤ b

case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a * c ≤ b → a ≤ b / c

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a ≤ b / c → a * c ≤ b
Tactic:
intro h i
State after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
⊢ (a * c) i ≤ b i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
⊢ (a * c) i ≤ b i
Tactic:
have hi := h i
State after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ (b / c) i
⊢ (a * c) i ≤ b i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ (b / c) i
⊢ (a * c) i ≤ b i
Tactic:
simp at hi
State after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ b i / c i
⊢ (a * c) i ≤ b i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i ≤ b i / c i
⊢ (a * c) i ≤ b i
Tactic:
rw [_root_.le_div_iff (hc i)] at hi
State after:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i * c i ≤ b i
⊢ (a * c) i ≤ b i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a ≤ b / c
i : m
hi : a i * c i ≤ b i
⊢ (a * c) i ≤ b i
Tactic:
exact hi
State after:
no goals

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a * c ≤ b → a ≤ b / c
Tactic:
intro h i
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
⊢ a i ≤ (b / c) i

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
⊢ a i ≤ (b / c) i
Tactic:
have hi := h i
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : (a * c) i ≤ b i
⊢ a i ≤ (b / c) i

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : (a * c) i ≤ b i
⊢ a i ≤ (b / c) i
Tactic:
simp at hi
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ (b / c) i

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ (b / c) i
Tactic:
dsimp
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ b i / c i

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ b i / c i
Tactic:
rw [_root_.le_div_iff (hc i)]
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i * c i ≤ b i

State before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i * c i ≤ b i
Tactic:
exact hi
State after:
no goals