Theorem: Vec.div_le_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 → ℝ
hb : StrongLT 0 b
⊢ 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 → ℝ
hb : StrongLT 0 b
⊢ 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 → ℝ
hb : StrongLT 0 b
⊢ 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 → ℝ
hb : StrongLT 0 b
⊢ 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 → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
⊢ a i ≤ (c * b) i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
⊢ a i ≤ (c * 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 → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : (a / b) i ≤ c i
⊢ a i ≤ (c * b) i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : (a / b) i ≤ c i
⊢ a i ≤ (c * 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 → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i / b i ≤ c i
⊢ a i ≤ (c * b) i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i / b i ≤ c i
⊢ a i ≤ (c * b) i
Tactic:
rw [_root_.div_le_iff (hb 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 → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ (c * b) i

State before:
case mp
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
h : a / b ≤ c
i : m
hi : a i ≤ c i * b i
⊢ a i ≤ (c * 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 → ℝ
hb : StrongLT 0 b
⊢ 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
⊢ (a / 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
⊢ (a / b) i ≤ 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ (c * b) i
⊢ (a / 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ (c * b) i
⊢ (a / b) i ≤ 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ (a / 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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ (a / b) i ≤ 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 → ℝ
hb : StrongLT 0 b
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 → ℝ
hb : StrongLT 0 b
h : a ≤ c * b
i : m
hi : a i ≤ c i * b i
⊢ a i / b i ≤ c i
Tactic:
rw [_root_.div_le_iff (hb i)]
State after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hb : StrongLT 0 b
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 → ℝ
hb : StrongLT 0 b
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