awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 < f x}
have refine : ∀ (s : Set (α × α)),
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
Tactic: refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
have mp : (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
mp :
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
have mpr : (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
have mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
Tactic: rcases hf ε ε₀ with ⟨i, hi, H⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 ≤ f x}
have refine : ∀ (s : Set (α × α)),
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
Tactic: refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
have mp : (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
mp :
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
have mpr : (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
have mp : ∀ (ε' : ℝ≥0∞) (hε' : 0 < ε' ∧ ε' < ε), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
Tactic: rcases exists_between ε₀ with ⟨ε', hε'⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
have mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε'), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
Tactic: rcases hf ε' hε'.1 with ⟨i, hi, H⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist x y < ε
have rw : y ∈ eball x ε ↔ edist y x < ε
Tactic: rw [edist_comm, mem_eball]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : y ∈ eball x ε ↔ edist y x < ε
⊢ y ∈ eball x ε ↔ edist x y < ε
have rw₁ : edist y x < ε ↔ edist y x < ε
Tactic: rw [edist_comm, mem_eball]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε
have rw : y ∈ closedEBall x ε ↔ edist y x ≤ ε
Tactic: rw [edist_comm, mem_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : y ∈ closedEBall x ε ↔ edist y x ≤ ε
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε
have rw₁ : edist y x ≤ ε ↔ edist y x ≤ ε
Tactic: rw [edist_comm, mem_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
h : 0 < ε
⊢ x ∈ eball x ε
have rwa : edist x x < ε
Tactic: rwa [mem_eball, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε
have rw : 0 ≤ ε
Tactic: rw [mem_closedEBall, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ eball y ε ↔ y ∈ eball x ε
have rw : edist y x < ε ↔ y ∈ eball x ε
Tactic: rw [mem_eball', mem_eball]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : edist y x < ε ↔ y ∈ eball x ε
⊢ x ∈ eball y ε ↔ y ∈ eball x ε
have rw₁ : edist y x < ε ↔ edist y x < ε
Tactic: rw [mem_eball', mem_eball]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall y ε ↔ y ∈ closedEBall x ε
have rw : edist y x ≤ ε ↔ y ∈ closedEBall x ε
Tactic: rw [mem_closedEBall', mem_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : edist y x ≤ ε ↔ y ∈ closedEBall x ε
⊢ x ∈ closedEBall y ε ↔ y ∈ closedEBall x ε
have rw₁ : edist y x ≤ ε ↔ edist y x ≤ ε
Tactic: rw [mem_closedEBall', mem_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε
have this : 0 < ε - edist y x
Tactic: have : 0 < ε - edist y x := by simpa using h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε
have refine : edist y x + (ε - edist y x) ≤ ε
Tactic: refine ⟨ε - edist y x, this, eball_subset ?_ (ne_top_of_lt h)⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ edist x x < ∞
have rw : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ eball x 0 = ∅
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [eball_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have simp : edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₉ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
mpr₇ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₈ : edist x a < δ → x ∈ s → ¬edist x a < δ → edist (f x) b < ε ∧ f x ∈ t
Tactic: tauto