internlm/Lean-Github huggingface dataset:
Theorem: Real.soCone_add_sub_two_mul_of_nonneg
Proof state before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (2 * z) ^ 2 ≤ (x + y) ^ 2 - (x - y) ^ 2 ↔ z ^ 2 ≤ x * y
Tactic:
ring_nf
Proof state after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ z ^ 2 * 4 ≤ x * y * 4 ↔ z ^ 2 ≤ x * y
Theorem: Real.soCone_add_sub_two_mul_of_nonneg
Proof state before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ z ^ 2 * 4 ≤ x * y * 4 ↔ z ^ 2 ≤ x * y
Tactic:
simp
Proof state after:
no goals
Theorem: Real.soCone_add_sub_two_of_nonneg
Proof state before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
have h := soCone_add_sub_two_mul_of_nonneg 1 hx hy
Proof state after:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2 * 1] ↔ 1 ^ 2 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Theorem: Real.soCone_add_sub_two_of_nonneg
Proof state before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2 * 1] ↔ 1 ^ 2 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
rw [mul_one, one_rpow] at h
Proof state after:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Theorem: Real.soCone_add_sub_two_of_nonneg
Proof state before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
exact h
Proof state after:
no goals
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ (x - y).soCone ![x + y, 2 * z] ↔ y ≤ x ∧ z ^ 2 ≤ -(x * y)
Tactic:
conv => lhs; unfold soCone; simp [sqrt_le_iff, ← le_sub_iff_add_le']
Proof state after:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ∧ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ y ≤ x ∧ z ^ 2 ≤ -(x * y)
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ∧ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ y ≤ x ∧ z ^ 2 ≤ -(x * y)
Tactic:
apply Iff.and
Proof state after:
case h₁
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ↔ y ≤ x

case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ z ^ 2 ≤ -(x * y)
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
case h₁
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ↔ y ≤ x
Tactic:
rfl
Proof state after:
no goals
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ z ^ 2 ≤ -(x * y)
Tactic:
ring_nf!
Proof state after:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 ≤ -(x * y * 4) ↔ z ^ 2 ≤ -(x * y)
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 ≤ -(x * y * 4) ↔ z ^ 2 ≤ -(x * y)
Tactic:
rw [← neg_mul, ← div_le_iff (by norm_num)]
Proof state after:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 / 4 ≤ -(x * y) ↔ z ^ 2 ≤ -(x * y)
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 / 4 ≤ -(x * y) ↔ z ^ 2 ≤ -(x * y)
Tactic:
simp
Proof state after:
no goals
Theorem: Real.soCone_sub_add_two_mul_of_nonneg
Proof state before:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two_mul
Proof state before:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ((x + y) i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]
Tactic:
dsimp
Proof state after:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two_mul
Proof state before:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]
Tactic:
convert Iff.rfl
Proof state after:
case h.e'_2.h.e'_4
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2 * z i] = ![x - y, 2 • z]ᵀ i
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two_mul
Proof state before:
case h.e'_2.h.e'_4
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2 * z i] = ![x - y, 2 • z]ᵀ i
Tactic:
funext j
Proof state after:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2 * z i] j = ![x - y, 2 • z]ᵀ i j
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two_mul
Proof state before:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2 * z i] j = ![x - y, 2 • z]ᵀ i j
Tactic:
fin_cases j <;> simp
Proof state after:
no goals
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two
Proof state before:
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
⊢ ((x + y) i).soCone (![x - y, 2]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2]
Tactic:
dsimp
Proof state after:
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2]
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two
Proof state before:
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2]
Tactic:
convert Iff.rfl
Proof state after:
case h.e'_2.h.e'_4
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2] = ![x - y, 2]ᵀ i
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two
Proof state before:
case h.e'_2.h.e'_4
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2] = ![x - y, 2]ᵀ i
Tactic:
funext j
Proof state after:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2] j = ![x - y, 2]ᵀ i j
Theorem: Real.vec_soCone_apply_to_soCone_add_sub_two
Proof state before:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.77315
m : Type ?u.77312
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2] j = ![x - y, 2]ᵀ i j
Tactic:
fin_cases j <;> simp
Proof state after:
no goals
Theorem: Vec.sum_exp_eq_sum_div
Proof state before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ sum (exp (x - const n t)) = sum (exp x) / t.exp
Tactic:
unfold Vec.sum
Proof state after:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = (Finset.univ.sum fun i => exp x i) / t.exp
Theorem: Vec.sum_exp_eq_sum_div
Proof state before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = (Finset.univ.sum fun i => exp x i) / t.exp
Tactic:
rw [Finset.sum_div]
Proof state after:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = Finset.univ.sum fun i => exp x i / t.exp
Theorem: Vec.sum_exp_eq_sum_div
Proof state before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = Finset.univ.sum fun i => exp x i / t.exp
Tactic:
congr
Proof state after:
case e_f
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (fun i => exp (x - const n t) i) = fun i => exp x i / t.exp
Theorem: Vec.sum_exp_eq_sum_div
Proof state before:
case e_f
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (fun i => exp (x - const n t) i) = fun i => exp x i / t.exp
Tactic:
ext i
Proof state after:
case e_f.h
n : ℕ
x : Fin n → ℝ
t : ℝ
i : Fin n
⊢ exp (x - const n t) i = exp x i / t.exp
Theorem: Vec.sum_exp_eq_sum_div
Proof state before:
case e_f.h
n : ℕ
x : Fin n → ℝ
t : ℝ
i : Fin n
⊢ exp (x - const n t) i = exp x i / t.exp
Tactic:
simp [Vec.exp, Vec.const, Real.exp_sub]
Proof state after:
no goals
Theorem: Vec.sum_exp_pos
Proof state before:
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ 0 < sum (exp x)
Tactic:
apply Finset.sum_pos
Proof state after:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i

case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Theorem: Vec.sum_exp_pos
Proof state before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i

case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
{ intros i _; simp [Vec.exp, Real.exp_pos] }
Proof state after:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Theorem: Vec.sum_exp_pos
Proof state before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
{ existsi ⟨0, hn⟩; simp }
Proof state after:
no goals
Theorem: Vec.sum_exp_pos
Proof state before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i
Tactic:
intros i _
Proof state after:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ 0 < exp x i
Theorem: Vec.sum_exp_pos
Proof state before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ 0 < exp x i
Tactic:
simp [Vec.exp, Real.exp_pos]
Proof state after:
no goals
Theorem: Vec.sum_exp_pos
Proof state before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
existsi ⟨0, hn⟩
Proof state after:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ⟨0, hn⟩ ∈ Finset.univ
Theorem: Vec.sum_exp_pos
Proof state before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ⟨0, hn⟩ ∈ Finset.univ
Tactic:
simp
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.log_nonneg_of_ge_one
Proof state before:
x : ℝ
h : 0 ≤ x - 1
⊢ 1 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.log_pos_of_gt_one
Proof state before:
x : ℝ
h : 0 < x - 1
⊢ 1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
have hx1 : x ≤ 1 := by linarith
Proof state after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 / x ^ 2 - 1
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
have h0x : 0 ≤ x := by positivity
Proof state after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
⊢ 0 ≤ 1 / x ^ 2 - 1
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
have h0x2 : 0 < x ^ (2 : ℝ) := by positivity
Proof state after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ 0 ≤ 1 / x ^ 2 - 1
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
rw [le_sub_iff_add_le, zero_add, le_div_iff h0x2, one_mul]
Proof state after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ x ^ 2 ≤ 1
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ x ^ 2 ≤ 1
Tactic:
simpa [abs_eq_self.mpr h0x]
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
⊢ x ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ x
Tactic:
positivity
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_one_div_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
⊢ 0 < x ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
⊢ 0 ≤ 1 - x ^ 2
Tactic:
have hx1 : x ≤ 1 := by linarith
Proof state after:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 - x ^ 2
Theorem: Mathlib.Meta.Positivity.Real.one_sub_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 - x ^ 2
Tactic:
rw [le_sub_iff_add_le, zero_add]
Proof state after:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ x ^ 2 ≤ 1
Theorem: Mathlib.Meta.Positivity.Real.one_sub_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ x ^ 2 ≤ 1
Tactic:
simpa [abs_eq_self.mpr h1]
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_sq_nonneg_of_le_one
Proof state before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
⊢ x ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.exp_sub_one_pos_of_pos
Proof state before:
x : ℝ
h : 0 < x
⊢ 0 < x.exp - 1
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.one_sub_div_exp_pos_of_pos
Proof state before:
x : ℝ
h : 0 < x
⊢ 0 < 1 - 1 / x.exp
Tactic:
field_simp
Proof state after:
x : ℝ
h : 0 < x
⊢ 0 < x.exp
Theorem: Mathlib.Meta.Positivity.Real.one_sub_div_exp_pos_of_pos
Proof state before:
x : ℝ
h : 0 < x
⊢ 0 < x.exp
Tactic:
positivity
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have ha : 0 ≤ a := by linarith
Proof state after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have ha1 : 1 < a := by linarith
Proof state after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have hx : 0 ≤ x := by linarith
Proof state after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < (a * x) ^ 2 - x ^ 2
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have hx2 : 0 < x ^ (2 : ℝ) := by positivity
Proof state after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 0 < (a * x) ^ 2 - x ^ 2
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
rw [sub_pos, Real.mul_rpow ha hx, ← div_lt_iff hx2, div_self (ne_of_gt hx2)]
Proof state after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 1 < a ^ 2
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 1 < a ^ 2
Tactic:
simp [ha1, abs_eq_self.mpr ha]
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
⊢ 0 ≤ a
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
⊢ 1 < a
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Mathlib.Meta.Positivity.Real.scaled_sq_diff_pos_of_pos
Proof state before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < x ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
⊢ M⁻¹ k k * M k k = 1
Tactic:
letI : Unique {a // id a = k} := ⟨⟨⟨k, rfl⟩⟩, fun j => Subtype.ext j.property⟩
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
⊢ M⁻¹ k k * M k k = 1
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
⊢ M⁻¹ k k * M k k = 1
Tactic:
have h := congr_fun (congr_fun
  (toSquareBlock_inv_mul_toSquareBlock_eq_one hM k) ⟨k, rfl⟩) ⟨k, rfl⟩
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : (M⁻¹.toSquareBlock id k * M.toSquareBlock id k) ⟨k, ⋯⟩ ⟨k, ⋯⟩ = 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : (M⁻¹.toSquareBlock id k * M.toSquareBlock id k) ⟨k, ⋯⟩ ⟨k, ⋯⟩ = 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
dsimp only [HMul.hMul, dotProduct] at h
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h :
  ∑ i : { a // id a = k }, Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ i) (M.toSquareBlock id k i ⟨k, ⋯⟩) =
    OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h :
  ∑ i : { a // id a = k }, Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ i) (M.toSquareBlock id k i ⟨k, ⋯⟩) =
    OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
rw [@Fintype.sum_unique _ _ _ _] at h
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ default) (M.toSquareBlock id k default ⟨k, ⋯⟩) = OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ default) (M.toSquareBlock id k default ⟨k, ⋯⟩) = OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
simp at h
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = 1
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = 1
Tactic:
rw [← h]
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩)
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩)
Tactic:
simp [toSquareBlock, toSquareBlockProp]
Proof state after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹ k k) (M k k)
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular
Proof state before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹ k k) (M k k)
Tactic:
rfl
Proof state after:
no goals