internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = (dividedPowers hI hJ hIJ).dpow n (a + b)
Tactic:
simp only [IdealAdd.dividedPowers, dpow_eq hI hJ hIJ n ha hb]
Proof state after:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hsup.dpow k a * hsup.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hsup.dpow x a * hsup.dpow (n - x) b = hI.dpow x a * hJ.dpow (n - x) b
Theorem: DividedPowers.IdealAdd.dpow_unique
Proof state before:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (n + 1), hsup.dpow x a * hsup.dpow (n - x) b = hI.dpow x a * hJ.dpow (n - x) b
Tactic:
intro k _
Proof state after:
case h_eq.intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hsup : DividedPowers (I + J)
hI' : ∀ (n : ℕ), ∀ a ∈ I, hI.dpow n a = hsup.dpow n a
hJ' : ∀ (n : ℕ), ∀ b ∈ J, hJ.dpow n b = hsup.dpow n b
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a :=
  fun n a ha =>
    Eq.mpr
      (id
        (congrArg (fun _a => _a = hJ.dpow n a)
          (hI' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).left)))
      (Eq.mpr
        (id
          (congrArg (fun _a => hsup.dpow n a = _a)
            (hJ' n a (Eq.mp (congrArg (fun _a => _a) (propext Submodule.mem_inf)) ha).right)))
        (Eq.refl (hsup.dpow n a)))
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hsup.dpow k a * hsup.dpow (n - k) b = hI.dpow k a * hJ.dpow (n - k) b
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ τ ≤ τ' ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a
Tactic:
rw [le_iff_nhds]
Proof state after:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a
Tactic:
rw [forall_comm]
Proof state after:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (b : α) (a : Set α), b ∈ a → a ∈ nhds b → a ∈ nhds b
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (b : α) (a : Set α), b ∈ a → a ∈ nhds b → a ∈ nhds b
Tactic:
apply forall_congr'
Proof state after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
⊢ ∀ (a : α), nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
⊢ ∀ (a : α), nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
intro a
Proof state after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
rw [Filter.le_def]
Proof state after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ (∀ x ∈ nhds a, x ∈ nhds a) ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ (∀ x ∈ nhds a, x ∈ nhds a) ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
apply forall_congr'
Proof state after:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ ∀ (a_1 : Set α), a_1 ∈ nhds a → a_1 ∈ nhds a ↔ a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ ∀ (a_1 : Set α), a_1 ∈ nhds a → a_1 ∈ nhds a ↔ a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
intro s
Proof state after:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ nhds a → s ∈ nhds a ↔ a ∈ s → s ∈ nhds a → s ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ nhds a → s ∈ nhds a ↔ a ∈ s → s ∈ nhds a → s ∈ nhds a
Tactic:
constructor
Proof state after:
case h.h.mp
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (s ∈ nhds a → s ∈ nhds a) → a ∈ s → s ∈ nhds a → s ∈ nhds a

case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (a ∈ s → s ∈ nhds a → s ∈ nhds a) → s ∈ nhds a → s ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h.h.mp
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (s ∈ nhds a → s ∈ nhds a) → a ∈ s → s ∈ nhds a → s ∈ nhds a
Tactic:
exact fun h _ ↦ h
Proof state after:
no goals
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (a ∈ s → s ∈ nhds a → s ∈ nhds a) → s ∈ nhds a → s ∈ nhds a
Tactic:
intro h
Proof state after:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
⊢ s ∈ nhds a → s ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
by_cases ha : a ∈ s
Proof state after:
case pos
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∈ s
⊢ s ∈ nhds a → s ∈ nhds a

case neg
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∉ s
⊢ s ∈ nhds a → s ∈ nhds a
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case pos
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∈ s
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
exact h ha
Proof state after:
no goals
Theorem: TopologicalSpace.le_iff_nhds_le
Proof state before:
case neg
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∉ s
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
exact fun hs ↦ False.elim (ha (mem_of_mem_nhds hs))
Proof state after:
no goals
Theorem: mem_nhds_add_iff
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) ↔ Add.add a ⁻¹' V ∈ nhds b
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b

case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Theorem: mem_nhds_add_iff
Proof state before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b

case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Tactic:
. exact fun hV => ContinuousAt.preimage_mem_nhds (continuous_add_left a).continuousAt hV
Proof state after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Theorem: mem_nhds_add_iff
Proof state before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b
Tactic:
exact fun hV => ContinuousAt.preimage_mem_nhds (continuous_add_left a).continuousAt hV
Proof state after:
no goals
Theorem: mem_nhds_add_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Tactic:
intro hV
Proof state after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V ∈ nhds (a + b)
Theorem: mem_nhds_add_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V ∈ nhds (a + b)
Tactic:
suffices h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) by
  rw [h]
  apply ContinuousAt.preimage_mem_nhds (continuous_add_left (-a)).continuousAt
  convert hV
  apply neg_add_cancel_left
Proof state after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
Theorem: mem_nhds_add_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
Tactic:
rw [Set.preimage_preimage, eq_comm]
Proof state after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ (fun x => Add.add a (Add.add (-a) x)) ⁻¹' V = V
Theorem: mem_nhds_add_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ (fun x => Add.add a (Add.add (-a) x)) ⁻¹' V = V
Tactic:
convert Set.preimage_id'
Proof state after:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
x✝ : α
⊢ Add.add a (Add.add (-a) x✝) = x✝
Theorem: mem_nhds_add_iff
Proof state before:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
x✝ : α
⊢ Add.add a (Add.add (-a) x✝) = x✝
Tactic:
apply add_neg_cancel_left a
Proof state after:
no goals
Theorem: mem_nhds_add_iff
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ V ∈ nhds (a + b)
Tactic:
rw [h]
Proof state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) ∈ nhds (a + b)
Theorem: mem_nhds_add_iff
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) ∈ nhds (a + b)
Tactic:
apply ContinuousAt.preimage_mem_nhds (continuous_add_left (-a)).continuousAt
Proof state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add a ⁻¹' V ∈ nhds (-a + (a + b))
Theorem: mem_nhds_add_iff
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add a ⁻¹' V ∈ nhds (-a + (a + b))
Tactic:
convert hV
Proof state after:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ -a + (a + b) = b
Theorem: mem_nhds_add_iff
Proof state before:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ -a + (a + b) = b
Tactic:
apply neg_add_cancel_left
Proof state after:
no goals
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ τ = τ' ↔ nhds 0 = nhds 0
Tactic:
rw [TopologicalSpace.ext_iff_nhds]
Proof state after:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) ↔ nhds 0 = nhds 0
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) ↔ nhds 0 = nhds 0
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) → nhds 0 = nhds 0

case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ nhds 0 = nhds 0 → ∀ (x : α), nhds x = nhds x
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) → nhds 0 = nhds 0
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : ∀ (x : α), nhds x = nhds x
⊢ nhds 0 = nhds 0
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : ∀ (x : α), nhds x = nhds x
⊢ nhds 0 = nhds 0
Tactic:
exact h 0
Proof state after:
no goals
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ nhds 0 = nhds 0 → ∀ (x : α), nhds x = nhds x
Tactic:
intro h a
Proof state after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
⊢ nhds a = nhds a
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
⊢ nhds a = nhds a
Tactic:
ext s
Proof state after:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds a ↔ s ∈ nhds a
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds a ↔ s ∈ nhds a
Tactic:
rw [← add_zero a]
Proof state after:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds (a + 0) ↔ s ∈ nhds (a + 0)
Theorem: TopologicalAddGroup.ext_iff_nhds_zero
Proof state before:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds (a + 0) ↔ s ∈ nhds (a + 0)
Tactic:
simp only [mem_nhds_add_iff, h]
Proof state after:
no goals
Theorem: Ideal.IsBasis.ofComm
Proof state before:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ a * r ∈ B i
Tactic:
rw [mul_comm]
Proof state after:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ r * a ∈ B i
Theorem: Ideal.IsBasis.ofComm
Proof state before:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ r * a ∈ B i
Tactic:
refine' Ideal.mul_mem_left (B i) r h
Proof state after:
no goals
Theorem: Ideal.IsBasis.toRingSubgroupsBasis
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
u : α
⊢ u ∈ ↑(Submodule.toAddSubgroup (B i)) * ↑(Submodule.toAddSubgroup (B i)) → u ∈ ↑(Submodule.toAddSubgroup (B i))
Tactic:
rintro ⟨x, _, _, hy, rfl⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
x : α
left✝ : x ∈ ↑(Submodule.toAddSubgroup (B i))
w✝ : α
hy : w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
⊢ (fun x x_1 => x * x_1) x w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
Theorem: Ideal.IsBasis.toRingSubgroupsBasis
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
x : α
left✝ : x ∈ ↑(Submodule.toAddSubgroup (B i))
w✝ : α
hy : w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
⊢ (fun x x_1 => x * x_1) x w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
Tactic:
exact Ideal.mul_mem_left _ _ hy
Proof state after:
no goals
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ s ∈ nhds 0 ↔ ∃ i, ↑(B i) ∈ nhds 0 ∧ ↑(B i) ⊆ s
Tactic:
simp only [AddGroupFilterBasis.nhds_eq, AddGroupFilterBasis.N_zero,
  Filter.IsBasis.mem_filter_iff, FilterBasis.mem_filter_iff]
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔
    ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔
    ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) →
    ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s

case mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s) →
    ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof state before:
case mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) →
    ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s
Tactic:
rintro ⟨t, ⟨i, rfl⟩, hts⟩
Proof state after:
case mp.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
i : ι
hts : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof state before:
case mp.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
i : ι
hts : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s
Tactic:
simp only [Submodule.coe_toAddSubgroup] at hts
Proof state after:
case mp.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
i : ι
hts : ↑(B i) ⊆ s
⊢ ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s