internlm/Lean-Github huggingface dataset:
Theorem: Spts.not_two
Proof state before:
a : ℤ√(-3)
⊢ Zsqrtd.norm a ≠ 2
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
a : ℤ√(-3)
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq]
Proof state after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(Int.natAbs a.re ^ 2) ≠ 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(Int.natAbs a.re ^ 2) ≠ 2
Tactic:
norm_cast
Proof state after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬Int.natAbs a.re ^ 2 = 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬Int.natAbs a.re ^ 2 = 2
Tactic:
apply (Nat.pow_left_strictMono one_le_two).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
Tactic:
refine' ⟨_, hq⟩
Proof state after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
Tactic:
calc
  p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by rw [hq, mul_one, add_sub_cancel]
  _ = p.norm - 3 := by
    rw [Zsqrtd.norm_def]
    ring
  _ = 1 := by
    rw [hfour]
    norm_num
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
⊢ p.im ^ 2 = 1 → abs p.im = 1
Tactic:
intro h
Proof state after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ abs p.im = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ abs p.im = 1
Tactic:
rwa [← sq_eq_sq (abs_nonneg (_ : ℤ)) zero_le_one, one_pow, sq_abs]
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 = 1
Tactic:
apply le_antisymm
Proof state after:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1

case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1
Tactic:
contrapose! hfour with hq'
Proof state after:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ Zsqrtd.norm p ≠ 4
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ Zsqrtd.norm p ≠ 4
Tactic:
apply ne_of_gt
Proof state after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Theorem: Spts.four
Proof state before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Tactic:
rw [← Int.add_one_le_iff] at hq'
Proof state after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Theorem: Spts.four
Proof state before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Tactic:
calc
  4 < 3 * 2 := by norm_num
  _ ≤ 3 * p.im ^ 2 := (Int.mul_le_mul_of_nonneg_left hq' (by norm_num))
  _ ≤ p.re ^ 2 + 3 * p.im ^ 2 := (le_add_of_nonneg_left (pow_two_nonneg p.re))
  _ = p.norm := by
    rw [Zsqrtd.norm_def]
    ring
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = Zsqrtd.norm p
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.re * p.re - -3 * p.im * p.im
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
Proof state after:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2
Tactic:
exact sq_pos_of_ne_zero _ hq
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3
Tactic:
rw [hq, mul_one, add_sub_cancel]
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = Zsqrtd.norm p - 3
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ Zsqrtd.norm p - 3 = 1
Tactic:
rw [hfour]
Proof state after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ abs p.re = 1 ∧ abs p.im = 1
Tactic:
apply Spts.four hfour
Proof state after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ p.im ≠ 0
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ p.im ≠ 0
Tactic:
rintro him
Proof state after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Tactic:
rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
Proof state after:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
Proof state after:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False
Tactic:
norm_num at hfour
Proof state after:
no goals
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s (g ∘ f)
Tactic:
intro c
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
⊢ Convex 𝕜 {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
⊢ Convex 𝕜 {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
intro x hx y hy
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
y : E
hy : y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
y : E
hy : y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
simp only [Function.comp_apply, mem_setOf_eq] at hx hy
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
intro a b ha hb hab
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
simp only [Function.comp_apply, mem_setOf_eq]
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
cases le_total (f x) (f y) with
| inl h => 
    specialize hf (f y) ⟨hx.1, h⟩ ⟨hy.1, le_rfl⟩ ha hb hab
    simp only [mem_setOf_eq] at hf 
    exact ⟨hf.1, le_trans (hg hf.2) hy.2⟩
| inr h =>
    specialize hf (f x) ⟨hx.1, le_rfl⟩ ⟨hy.1, h⟩ ha hb hab
    simp only [mem_setOf_eq] at hf 
    exact ⟨hf.1, le_trans (hg hf.2) hx.2⟩
Proof state after:
no goals
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
specialize hf (f y) ⟨hx.1, h⟩ ⟨hy.1, le_rfl⟩ ha hb hab
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ {x | x ∈ s ∧ f x ≤ f y}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ {x | x ∈ s ∧ f x ≤ f y}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
simp only [mem_setOf_eq] at hf
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
exact ⟨hf.1, le_trans (hg hf.2) hy.2⟩
Proof state after:
no goals
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
specialize hf (f x) ⟨hx.1, le_rfl⟩ ⟨hy.1, h⟩ ha hb hab
Proof state after:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
simp only [mem_setOf_eq] at hf
Proof state after:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Theorem: QuasiconvexOn.monotone_comp
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
exact ⟨hf.1, le_trans (hg hf.2) hx.2⟩
Proof state after:
no goals
Theorem: QuasiconcaveOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ QuasiconcaveOn 𝕜 s (g ∘ f)
Tactic:
apply QuasiconvexOn.monotone_comp (β := βᵒᵈ) (γ := γᵒᵈ) (f := f) _ hf
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone g
Theorem: QuasiconcaveOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone g
Tactic:
rw [← monotone_dual_iff]
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)
Theorem: QuasiconcaveOn.monotone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)
Tactic:
exact hg
Proof state after:
no goals
Theorem: QuasiconcaveOn.antitone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s (g ∘ f)
Tactic:
apply QuasiconvexOn.antitone_comp (β := βᵒᵈ) (γ := γᵒᵈ) (f := f) _ hf
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone g
Theorem: QuasiconcaveOn.antitone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone g
Tactic:
rw [← antitone_dual_iff]
Proof state after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)
Theorem: QuasiconcaveOn.antitone_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Antitone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)
Tactic:
exact hg
Proof state after:
no goals
Theorem: Set.sep_of_subset
Proof state before:
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ t ∧ p x} ∩ s
Tactic:
ext x
Proof state after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ {x | x ∈ t ∧ p x} ∩ s
Theorem: Set.sep_of_subset
Proof state before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ {x | x ∈ t ∧ p x} ∩ s
Tactic:
simp only [mem_sep_iff, mem_inter_iff]
Proof state after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ s ∧ p x ↔ (x ∈ t ∧ p x) ∧ x ∈ s
Theorem: Set.sep_of_subset
Proof state before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ s ∧ p x ↔ (x ∈ t ∧ p x) ∧ x ∈ s
Tactic:
rw [and_assoc, and_comm]
Proof state after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x ∧ x ∈ s ↔ x ∈ t ∧ p x ∧ x ∈ s
Theorem: Set.sep_of_subset
Proof state before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x ∧ x ∈ s ↔ x ∈ t ∧ p x ∧ x ∈ s
Tactic:
simp only [iff_and_self, and_imp]
Proof state after:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x → x ∈ s → x ∈ t
Theorem: Set.sep_of_subset
Proof state before:
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x → x ∈ s → x ∈ t
Tactic:
exact fun _ h' => hst h'
Proof state after:
no goals
Theorem: Convex.quasiconvexOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
⊢ QuasiconvexOn 𝕜 t f
Tactic:
intro b
Proof state after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ f x ≤ b}