awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I : Ideal A
hI : I ∈ F
J : Ideal A
hJ : J ∈ F
⊢ ∃ (z : Set A),
    Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} z ∧ z ⊆ (↑I : Set A) ∩ (↑J : Set A)

Tactic:
exact ⟨I ⊓ J, ⟨I ⊓ J, Order.PFilter.inf_mem hI hJ, rfl⟩, fun _ h ↦ h⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ ∀ {U : Set A}, Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} U → 0 ∈ U

Tactic:
aesop
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ ∀ {U : Set A},
    Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} U →
      ∃ (V : Set A), Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} V ∧ V + V ⊆ U

Tactic:
aesop
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ ∀ {U : Set A},
    Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} U →
      ∃ (V : Set A),
        Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} V ∧ V ⊆ (fun (x : A) ↦ -x) ⁻¹' U

Tactic:
aesop
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ ∀ (x₀ : A) {U : Set A},
    Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} U →
      ∃ (V : Set A),
        Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} V ∧
          V ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' U

Tactic:
aesop
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V * V ⊆ (↑I : Set A)

Tactic:
⟨I, ⟨I, hI, rfl⟩, Set.mul_subset_iff.mpr fun _ h₁ _ h₂ ↦ mul_mem h₁ h₂⟩

Premises used: Iff.mpr, Set.mul_subset_iff, SetLike.coe, And.intro, Exists.intro, rfl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V * V ⊆ (↑I : Set A)

Tactic:
exact ⟨I, ⟨I, hI, rfl⟩, Set.mul_subset_iff.mpr fun _ h₁ _ h₂ ↦ mul_mem h₁ h₂⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
x₀ : A
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑I : Set A)

Tactic:
⟨I, ⟨I, hI, rfl⟩, fun a ha ↦ Ideal.mul_mem_left I x₀ ha⟩

Premises used: SetLike.coe, And.intro, Exists.intro, Ideal.mul_mem_left, rfl
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
x₀ : A
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑I : Set A)

Tactic:
exact ⟨I, ⟨I, hI, rfl⟩, fun a ha ↦ Ideal.mul_mem_left I x₀ ha⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
x₀ : A
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑I : Set A)

Tactic:
⟨I.colon {x₀}, ⟨I.colon {x₀}, IsUniform.colon_mem hI x₀, rfl⟩,
      fun a ha ↦ Set.mem_preimage.mpr (Submodule.mem_colon_singleton.mp ha)⟩

Premises used: Iff.mpr, IdealFilter.IsUniform.colon_mem, Submodule.colon, SetLike.coe, And.intro, Exists.intro, Iff.mp, Submodule.mem_colon_singleton, Singleton.singleton, rfl, Set.mem_preimage
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
x₀ : A
I : Ideal A
hI : I ∈ F
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) V ∧
      V ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑I : Set A)

Tactic:
refine ⟨I.colon {x₀}, ⟨I.colon {x₀}, IsUniform.colon_mem hI x₀, rfl⟩,
      fun a ha ↦ Set.mem_preimage.mpr (Submodule.mem_colon_singleton.mp ha)⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ F.IsUniform ↔
    ∃ (B : RingFilterBasis A),
      Eq.{u_1 + 1} (α := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
        {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}

Tactic:
⟨fun _ ↦ ⟨F.ringFilterBasis, rfl⟩, fun ⟨B, hB⟩ ↦ ⟨fun {I} hI a ↦ ?_⟩⟩

Premises used: IdealFilter.IsUniform, _private.0.IdealFilter.isUniform_iff_exists_ringFilterBasis.match_1, IdealFilter.IsUniform.mk, Iff.intro, Exists.intro, IdealFilter.ringFilterBasis, rfl
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
refine :
  (∃ (B : RingFilterBasis A),
      Eq.{u_1 + 1} (α := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
        {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}) →
    ∀ (B : RingFilterBasis A)
      (hB :
        Eq.{u_1 + 1} (α := Set (Set A))
          (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
          {x : Set A | ∃ I ∈ F, (↑I : Set A) = x})
      {I : Ideal A} (hI : I ∈ F) (a : A), Submodule.colon I {a} ∈ F
⊢ F.IsUniform ↔
    ∃ (B : RingFilterBasis A),
      Eq.{u_1 + 1} (α := Set (Set A))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
        {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}

Tactic:
refine ⟨fun _ ↦ ⟨F.ringFilterBasis, rfl⟩, fun ⟨B, hB⟩ ↦ ⟨fun {I} hI a ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h :
  ∃ (B : RingFilterBasis A),
    Eq.{u_1 + 1} (α := Set (Set A))
      (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
      {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
B : RingFilterBasis A
hB :
  Eq.{u_1 + 1} (α := Set (Set A)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
    {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
I : Ideal A
hI : I ∈ F
a : A
⊢ Membership.mem (γ := Set (Set A)) {x : Set A | ∃ I ∈ F, (↑I : Set A) = x} (↑I : Set A)

Tactic:
simpa
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h :
  ∃ (B : RingFilterBasis A),
    Eq.{u_1 + 1} (α := Set (Set A))
      (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
      {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
B : RingFilterBasis A
hB :
  Eq.{u_1 + 1} (α := Set (Set A)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
    {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
I : Ideal A
hI : I ∈ F
a : A
obtain : ∀ (V : Set A) (hbasis : V ∈ B) (hsub : V ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)), Submodule.colon I {a} ∈ F
⊢ Submodule.colon I {a} ∈ F

Tactic:
obtain ⟨V, hbasis, hsub⟩ := B.mul_right a (U := I) (hB.ge (by simpa))

Premises used: Eq.ge, RingFilterBasis.mul_right
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h :
  ∃ (B : RingFilterBasis A),
    Eq.{u_1 + 1} (α := Set (Set A))
      (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
      {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
B : RingFilterBasis A
hB :
  Eq.{u_1 + 1} (α := Set (Set A)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
    {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
I : Ideal A
hI : I ∈ F
a : A
V : Set A
hbasis : V ∈ B
hsub : V ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)
obtain :
  ∀ (J : Ideal A) (hJ : J ∈ F) (hbasis : (↑J : Set A) ∈ B)
    (hsub : (↑J : Set A) ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)), Submodule.colon I {a} ∈ F
⊢ Submodule.colon I {a} ∈ F

Tactic:
obtain ⟨J, hJ, rfl⟩ := hB.le hbasis

Premises used: Eq.le, rfl
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h :
  ∃ (B : RingFilterBasis A),
    Eq.{u_1 + 1} (α := Set (Set A))
      (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
      {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
B : RingFilterBasis A
hB :
  Eq.{u_1 + 1} (α := Set (Set A)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
    {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
I : Ideal A
hI : I ∈ F
a : A
J : Ideal A
hJ : J ∈ F
hbasis : (↑J : Set A) ∈ B
hsub : (↑J : Set A) ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)
x : A
hx : x ∈ J
⊢ x ∈ Submodule.colon I {a}

Tactic:
simpa using (hsub hx)
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h :
  ∃ (B : RingFilterBasis A),
    Eq.{u_1 + 1} (α := Set (Set A))
      (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
      {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
B : RingFilterBasis A
hB :
  Eq.{u_1 + 1} (α := Set (Set A)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _))
    {x : Set A | ∃ I ∈ F, (↑I : Set A) = x}
I : Ideal A
hI : I ∈ F
a : A
J : Ideal A
hJ : J ∈ F
hbasis : (↑J : Set A) ∈ B
hsub : (↑J : Set A) ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)
⊢ Submodule.colon I {a} ∈ F

Tactic:
exact Order.PFilter.mem_of_le (fun x hx ↦ by simpa using (hsub hx)) hJ

Premises used: Order.PFilter.mem_of_le
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ IsTopologicalAddGroup.{u_1} (WithIdealFilter F)

Tactic:
F.addGroupFilterBasis.isTopologicalAddGroup

Premises used: instRingWithIdealFilter._aux_18, AddGroupFilterBasis.isTopologicalAddGroup, instRingWithIdealFilter._aux_2, WithIdealFilter, instRingWithIdealFilter._aux_17, instRingWithIdealFilter._aux_1, IdealFilter.addGroupFilterBasis
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
mp : s ∈ 𝓝 a → ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
mpr : (∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s) → s ∈ 𝓝 a
⊢ s ∈ 𝓝 a ↔ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s

Tactic:
constructor
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
mp :
  ∀ (t : Set A) (ht : t ∈ F.addGroupFilterBasis) (hts : (fun (y : A) ↦ a + y) '' t ⊆ s),
    ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s

Tactic:
rcases ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.1 hs with ⟨t, ht, hts⟩

Premises used: AddGroupFilterBasis.nhds_hasBasis, Filter.HasBasis.mem_iff, Iff.mp, IdealFilter.addGroupFilterBasis
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
t : Set A
ht : t ∈ F.addGroupFilterBasis
hts : (fun (y : A) ↦ a + y) '' t ⊆ s
mp :
  ∀ (I : Ideal A) (hI : I ∈ F) (hts : (fun (y : A) ↦ a + y) '' (↑I : Set A) ⊆ s),
    ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s

Tactic:
rcases ht with ⟨I, hI, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
I : Ideal A
hI : I ∈ F
hts : (fun (y : A) ↦ a + y) '' (↑I : Set A) ⊆ s
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s

Tactic:
⟨I, hI, hts⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
I : Ideal A
hI : I ∈ F
hts : (fun (y : A) ↦ a + y) '' (↑I : Set A) ⊆ s
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s

Tactic:
exact ⟨I, hI, hts⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ s ∈ 𝓝 a

Tactic:
((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_

Premises used: Iff.mpr, AddGroupFilterBasis.nhds_hasBasis, Filter.HasBasis.mem_iff, Set.Mem, WithIdealFilter, IdealFilter.addGroupFilterBasis
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
mpr : ∃ i ∈ F.addGroupFilterBasis, (fun (y : A) ↦ a + y) '' i ⊆ s
⊢ s ∈ 𝓝 a

Tactic:
refine ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_

Premises used: Iff.mpr, AddGroupFilterBasis.nhds_hasBasis, Filter.HasBasis.mem_iff, IdealFilter.addGroupFilterBasis
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ ∃ i ∈ F.addGroupFilterBasis, (fun (y : A) ↦ a + y) '' i ⊆ s

Tactic:
⟨I, ⟨I, hI, rfl⟩, hIs⟩

Premises used: SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
⊢ ∃ i ∈ F.addGroupFilterBasis, (fun (y : A) ↦ a + y) '' i ⊆ s

Tactic:
exact ⟨I, ⟨I, hI, rfl⟩, hIs⟩
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
s : Set (WithIdealFilter F)
⊢ Membership.mem (γ := Filter (WithIdealFilter F)) (𝓝 0) s ↔ ∃ I ∈ F, idealSet I ⊆ s

Tactic:
simpa [zero_vadd] using mem_nhds_iff (a := 0) (s := s)

Premises used: zero_vadd, WithIdealFilter.mem_nhds_iff
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ IsLinearTopology.{u_1, u_1} (WithIdealFilter F) (WithIdealFilter F)

Tactic:
IsLinearTopology.mk_of_hasBasis' (R := (WithIdealFilter F))
    (M := (WithIdealFilter F))
    (ι := Ideal A) (S := Ideal A)
    (p := fun I : Ideal A ↦ I ∈ F) (s := fun I : Ideal A ↦ I)
    ⟨fun _ ↦ mem_nhds_zero_iff⟩
    (fun I a _ hm ↦ Submodule.smul_mem I a hm)

Premises used: WithIdealFilter.mem_nhds_zero_iff, IsLinearTopology.mk_of_hasBasis', WithIdealFilter, Filter.HasBasis.mk, Submodule.smul_mem
-- Module: Mathlib.RingTheory.IdealFilter.Topology
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
inst_1 : F.IsUniform
⊢ IsTopologicalRing.{u_1} (WithIdealFilter F)

Tactic:
F.ringFilterBasis.isTopologicalRing

Premises used: instRingWithIdealFilter._aux_18, RingFilterBasis.isTopologicalRing, Set.Mem, instRingWithIdealFilter._aux_2, instRingWithIdealFilter._aux_6, WithIdealFilter, instRingWithIdealFilter._aux_17, instRingWithIdealFilter._aux_1, IdealFilter.ringFilterBasis
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
isTrue : i = j → e i * e j = e i
isFalse : ¬i = j → e i * e j = 0
⊢ e i * e j = if i = j then e i else 0

Tactic:
split
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h : i = j
⊢ e i * e j = e i

Tactic:
simp [*, (he.idem j).eq]

Premises used: OrthogonalIdempotents.idem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h : ¬i = j
⊢ e i * e j = 0

Tactic:
he.ortho ‹_›

Premises used: OrthogonalIdempotents.ortho
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h : ¬i = j
⊢ e i * e j = 0

Tactic:
exact he.ortho ‹_›

Premises used: OrthogonalIdempotents.ortho
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : DecidableEq I
H : ∀ (i j : I), e i * e j = if i = j then e i else 0
i : I
⊢ IsIdempotentElem (e i)

Tactic:
simpa using H i i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e_1 : I → R
inst_1 : DecidableEq I
H : ∀ (i j : I), e_1 i * e_1 j = if i = j then e_1 i else 0
i j : I
e : i ≠ j
⊢ (fun (x1 x2 : I) ↦ e_1 x1 * e_1 x2 = 0) i j

Tactic:
simpa [e] using H i j
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ IsIdempotentElem.{u_1} (M := R) (∑ i ∈ s, e i)

Tactic:
simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

Premises used: Finset.mul_sum, IsIdempotentElem, OrthogonalIdempotents.mul_eq, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ IsIdempotentElem.{u_1} (M := R) (∑ i ∈ s, e i)

Tactic:
classical
  simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

Premises used: Finset.mul_sum, IsIdempotentElem, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
simp [Finset.mul_sum, he.mul_eq, h]

Premises used: Finset.mul_sum, OrthogonalIdempotents.mul_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
classical
  simp [Finset.mul_sum, he.mul_eq, h]

Premises used: Finset.mul_sum
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
simp [Finset.mul_sum, he.mul_eq, h]

Premises used: Finset.mul_sum, OrthogonalIdempotents.mul_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
classical
  simp [Finset.mul_sum, he.mul_eq, h]

Premises used: Finset.mul_sum
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)

Tactic:
simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Premises used: OrthogonalIdempotents.iff_mul_eq, apply_ite, map_mul, OrthogonalIdempotents.mul_eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)

Tactic:
classical
  simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Premises used: OrthogonalIdempotents.iff_mul_eq, apply_ite, map_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ OrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e) ↔ OrthogonalIdempotents e

Tactic:
simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Premises used: OrthogonalIdempotents.iff_mul_eq, Function.Injective.eq_iff, apply_ite
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Type u_3
e : I → R
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ OrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e) ↔ OrthogonalIdempotents e

Tactic:
classical
  simp [iff_mul_eq, ← hf.eq_iff, apply_ite]

Premises used: OrthogonalIdempotents.iff_mul_eq, Function.Injective.eq_iff, apply_ite
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
J : Type u_4
i : J ↪ I
⊢ OrthogonalIdempotents.{u_1, u_4} (I := J) (e ∘ (⇑i : (a : J) → I))

Tactic:
simp [iff_mul_eq, he.mul_eq]

Premises used: OrthogonalIdempotents.iff_mul_eq, OrthogonalIdempotents.mul_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
J : Type u_4
i : J ↪ I
⊢ OrthogonalIdempotents.{u_1, u_4} (I := J) (e ∘ (⇑i : (a : J) → I))

Tactic:
classical
  simp [iff_mul_eq, he.mul_eq]

Premises used: OrthogonalIdempotents.iff_mul_eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
J : Type u_4
i : J ≃ I
⊢ OrthogonalIdempotents.{u_1, u_4} (I := J) (e ∘ (⇑i : (a : J) → I)) ↔ OrthogonalIdempotents e

Tactic:
simp [iff_mul_eq, i.forall_congr_left]

Premises used: OrthogonalIdempotents.iff_mul_eq, Equiv.forall_congr_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
J : Type u_4
i : J ≃ I
⊢ OrthogonalIdempotents.{u_1, u_4} (I := J) (e ∘ (⇑i : (a : J) → I)) ↔ OrthogonalIdempotents e

Tactic:
classical
  simp [iff_mul_eq, i.forall_congr_left]

Premises used: OrthogonalIdempotents.iff_mul_eq, Equiv.forall_congr_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
inst_1 : Unique I
⊢ OrthogonalIdempotents e ↔ IsIdempotentElem (e default)

Tactic:
simp only [orthogonalIdempotents_iff, Unique.forall_iff, Subsingleton.pairwise, and_true]

Premises used: and_true, orthogonalIdempotents_iff, Unique.forall_iff, Subsingleton.pairwise
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
i j : Option I
ne : i ≠ j
none : ∀ (ne : Option.none ≠ j), Option.elim Option.none x e * j.elim x e = 0
some : ∀ (i : I) (ne : Option.some i ≠ j), (Option.some i).elim x e * j.elim x e = 0
⊢ i.elim x e * j.elim x e = 0

Tactic:
rcases i with - | i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
j : Option I
ne : Option.none ≠ j
none :
  ∀ (ne : Ne.{u_3 + 1} (α := Option I) Option.none Option.none),
    Option.elim Option.none x e * Option.elim Option.none x e = 0
none₁ : ∀ (j : I) (ne : Option.none ≠ some j), Option.elim Option.none x e * (some j).elim x e = 0
⊢ Option.elim Option.none x e * j.elim x e = 0

Tactic:
rcases j with - | j
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst_1 : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i : I, e i = 0
hx₂ : (∑ i : I, e i) * x = 0
j : Option I
i : I
ne : Option.some i ≠ j
some : ∀ (ne : Option.some i ≠ none), (Option.some i).elim x e * Option.elim none x e = 0
some₁ : ∀ (j : I) (ne : Option.some i ≠ Option.some j), (Option.some i).elim x e * (Option.some j).elim x e = 0
⊢ (Option.some i).elim x e * j.elim x e = 0

Tactic:
rcases j with - | j