internlm/Lean-Github huggingface dataset:
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
Proof state after:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : r < 1),
      ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ⨆ (_ : r < 1),
      ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ (fun x_1 => ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) = fun i =>
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
⊢ (fun x_1 => ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) = fun i =>
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext rle1
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑a.toNNReal * ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
norm_cast
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply NNReal.eq
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑(a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊)
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑(a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊)
Tactic:
simp only [coe_nnnorm, NNReal.coe_mul]
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ↑a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ↑a.toNNReal * ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Tactic:
rw [← Real.norm_of_nonneg (@NNReal.zero_le_coe a.toNNReal), ← Complex.norm_real, ← norm_mul]
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ‖↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ =
    ‖↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp‖
Tactic:
congr
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ↑↑a.toNNReal * ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp
Tactic:
rw [← MeasureTheory.integral_mul_left, Real.coe_toNNReal a ha.le]
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ∫ (a_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp =
    ∫ (a_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Tactic:
congr
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun a_1 =>
    ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun a_1 =>
    ↑a * (↑(1 / a) * f a_1 * K x a_1 * (Complex.I * ↑n * ↑a_1).exp)
Tactic:
ext y
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp)
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (↑(1 / a) * f y * K x y * (Complex.I * ↑n * ↑y).exp)
Tactic:
field_simp
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (f y * K x y * (Complex.I * ↑n * ↑y).exp) / ↑a
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = ↑a * (f y * K x y * (Complex.I * ↑n * ↑y).exp) / ↑a
Tactic:
rw [mul_div_cancel_left₀]
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ↑a ≠ 0
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ↑a ≠ 0
Tactic:
norm_cast
Proof state after:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ¬a = 0
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s.h.e_s.h.a.e_a.e_f.h.ha
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ ¬a = 0
Tactic:
exact ha.ne.symm
Proof state after:
no goals
Theorem: h1
Proof state before:
⊢ 2 ∈ Set.Ioc 1 2
Tactic:
simp
Proof state after:
no goals
Theorem: h2
Proof state before:
⊢ Real.IsConjExponent 2 2
Tactic:
rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
Proof state after:
no goals
Theorem: localOscillation_on_emptyset
Proof state before:
X : Type
inst✝ : PseudoMetricSpace X
f g : C(X, ℂ)
⊢ localOscillation ∅ f g = 0
Tactic:
simp [localOscillation]
Proof state after:
no goals
Theorem: localOscillation_on_empty_ball
Proof state before:
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ localOscillation (Metric.ball x R) f g = 0
Tactic:
convert localOscillation_on_emptyset
Proof state after:
case h.e'_2.h.e'_3
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ Metric.ball x R = ∅
Theorem: localOscillation_on_empty_ball
Proof state before:
case h.e'_2.h.e'_3
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ Metric.ball x R = ∅
Tactic:
exact Metric.ball_eq_empty.mpr R_nonpos
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ≤ ⨆ i ∈ s, f i
Tactic:
apply ConditionallyCompleteLattice.le_csSup
Proof state after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)

case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)

case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Tactic:
. rw [bddAbove_def] at *
  rcases hfs with ⟨x, hx⟩
  use (max x (sSup ∅))
  intro y hy
  simp at hy
  rcases hy with ⟨z, hz⟩
  rw [iSup] at hz
  by_cases h : z ∈ s
  . have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
      rw [Set.eq_singleton_iff_unique_mem]
      constructor
      . simpa
      . intro x hx
        simp at hx
        exact hx.2.symm
    rw [this] at hz
    have : sSup {f z} = f z := by apply csSup_singleton
    rw [this] at hz
    simp at hx
    have : f z ≤ x := hx z h
    rw [hz] at this
    apply le_max_of_le_left this
  have : (@Set.range α (z ∈ s) fun _ ↦ f z) = ∅ := by
    simpa
  rw [this] at hz
  rw [hz]
  exact le_max_right x y
Proof state after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Tactic:
rw [Set.mem_range]
Proof state after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Tactic:
rcases ha with ⟨i, hi, fia⟩
Proof state after:
case a.intro.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a.intro.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Tactic:
use i
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ⨆ (_ : i ∈ s), f i = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ⨆ (_ : i ∈ s), f i = a
Tactic:
rw [iSup]
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ sSup (Set.range fun h => f i) = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ sSup (Set.range fun h => f i) = a
Tactic:
convert csSup_singleton _
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (Set.range fun h => f i) = {a}
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (Set.range fun h => f i) = {a}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (a ∈ Set.range fun h => f i) ∧ ∀ x ∈ Set.range fun h => f i, x = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (a ∈ Set.range fun h => f i) ∧ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
constructor
Proof state after:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i

case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i

case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
. simp
  use hi, fia
Proof state after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
. intro x hx
  simp at hx
  rwa [hx.2] at fia
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)
Tactic:
rw [bddAbove_def] at *
Proof state after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : ∃ x, ∀ y ∈ f '' s, y ≤ x
ha : ∃ i ∈ s, f i = a
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : ∃ x, ∀ y ∈ f '' s, y ≤ x
ha : ∃ i ∈ s, f i = a
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Tactic:
rcases hfs with ⟨x, hx⟩
Proof state after:
case a.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case a.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Tactic:
use (max x (sSup ∅))
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ max x (sSup ∅)
Tactic:
intro y hy
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
⊢ y ≤ max x (sSup ∅)
Tactic:
simp at hy
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : ∃ y_1, ⨆ (_ : y_1 ∈ s), f y_1 = y
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : ∃ y_1, ⨆ (_ : y_1 ∈ s), f y_1 = y
⊢ y ≤ max x (sSup ∅)
Tactic:
rcases hy with ⟨z, hz⟩
Proof state after:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : ⨆ (_ : z ∈ s), f z = y
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : ⨆ (_ : z ∈ s), f z = y
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [iSup] at hz
Proof state after:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
⊢ y ≤ max x (sSup ∅)
Tactic:
by_cases h : z ∈ s
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)

case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)

case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Tactic:
. have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
    rw [Set.eq_singleton_iff_unique_mem]
    constructor
    . simpa
    . intro x hx
      simp at hx
      exact hx.2.symm
  rw [this] at hz
  have : sSup {f z} = f z := by apply csSup_singleton
  rw [this] at hz
  simp at hx
  have : f z ≤ x := hx z h
  rw [hz] at this
  apply le_max_of_le_left this
Proof state after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Tactic:
have : (@Set.range α (z ∈ s) fun _ ↦ f z) = ∅ := by
  simpa
Proof state after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)