internlm/Lean-Github huggingface dataset:
Theorem: Matroid.restrict_indep_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hI : M.Indep I
⊢ M ↾ I = freeOn I
Tactic:
refine eq_of_indep_iff_indep_forall rfl (fun J _ ↦ ?_)
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ (M ↾ I).Indep J ↔ (freeOn I).Indep J
Theorem: Matroid.restrict_indep_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ (M ↾ I).Indep J ↔ (freeOn I).Indep J
Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, freeOn_indep_iff, and_iff_right_iff_imp]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ J ⊆ I → M.Indep J
Theorem: Matroid.restrict_indep_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ J ⊆ I → M.Indep J
Tactic:
exact hI.subset
Proof state after:
no goals
Theorem: Matroid.indep_iff_restrict_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M.Indep I ↔ M ↾ I = freeOn I
Tactic:
refine ⟨restrict_indep_eq_freeOn, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
⊢ M.Indep I
Theorem: Matroid.indep_iff_restrict_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
⊢ M.Indep I
Tactic:
have h' := restrict_indep_iff (M := M) (I := I) (R := I)
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
h' : (M ↾ I).Indep I ↔ M.Indep I ∧ I ⊆ I
⊢ M.Indep I
Theorem: Matroid.indep_iff_restrict_eq_freeOn
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
h' : (M ↾ I).Indep I ↔ M.Indep I ∧ I ⊆ I
⊢ M.Indep I
Tactic:
rwa [h, freeOn_indep_iff, iff_true_intro Subset.rfl, and_true, true_iff] at h'
Proof state after:
no goals
Theorem: Matroid.restrict_subset_loops_eq
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
⊢ M ↾ X = loopyOn X
Tactic:
refine eq_of_indep_iff_indep_forall rfl (fun I hI ↦ ?_)
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ (M ↾ X).Indep I ↔ (loopyOn X).Indep I
Theorem: Matroid.restrict_subset_loops_eq
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ (M ↾ X).Indep I ↔ (loopyOn X).Indep I
Tactic:
simp only [restrict_indep_iff, loopyOn_indep_iff]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ M.Indep I ∧ I ⊆ X ↔ I = ∅
Theorem: Matroid.restrict_subset_loops_eq
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ M.Indep I ∧ I ⊆ X ↔ I = ∅
Tactic:
use fun h ↦ h.1.eq_empty_of_subset_loops (h.2.trans hX)
Proof state after:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ I = ∅ → M.Indep I ∧ I ⊆ X
Theorem: Matroid.restrict_subset_loops_eq
Proof state before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ I = ∅ → M.Indep I ∧ I ⊆ X
Tactic:
rintro rfl
Proof state after:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
hI : ∅ ⊆ (M ↾ X).E
⊢ M.Indep ∅ ∧ ∅ ⊆ X
Theorem: Matroid.restrict_subset_loops_eq
Proof state before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
hI : ∅ ⊆ (M ↾ X).E
⊢ M.Indep ∅ ∧ ∅ ⊆ X
Tactic:
simp
Proof state after:
no goals
Theorem: tsum_support_eq
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
⊢ ∑' (x : ↑(support f)), f ↑x = ∑' (x : α), f x
Tactic:
simp [tsum_subtype]
Proof state after:
no goals
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∑' (x : ↑(s ∩ support f)), f ↑x = ∑' (x : ↑s), f ↑x
Tactic:
rw [tsum_congr (show ∀ (a : s), f a = (s.indicator f) a from _),
  tsum_congr ((show ∀ (a : ↑ (s ∩ f.support)), f a = (s.indicator f) a from _)),
  tsum_subtype_eq_of_support_subset (by simp), tsum_subtype_eq_of_support_subset (by simp)]
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑(s ∩ support f)), f ↑a = s.indicator f ↑a

α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑s), f ↑a = s.indicator f ↑a
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑s), f ↑a = s.indicator f ↑a
Tactic:
rintro ⟨a, ha⟩
Proof state after:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Tactic:
simp [indicator_of_mem ha]
Proof state after:
no goals
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ support (s.indicator f) ⊆ s ∩ support f
Tactic:
simp
Proof state after:
no goals
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ support (s.indicator f) ⊆ s
Tactic:
simp
Proof state after:
no goals
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑(s ∩ support f)), f ↑a = s.indicator f ↑a
Tactic:
rintro ⟨a,ha⟩
Proof state after:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s ∩ support f
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Theorem: tsum_inter_support_eq_tsum_subtype
Proof state before:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s ∩ support f
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Tactic:
simp [indicator_of_mem ha.1]
Proof state after:
no goals
Theorem: tsum_subtype_eq_tsum_subtype
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s t : Set α
h : s ∩ support f = t ∩ support f
⊢ ∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
Tactic:
rw [← tsum_inter_support_eq_tsum_subtype, eq_comm, ← tsum_inter_support_eq_tsum_subtype, h]
Proof state after:
no goals
Theorem: ENat.eq_top_iff_forall_lt
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ n = ⊤ ↔ ∀ (m : ℕ), ↑m < n
Tactic:
refine ⟨fun h m ↦ h ▸ coe_lt_top m ,fun h ↦ ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ n = ⊤
Theorem: ENat.eq_top_iff_forall_lt
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ n = ⊤
Tactic:
rw [← not_not (a := (n = ⊤)), ← Ne, ne_top_iff_exists]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ ¬∃ a, ↑a = n
Theorem: ENat.eq_top_iff_forall_lt
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ ¬∃ a, ↑a = n
Tactic:
rintro ⟨a, rfl⟩
Proof state after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
a : ℕ
h : ∀ (m : ℕ), ↑m < ↑a
⊢ False
Theorem: ENat.eq_top_iff_forall_lt
Proof state before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
a : ℕ
h : ∀ (m : ℕ), ↑m < ↑a
⊢ False
Tactic:
exact (h a).ne rfl
Proof state after:
no goals
Theorem: ENat.iInf_ne_top
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
inst✝ : CompleteLattice α
f : ℕ∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x
Tactic:
rw [iInf_subtype', cinfi_ne_top]
Proof state after:
no goals
Theorem: ENat.indicator_support_le
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
⊢ (support f).indicator 1 i ≤ f i
Tactic:
by_cases hi : i ∈ support f
Proof state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∈ support f
⊢ (support f).indicator 1 i ≤ f i

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ (support f).indicator 1 i ≤ f i
Theorem: ENat.indicator_support_le
Proof state before:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ (support f).indicator 1 i ≤ f i
Tactic:
rw [indicator_apply_eq_zero.2 (fun h ↦ (hi h).elim)]
Proof state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ 0 ≤ f i
Theorem: ENat.indicator_support_le
Proof state before:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ 0 ≤ f i
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: ENat.indicator_support_le
Proof state before:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∈ support f
⊢ (support f).indicator 1 i ≤ f i
Tactic:
rwa [indicator_apply_eq_self.2 (fun h ↦ (h hi).elim), Pi.one_apply, ENat.one_le_iff_ne_zero]
Proof state after:
no goals
Theorem: ENat.embedding_coe
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ (range Nat.cast).OrdConnected
Tactic:
rw [range_coe']
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ (Iio ⊤).OrdConnected
Theorem: ENat.embedding_coe
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ (Iio ⊤).OrdConnected
Tactic:
exact ordConnected_Iio
Proof state after:
no goals
Theorem: ENat.isOpen_image_coe
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ
⊢ IsOpen (Nat.cast '' s)
Tactic:
rw [← openEmbedding_coe.open_iff_image_open]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ
⊢ IsOpen s
Theorem: ENat.isOpen_image_coe
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ
⊢ IsOpen s
Tactic:
exact trivial
Proof state after:
no goals
Theorem: ENat.isOpen_singleton
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n x : ℕ∞
hx : x ≠ ⊤
⊢ IsOpen {x}
Tactic:
lift x to ℕ using hx
Proof state after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {↑x}
Theorem: ENat.isOpen_singleton
Proof state before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {↑x}
Tactic:
rw [← image_singleton, ← openEmbedding_coe.open_iff_image_open]
Proof state after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {x}
Theorem: ENat.isOpen_singleton
Proof state before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
x : ℕ
⊢ IsOpen {x}
Tactic:
exact trivial
Proof state after:
no goals
Theorem: ENat.isOpen_of_top_not_mem
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ IsOpen s
Tactic:
convert isOpen_image_coe ((↑) ⁻¹' s)
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ s = Nat.cast '' (Nat.cast ⁻¹' s)
Theorem: ENat.isOpen_of_top_not_mem
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ s = Nat.cast '' (Nat.cast ⁻¹' s)
Tactic:
simp_rw [eq_comm (a := s), image_preimage_eq_iff, range_coe', Iio, lt_top_iff_ne_top,
  ← compl_singleton_eq, subset_compl_singleton_iff]
Proof state after:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ ⊤ ∉ s
Theorem: ENat.isOpen_of_top_not_mem
Proof state before:
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ ⊤ ∉ s
Tactic:
assumption
Proof state after:
no goals
Theorem: ENat.mem_nhds_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s
Tactic:
rw [_root_.mem_nhds_iff]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s
Theorem: ENat.mem_nhds_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s
Tactic:
exact ⟨fun ⟨_, h, _, h'⟩ ↦ h h', fun h ↦ ⟨_, singleton_subset_iff.2 h, isOpen_singleton hx, rfl⟩⟩
Proof state after:
no goals
Theorem: ENat.nhds_cast_eq
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}
Tactic:
ext
Proof state after:
case a
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
s✝ : Set ℕ∞
⊢ s✝ ∈ 𝓝 ↑n ↔ s✝ ∈ 𝓟 {↑n}
Theorem: ENat.nhds_cast_eq
Proof state before:
case a
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
s✝ : Set ℕ∞
⊢ s✝ ∈ 𝓝 ↑n ↔ s✝ ∈ 𝓟 {↑n}
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.nhds_eq
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
hn : n ≠ ⊤
⊢ 𝓝 n = 𝓟 {n}
Tactic:
lift n to ℕ using hn
Proof state after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}
Theorem: ENat.nhds_eq
Proof state before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.nhds_top
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ 𝓝 ⊤ = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
Tactic:
simp_rw [nhds_top_order, Ioi, lt_top_iff_ne_top]
Proof state after:
no goals
Theorem: ENat.nhds_top'
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ 𝓝 ⊤ = ⨅ a, 𝓟 (Ioi ↑a)
Tactic:
refine nhds_top.trans <| iInf_ne_top _
Proof state after:
no goals
Theorem: ENat.nhds_cast_cast
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ 𝓝 (↑m, ↑n) = 𝓟 {(↑m, ↑n)}
Tactic:
rw [((openEmbedding_coe.prod openEmbedding_coe).map_nhds_eq (m, n)).symm]
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ Filter.map (fun x => (↑x.1, ↑x.2)) (𝓝 (m, n)) = 𝓟 {(↑m, ↑n)}
Theorem: ENat.nhds_cast_cast
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ Filter.map (fun x => (↑x.1, ↑x.2)) (𝓝 (m, n)) = 𝓟 {(↑m, ↑n)}
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.nhds_cast_top
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
m : ℕ
⊢ 𝓝 (↑m, ⊤) = 𝓟 {↑m} ×ˢ ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
Tactic:
rw [nhds_prod_eq, nhds_cast_eq, nhds_top, principal_singleton]
Proof state after:
no goals
Theorem: ENat.tendsto_nhds_top_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
m : α → ℕ∞
f : Filter α
⊢ Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℕ), ∀ᶠ (a : α) in f, ↑x < m a
Tactic:
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
clear n ι β s α
Proof state after:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Theorem: ENat.tendsto_mul
Proof state before:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
wlog h : b ≤ a with h'
Proof state after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h' : ∀ {a b : ℕ∞}, a ≠ 0 ∨ b ≠ ⊤ → b ≠ 0 ∨ a ≠ ⊤ → b ≤ a → Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
h : ¬b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Theorem: ENat.tendsto_mul
Proof state before:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
obtain (rfl | ha') := eq_or_ne a ⊤
Proof state after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
ha' : a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Theorem: ENat.tendsto_mul
Proof state before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
ha' : a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
lift a to ℕ using ha'
Proof state after:
case inr.intro
b : ℕ∞
a : ℕ
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
h : b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))
Theorem: ENat.tendsto_mul
Proof state before:
case inr.intro
b : ℕ∞
a : ℕ
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
h : b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))
Tactic:
lift b to ℕ using (h.trans_lt (WithTop.coe_lt_top a)).ne
Proof state after:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))
Theorem: ENat.tendsto_mul
Proof state before:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))
Tactic:
rw [← Nat.cast_mul, nhds_cast_cast, nhds_cast_eq]
Proof state after:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓟 {(↑a, ↑b)}) (𝓟 {↑(a * b)})
Theorem: ENat.tendsto_mul
Proof state before:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓟 {(↑a, ↑b)}) (𝓟 {↑(a * b)})
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h' : ∀ {a b : ℕ∞}, a ≠ 0 ∨ b ≠ ⊤ → b ≠ 0 ∨ a ≠ ⊤ → b ≤ a → Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
h : ¬b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
specialize h' hb ha (not_le.1 h).le
Proof state after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Theorem: ENat.tendsto_mul
Proof state before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
rw [nhds_swap a b, mul_comm, tendsto_map'_iff]
Proof state after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto ((fun p => p.1 * p.2) ∘ Prod.swap) (𝓝 (b, a)) (𝓝 (b * a))
Theorem: ENat.tendsto_mul
Proof state before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto ((fun p => p.1 * p.2) ∘ Prod.swap) (𝓝 (b, a)) (𝓝 (b * a))
Tactic:
convert h'
Proof state after:
case h.e'_3.h
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
x✝ : ℕ∞ × ℕ∞
⊢ ((fun p => p.1 * p.2) ∘ Prod.swap) x✝ = x✝.1 * x✝.2
Theorem: ENat.tendsto_mul
Proof state before:
case h.e'_3.h
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
x✝ : ℕ∞ × ℕ∞
⊢ ((fun p => p.1 * p.2) ∘ Prod.swap) x✝ = x✝.1 * x✝.2
Tactic:
simp [mul_comm]
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))
Tactic:
rw [top_mul (by simpa using hb), tendsto_nhds_top_iff]
Proof state after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ ∀ (x : ℕ), ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Theorem: ENat.tendsto_mul
Proof state before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ ∀ (x : ℕ), ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Tactic:
intro x
Proof state after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Theorem: ENat.tendsto_mul
Proof state before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Tactic:
refine hforall.mono ?_
Proof state after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (x_1 : ℕ∞ × ℕ∞), ↑x < x_1.1 ∧ 0 < x_1.2 → ↑x < x_1.1 * x_1.2
Theorem: ENat.tendsto_mul
Proof state before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (x_1 : ℕ∞ × ℕ∞), ↑x < x_1.1 ∧ 0 < x_1.2 → ↑x < x_1.1 * x_1.2
Tactic:
simp only [and_imp, Prod.forall, ← ENat.one_le_iff_pos]
Proof state after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (a b : ℕ∞), ↑x < a → 1 ≤ b → ↑x < a * b
Theorem: ENat.tendsto_mul
Proof state before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (a b : ℕ∞), ↑x < a → 1 ≤ b → ↑x < a * b
Tactic:
exact fun y z hy hz ↦ hy.trans_le <| le_mul_of_one_le_right' hz
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ b ≠ 0
Tactic:
simpa using hb
Proof state after:
no goals
Theorem: ENat.tendsto_mul
Proof state before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
Tactic:
refine (lt_mem_nhds (show (x : ℕ∞) < ⊤ from WithTop.coe_lt_top x)).prod_nhds ?_
Proof state after:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Theorem: ENat.tendsto_mul
Proof state before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Tactic:
obtain (rfl | hbne) := eq_or_ne b ⊤
Proof state after:
case inl
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ⊤, 0 < y

case inr
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hbne : b ≠ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Theorem: ENat.tendsto_mul
Proof state before:
case inr
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hbne : b ≠ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Tactic:
lift b to ℕ using hbne
Proof state after:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ↑b, 0 < y