awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
a : (↑(toNNReal (σ x) + toNNReal x) : ℝ) = (↑1 : ℝ)
⊢ toNNReal (σ x) + toNNReal x = 1

Tactic:
ext
-- Module: Mathlib.Topology.UnitInterval
Goal:
x : (↑I : Type)
⊢ (↑(toNNReal (σ x) + toNNReal x) : ℝ) = (↑1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ (f : X →ᵇ ℝ),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
let ⟨f, hfs, hft, hf⟩ := exists_continuous_zero_one_of_isClosed hs ht hd
  ⟨⟨f, 1, fun _ _ => Real.dist_le_of_mem_Icc_01 (hf _) (hf _)⟩, hfs, hft, hf⟩

Premises used: exists_continuous_zero_one_of_isClosed, _private.0.exists_bounded_zero_one_of_closed.match_1, Exists, Set.EqOn, And, Real.dist_le_of_mem_Icc_01, And.intro, BoundedContinuousFunction.mk, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ s
⊢ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x = Function.const X a x

Tactic:
simp [hfs hx]
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ t
⊢ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x = Function.const X b x

Tactic:
simp [hft hx]
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
dsimp : a ≤ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)
⊢ a ≤ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x

Tactic:
dsimp
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
nlinarith :
  a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) < a →
    a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) - a +
        (0 - (a - b) * HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)) =
      0
⊢ a ≤ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
nlinarith [(hf01 x).1]

Premises used: And.left
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
dsimp : a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) ≤ b
⊢ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x ≤ b

Tactic:
dsimp
-- Module: Mathlib.Topology.UrysohnsBounded
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
nlinarith :
  b < a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) →
    b - (a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)) +
        (0 - (a - b) * HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)) =
      0
⊢ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) ≤ b

Tactic:
nlinarith [(hf01 x).2]

Premises used: And.right
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ c.left (P := P).U (P := P) ⊆ c.right (P := P).C (P := P)

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, closure, Classical.choose, Set.sInter
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ c.left (P := P).U (P := P) ⊆ c.U (P := P)

Tactic:
Subset.trans c.left_U_subset_right_C c.right.subset

Premises used: Set.Subset.trans, Urysohns.CU.left_U_subset_right_C, Urysohns.CU.right, Urysohns.CU.subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ c.C (P := P) ⊆ c.right (P := P).C (P := P)

Tactic:
Subset.trans c.left.subset c.left_U_subset_right_C

Premises used: Set.Subset.trans, Urysohns.CU.left_U_subset_right_C, Urysohns.CU.left, Urysohns.CU.subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ c.C (P := P)
⊢ approx (P := P) 0 c x = 0

Tactic:
indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _

Premises used: Urysohns.CU.approx, Set.indicator_of_notMem, Urysohns.CU.subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ c.C (P := P)
⊢ approx (P := P) 0 c x = 0

Tactic:
exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _

Premises used: Set.indicator_of_notMem, Urysohns.CU.subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
succ : x ∈ c.right (P := P).C (P := P)
succ₁ : x ∈ c.left (P := P).C (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 0

Tactic:
rw [ihn, ihn, midpoint_self]

Premises used: midpoint_self
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
⊢ x ∈ c.right (P := P).C (P := P)

Tactic:
c.subset_right_C hx

Premises used: Urysohns.CU.subset_right_C
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
⊢ x ∈ c.left (P := P).C (P := P)

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
⊢ x ∈ c.right (P := P).C (P := P)

Tactic:
exacts [c.subset_right_C hx, hx]

Premises used: Urysohns.CU.subset_right_C
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C (P := P)
zero : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) 0 c x = 0
succ :
  ∀ (n : ℕ) (ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0) (c : CU P) (hx : x ∈ c.C (P := P)),
    approx (P := P) (n + 1) c x = 0
⊢ approx (P := P) n c x = 0

Tactic:
induction n generalizing c with
  | zero => exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]

Premises used: Urysohns.CU.subset_right_C, midpoint_self, Urysohns.CU.approx, Set.indicator_of_notMem, Urysohns.CU.subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∉ c.U (P := P)
⊢ x ∈ (c.U (P := P))ᶜ

Tactic:
rw [← mem_compl_iff] at hx

Premises used: Set.mem_compl_iff
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ (c.U (P := P))ᶜ
⊢ approx (P := P) 0 c x = 1

Tactic:
indicator_of_mem hx _

Premises used: Urysohns.CU.approx, Set.indicator_of_mem
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ (c.U (P := P))ᶜ
⊢ approx (P := P) 0 c x = 1

Tactic:
exact indicator_of_mem hx _

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
succ : x ∉ c.right (P := P).U (P := P)
succ₁ : x ∉ c.left (P := P).U (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 1

Tactic:
rw [ihn, ihn, midpoint_self]

Premises used: midpoint_self
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
⊢ x ∉ c.right (P := P).U (P := P)

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
⊢ x ∉ c.left (P := P).U (P := P)

Tactic:
fun hU => hx <| c.left_U_subset hU

Premises used: Not, Urysohns.CU.left_U_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
⊢ x ∉ c.right (P := P).U (P := P)

Tactic:
exacts [hx, fun hU => hx <| c.left_U_subset hU]

Premises used: Urysohns.CU.left_U_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U (P := P)
zero : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) 0 c x = 1
succ :
  ∀ (n : ℕ) (ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1) (c : CU P) (hx : x ∉ c.U (P := P)),
    approx (P := P) (n + 1) c x = 1
⊢ approx (P := P) n c x = 1

Tactic:
induction n generalizing c with
  | zero =>
    rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]

Premises used: midpoint_self, Urysohns.CU.approx, Set.indicator_of_mem, Set.mem_compl_iff, Urysohns.CU.left_U_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ approx (P := P) 0 c x

Tactic:
indicator_nonneg (fun _ _ => zero_le_one) _

Premises used: Urysohns.CU.approx, zero_le_one, Set.indicator_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ 0 ≤ approx (P := P) 0 c x

Tactic:
exact indicator_nonneg (fun _ _ => zero_le_one) _

Premises used: zero_le_one, Set.indicator_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
succ :
  0 ≤
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)
⊢ 0 ≤ approx (P := P) (n + 1) c x

Tactic:
simp only [approx, midpoint_eq_smul_add]

Premises used: midpoint_eq_smul_add, Urysohns.CU.approx
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
⊢ 0 ≤
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)

Tactic:
mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_)

Premises used: Iff.mpr, mul_nonneg, add_nonneg, inv_nonneg, zero_le_two
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
succ : 0 ≤ approx (P := P) n (c.left (P := P)) x
succ₁ : 0 ≤ approx (P := P) n (c.right (P := P)) x
⊢ 0 ≤
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)

Tactic:
refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_)

Premises used: Iff.mpr, mul_nonneg, inv_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
⊢ 0 ≤ approx (P := P) n (c.left (P := P)) x

Tactic:
apply ihn
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
⊢ 0 ≤ approx (P := P) n (c.right (P := P)) x

Tactic:
apply ihn
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero : ∀ (c : CU P), 0 ≤ approx (P := P) 0 c x
succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x) (c : CU P), 0 ≤ approx (P := P) (n + 1) c x
⊢ 0 ≤ approx (P := P) n c x

Tactic:
induction n generalizing c with
  | zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

Premises used: Iff.mpr, mul_nonneg, midpoint_eq_smul_add, Urysohns.CU.approx, zero_le_one, inv_nonneg, Set.indicator_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ approx (P := P) 0 c x ≤ 1

Tactic:
indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one

Premises used: le_rfl, Urysohns.CU.approx, zero_le_one, Set.indicator_apply_le'
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ approx (P := P) 0 c x ≤ 1

Tactic:
exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one

Premises used: le_rfl, zero_le_one, Set.indicator_apply_le'
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
succ : (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1
⊢ approx (P := P) (n + 1) c x ≤ 1

Tactic:
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]

Premises used: midpoint_eq_smul_add, Urysohns.CU.approx, invOf_eq_inv, smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
⊢ approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
have := add_le_add (ihn (left c)) (ihn (right c))
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
this : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ HAdd.hAdd (α := ℝ) 1 1
⊢ approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ 2

Tactic:
norm_num at this
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
this : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ 2
⊢ (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1

Tactic:
Iff.mpr (div_le_one zero_lt_two) this

Premises used: Iff.mpr, div_le_one, zero_lt_two
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
this : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ 2
⊢ (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1

Tactic:
exact Iff.mpr (div_le_one zero_lt_two) this

Premises used: Iff.mpr, div_le_one
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero : ∀ (c : CU P), approx (P := P) 0 c x ≤ 1
succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1) (c : CU P), approx (P := P) (n + 1) c x ≤ 1
⊢ approx (P := P) n c x ≤ 1

Tactic:
induction n generalizing c with
  | zero => exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
    have := add_le_add (ihn (left c)) (ihn (right c))
    norm_num at this
    exact Iff.mpr (div_le_one zero_lt_two) this

Premises used: le_rfl, midpoint_eq_smul_add, Urysohns.CU.approx, zero_le_one, Set.indicator_apply_le', invOf_eq_inv, smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ BddAbove (α := ℝ) (range fun (n : ℕ) ↦ approx (P := P) n c x)

Tactic:
⟨1, fun _ ⟨n, hn⟩ => hn ▸ c.approx_le_one n x⟩

Premises used: _private.0.Urysohns.CU.bddAbove_range_approx.match_1, Eq.rec, LE.le, BddAbove, Urysohns.CU.approx_le_one, Set.Nonempty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
pos : ∀ (hx : x ∈ c₁.U (P := P)), approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
neg : ∀ (hx : x ∉ c₁.U (P := P)), approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
⊢ approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x

Tactic:
by_cases hx : x ∈ c₁.U

Premises used: Urysohns.CU.U
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U (P := P)
⊢ approx (P := P) n₂ c₂ x = 0

Tactic:
approx_of_mem_C _ _ (h hx)

Premises used: Urysohns.CU.approx_of_mem_C
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U (P := P)
⊢ 0 ≤ approx (P := P) n₁ c₁ x

Tactic:
approx_nonneg _ _ _

Premises used: Urysohns.CU.approx_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U (P := P)
⊢ approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x

Tactic:
calc
      approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
      _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _

Premises used: Urysohns.CU.approx_of_mem_C, Urysohns.CU.approx_nonneg, Urysohns.CU.approx
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∉ c₁.U (P := P)
⊢ approx (P := P) n₂ c₂ x ≤ 1

Tactic:
approx_le_one _ _ _

Premises used: Urysohns.CU.approx_le_one
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∉ c₁.U (P := P)
⊢ 1 = approx (P := P) n₁ c₁ x

Tactic:
(approx_of_notMem_U _ _ hx).symm

Premises used: Eq.symm, Urysohns.CU.approx_of_notMem_U
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
hx : x ∉ c₁.U (P := P)
⊢ approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x

Tactic:
calc
      approx n₂ c₂ x ≤ 1 := approx_le_one _ _ _
      _ = approx n₁ c₁ x := (approx_of_notMem_U _ _ hx).symm

Premises used: Urysohns.CU.approx, Urysohns.CU.approx_le_one, Eq.symm, Urysohns.CU.approx_of_notMem_U
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ Membership.mem (γ := Set ℝ)
    (Icc ((c.right (P := P).U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x))
    ((c.U (P := P))ᶜ.indicator 1 x)

Tactic:
⟨le_rfl, ?_⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
zero : LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)
⊢ Membership.mem (γ := Set ℝ)
    (Icc ((c.right (P := P).U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x))
    ((c.U (P := P))ᶜ.indicator 1 x)

Tactic:
refine ⟨le_rfl, ?_⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
h₂ : LE.le (α := ℝ) 0 (1 x)
⊢ LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)

Tactic:
grw [left_U_subset]

Premises used: Urysohns.CU.left_U_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ LE.le (α := ℝ) 0 1

Tactic:
positivity
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn :
  ∀ (c : CU P),
    approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
c : CU P
⊢ midpoint ℝ (approx (P := P) n (c.right (P := P).left (P := P)) x)
        (approx (P := P) n (c.right (P := P).right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ∧
    midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P).left (P := P)) x)
        (approx (P := P) n (c.left (P := P).right (P := P)) x)

Tactic:
⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩

Premises used: midpoint_le_midpoint, And.right, And.left, And.intro