internlm/Lean-Github huggingface dataset:
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
⊢ Disjoint (Iic a ∪ Ici d) (Icc b c)
Tactic:
simp_rw [Set.disjoint_union_left, Set.disjoint_iff, Set.subset_def, Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc,
  Set.mem_empty_iff_false, and_imp, imp_false, not_le, Set.mem_Ici]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
⊢ (∀ x ≤ a, b ≤ x → c < x) ∧ ∀ (x : ℝ), d ≤ x → b ≤ x → c < x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
⊢ (∀ x ≤ a, b ≤ x → c < x) ∧ ∀ (x : ℝ), d ≤ x → b ≤ x → c < x
Tactic:
constructor <;> intros <;> linarith
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ContDiff ℝ ⊤ Ψ
Tactic:
exact ContMDiff.contDiff hΨSmooth
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
constructor
Proof state after:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ HasCompactSupport Ψ

case h.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ HasCompactSupport Ψ
Tactic:
rw [hasCompactSupport_def]
Proof state after:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ IsCompact (closure (Function.support Ψ))
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ IsCompact (closure (Function.support Ψ))
Tactic:
apply IsCompact.closure_of_subset (K := Set.Icc a d) isCompact_Icc
Proof state after:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Function.support Ψ ⊆ Icc a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Function.support Ψ ⊆ Icc a d
Tactic:
simp_rw [Function.support_subset_iff, ne_eq, <-hΨ0]
Proof state after:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ∀ (x : ℝ), ¬(x ≤ a ∨ d ≤ x) → x ∈ Icc a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ∀ (x : ℝ), ¬(x ≤ a ∨ d ≤ x) → x ∈ Icc a d
Tactic:
intro x hx
Proof state after:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬(x ≤ a ∨ d ≤ x)
⊢ x ∈ Icc a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬(x ≤ a ∨ d ≤ x)
⊢ x ∈ Icc a d
Tactic:
contrapose! hx
Proof state after:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : x ∉ Icc a d
⊢ x ≤ a ∨ d ≤ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : x ∉ Icc a d
⊢ x ≤ a ∨ d ≤ x
Tactic:
simp only [Set.mem_Icc, not_and_or] at hx
Proof state after:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬a ≤ x ∨ ¬x ≤ d
⊢ x ≤ a ∨ d ≤ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬a ≤ x ∨ ¬x ≤ d
⊢ x ≤ a ∨ d ≤ x
Tactic:
by_contra! h'
Proof state after:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬a ≤ x ∨ ¬x ≤ d
h' : a < x ∧ x < d
⊢ False
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
hx : ¬a ≤ x ∨ ¬x ≤ d
h' : a < x ∧ x < d
⊢ False
Tactic:
cases' hx <;> linarith
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
constructor
Proof state after:
case h.right.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ (Icc b c).indicator 1 ≤ Ψ

case h.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ (Icc b c).indicator 1 ≤ Ψ
Tactic:
intro x
Proof state after:
case h.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ (Icc b c).indicator 1 x ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ (Icc b c).indicator 1 x ≤ Ψ x
Tactic:
rw [Set.indicator_apply]
Proof state after:
case h.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ (if x ∈ Icc b c then 1 x else 0) ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ (if x ∈ Icc b c then 1 x else 0) ≤ Ψ x
Tactic:
split_ifs with h
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Icc b c
⊢ 1 x ≤ Ψ x

case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
⊢ 0 ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Icc b c
⊢ 1 x ≤ Ψ x
Tactic:
simp only [Set.mem_Icc, Pi.one_apply] at *
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : b ≤ x ∧ x ≤ c
⊢ 1 ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : b ≤ x ∧ x ≤ c
⊢ 1 ≤ Ψ x
Tactic:
simp_rw [hΨ1 x] at h
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : Ψ x = 1
⊢ 1 ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : Ψ x = 1
⊢ 1 ≤ Ψ x
Tactic:
exact Eq.le (_root_.id h.symm)
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
⊢ 0 ≤ Ψ x
Tactic:
have : Ψ x ∈ Set.range Ψ := by simp only [Set.mem_range, exists_apply_eq_apply]
Proof state after:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
this : Ψ x ∈ range Ψ
⊢ 0 ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
this : Ψ x ∈ range Ψ
⊢ 0 ≤ Ψ x
Tactic:
have : Ψ x ∈ Set.Icc 0 1 := hΨrange this
Proof state after:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
this✝ : Ψ x ∈ range Ψ
this : Ψ x ∈ Icc 0 1
⊢ 0 ≤ Ψ x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
this✝ : Ψ x ∈ range Ψ
this : Ψ x ∈ Icc 0 1
⊢ 0 ≤ Ψ x
Tactic:
exact this.left
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Icc b c
⊢ Ψ x ∈ range Ψ
Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
constructor
Proof state after:
case h.right.right.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Ψ ≤ (Ioo a d).indicator 1

case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Ψ ≤ (Ioo a d).indicator 1
Tactic:
intro x
Proof state after:
case h.right.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ Ψ x ≤ (Ioo a d).indicator 1 x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ Ψ x ≤ (Ioo a d).indicator 1 x
Tactic:
rw [Set.indicator_apply]
Proof state after:
case h.right.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ Ψ x ≤ if x ∈ Ioo a d then 1 x else 0
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ Ψ x ≤ if x ∈ Ioo a d then 1 x else 0
Tactic:
split_ifs with h
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
⊢ Ψ x ≤ 1 x

case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Ioo a d
⊢ Ψ x ≤ 0
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
⊢ Ψ x ≤ 1 x
Tactic:
have : Ψ x ∈ Set.range Ψ := by simp only [Set.mem_range, exists_apply_eq_apply]
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
this : Ψ x ∈ range Ψ
⊢ Ψ x ≤ 1 x
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
this : Ψ x ∈ range Ψ
⊢ Ψ x ≤ 1 x
Tactic:
have : Ψ x ∈ Set.Icc 0 1 := hΨrange this
Proof state after:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
this✝ : Ψ x ∈ range Ψ
this : Ψ x ∈ Icc 0 1
⊢ Ψ x ≤ 1 x