awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, y + z * x}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
Tactic: rw [mul_comm, span_pair_add_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y + z * x}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_add_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {z * y + x, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {y * z + x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_right_mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {y * z + x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {z * y + x, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_right_mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, z * x + y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, x * z + y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_left_mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, x * z + y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, z * x + y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_left_mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x - y * z + y * z, y}) (span {x, y})
Tactic: rw [← span_pair_add_right_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x - y * z + y * z, y}) (span {x, y})
z₁ : α
⊢ Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_add_right_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y - x * z + x * z}) (span {x, y})
Tactic: rw [← span_pair_add_left_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y - x * z + x * z}) (span {x, y})
z₁ : α
⊢ Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_add_left_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x - z * y, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_sub_right_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x - z * y, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_sub_right_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, y - z * x}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})
Tactic: rw [mul_comm, span_pair_sub_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y - z * x}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_sub_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔
    Membership.mem (γ := Submodule R R) (Ideal.span {1 - e}) x
have rw : Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔ ∃ (a : R), a * (1 - e) = x
Tactic: rw [Ideal.mem_span_singleton']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
⊢ x * (1 - e) = x
have rw : x * 1 - x * e = x
Tactic: rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
rw : x * 1 - x * e = x
⊢ x * (1 - e) = x
have rw₁ : x * 1 - 0 = x
Tactic: rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
rw : x * 1 - x * e = x
rw₁ : x * 1 - 0 = x
⊢ x * (1 - e) = x
have rw₂ : x - 0 = x
Tactic: rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
rw : x * 1 - x * e = x
rw₁ : x * 1 - 0 = x
rw₂ : x - 0 = x
⊢ x * (1 - e) = x
have rw₃ : x = x
Tactic: rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔ ∃ (a : R), a * (1 - e) = x
have refine : ∀ (h : ∃ (a : R), a * (1 - e) = x),
  Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
Tactic: refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : ∃ (a : R), a * (1 - e) = x
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
have obtain : ∀ (x : R), Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) (x * (1 - e))
Tactic: obtain ⟨x, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) (x * (1 - e))
have change : x * (1 - e) * e = 0
Tactic: change x * (1 - e) * e = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0
have rw : x * ((1 - e) * e) = 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw : x * ((1 - e) * e) = 0
⊢ x * (1 - e) * e = 0
have rw₁ : x * (1 * e - e * e) = 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw : x * ((1 - e) * e) = 0
rw₁ : x * (1 * e - e * e) = 0
⊢ x * (1 - e) * e = 0
have rw₂ : x * (e - e * e) = 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw : x * ((1 - e) * e) = 0
rw₁ : x * (1 * e - e * e) = 0
rw₂ : x * (e - e * e) = 0
⊢ x * (1 - e) * e = 0
have rw₃ : x * (e - e) = 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw : x * ((1 - e) * e) = 0
rw₁ : x * (1 * e - e * e) = 0
rw₂ : x * (e - e * e) = 0
rw₃ : x * (e - e) = 0
⊢ x * (1 - e) * e = 0
have rw₄ : x * 0 = 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw : x * ((1 - e) * e) = 0
rw₁ : x * (1 * e - e * e) = 0
rw₂ : x * (e - e * e) = 0
rw₃ : x * (e - e) = 0
rw₄ : x * 0 = 0
⊢ x * (1 - e) * e = 0
have rw₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ Eq (α := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e))) (Ideal.span {e})
have rw : Eq (α := Submodule R R) (Ideal.span {1 - (1 - e)}) (Ideal.span {e})
Tactic: rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
rw : Eq (α := Submodule R R) (Ideal.span {1 - (1 - e)}) (Ideal.span {e})
⊢ Eq (α := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e))) (Ideal.span {e})
have rw₁ : Eq (α := Submodule R R) (Ideal.span {e}) (Ideal.span {e})
Tactic: rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K
have mp : F.IsTorsionQuot (L ⊓ K) K → F.IsTorsionQuot L K
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
mp : F.IsTorsionQuot (L ⊓ K) K → F.IsTorsionQuot L K
⊢ F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K
have mpr : F.IsTorsionQuot L K → F.IsTorsionQuot (L ⊓ K) K
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}
have mp : ∀ (I : Ideal A) (hI : I ∈ F) (hI_le : I ≤ Submodule.colon (L ⊓ K) {k}), ∃ I ∈ F, I ≤ Submodule.colon L {k}
Tactic: rcases h k hk with ⟨I, hI, hI_le⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (hypothesis)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}
have hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
Tactic: have hcol : (L ⊓ K).colon {k} = Submodule.colon L {k} :=
      Submodule.colon_inf_eq_left_of_subset (Set.singleton_subset_iff.mpr hk)
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
have mpr : ∀ (I : Ideal A) (hI : I ∈ F) (hI_le : I ≤ Submodule.colon L {k}), ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
Tactic: rcases h k hk with ⟨I, hI, hI_le⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (hypothesis)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
have hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
Tactic: have hcol : (L ⊓ K).colon {k} = Submodule.colon L {k} :=
      Submodule.colon_inf_eq_left_of_subset (Set.singleton_subset_iff.mpr hk)
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}
have obtain : ∀ (J : Ideal A) (hJ : J ∈ (↑F : Set (Ideal A))), ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}
Tactic: obtain ⟨J, hJ⟩ := F.nonempty
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
x : A
hx : x ∈ K
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
have obtain : ∀ (I' : Ideal A) (hI'F : I' ∈ F) (hI'x : I' ≤ Submodule.colon I {x}), ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
Tactic: obtain ⟨I', hI'F, hI'x⟩ := hI x hx
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
x : A
hx : x ∈ K
I' : Ideal A
hI'F : I' ∈ F
hI'x : I' ≤ Submodule.colon I {x}
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
have obtain : ∀ (J' : Ideal A) (hJ'F : J' ∈ F) (hJ'x : J' ≤ Submodule.colon J {x}), ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
Tactic: obtain ⟨J', hJ'F, hJ'x⟩ := hJ x hx
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
⊢ Order.IsPFilter.{u_1} (P := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
have nonempty : Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
Tactic: refine Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
nonempty : Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
⊢ Order.IsPFilter.{u_1} (P := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
have directed : DirectedOn (fun (x1 x2 : Ideal A) ↦ x1 ≥ x2) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
Tactic: refine Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
nonempty : Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
directed : DirectedOn (fun (x1 x2 : Ideal A) ↦ x1 ≥ x2) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
⊢ Order.IsPFilter.{u_1} (P := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
have mem_of_le : ∀ {x y : Ideal A},
  x ≤ y →
    Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} x →
      Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} y
Tactic: refine Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
⊢ Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
have nonempty : ∀ (J : Ideal A) (hJ : J ∈ (↑G : Set (Ideal A))),
  Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}
Tactic: obtain ⟨J, hJ⟩ := G.nonempty
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
I K : Ideal A
hK : K ∈ G
hIK : F.IsTorsionQuot I K
J L : Ideal A
hL : L ∈ G
hJL : F.IsTorsionQuot J L
⊢ ∃ (z : Ideal A),
    Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} z ∧
      (fun (x1 x2 : Ideal A) ↦ x1 ≥ x2) I z ∧ (fun (x1 x2 : Ideal A) ↦ x1 ≥ x2) J z
have directed : Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} (I ⊓ J)
Tactic: refine ⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
I J : Ideal A
hIJ : I ≤ J
⊢ Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} I →
    Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} J
have mem_of_le : ∀ (K : Ideal A) (hK : K ∈ G) (hIK : F.IsTorsionQuot I K),
  Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} J
Tactic: ⟨K, hK, hIK⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
⊢ F.IsGabriel ↔ F.IsUniform ∧ F • F = F
have mp : F.IsGabriel → F.IsUniform ∧ F • F = F
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
mp : F.IsGabriel → F.IsUniform ∧ F • F = F
⊢ F.IsGabriel ↔ F.IsUniform ∧ F • F = F
have mpr : F.IsUniform ∧ F • F = F → F.IsGabriel
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
⊢ F.IsUniform ∧ F • F = F
have mp : F • F = F
Tactic: refine ⟨hF.toIsUniform, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
⊢ F • F = F
have mp : ∀ (I : Ideal A), I ∈ (↑(F • F) : Set (Ideal A)) ↔ I ∈ (↑F : Set (Ideal A))
Tactic: ext I
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ (↑(F • F) : Set (Ideal A)) ↔ I ∈ (↑F : Set (Ideal A))
have mp : I ∈ (↑(F • F) : Set (Ideal A)) → I ∈ (↑F : Set (Ideal A))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
mp : I ∈ (↑(F • F) : Set (Ideal A)) → I ∈ (↑F : Set (Ideal A))
⊢ I ∈ (↑(F • F) : Set (Ideal A)) ↔ I ∈ (↑F : Set (Ideal A))
have mp₁ : I ∈ (↑F : Set (Ideal A)) → I ∈ (↑(F • F) : Set (Ideal A))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ (↑(F • F) : Set (Ideal A))
⊢ I ∈ (↑F : Set (Ideal A))
have mp : ∀ (J : Ideal A) (hJ : J ∈ F)
  (htors :
    F.IsTorsionQuot
      ((OrderDual.ofDual : (a : (Ideal A)ᵒᵈ) → Ideal A) ((OrderDual.toDual : (a : Ideal A) → (Ideal A)ᵒᵈ) I)) J),
  I ∈ (↑F : Set (Ideal A))
Tactic: rcases hI with ⟨J, hJ, htors⟩
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I J : Ideal A
hJ : J ∈ F
htors :
  F.IsTorsionQuot
    ((OrderDual.ofDual : (a : (Ideal A)ᵒᵈ) → Ideal A) ((OrderDual.toDual : (a : Ideal A) → (Ideal A)ᵒᵈ) I)) J
⊢ I ∈ (↑F : Set (Ideal A))
have mp : ∀ (x : A) (hx : x ∈ J), Submodule.colon I {x} ∈ F
Tactic: refine hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I J : Ideal A
hJ : J ∈ F
htors :
  F.IsTorsionQuot
    ((OrderDual.ofDual : (a : (Ideal A)ᵒᵈ) → Ideal A) ((OrderDual.toDual : (a : Ideal A) → (Ideal A)ᵒᵈ) I)) J
x : A
hx : x ∈ J
⊢ Submodule.colon I {x} ∈ F
have mp : ∀ (K : Ideal A) (hK : K ∈ F)
  (hincl :
    K ≤
      Submodule.colon (M := A)
        ((OrderDual.ofDual : (a : (Ideal A)ᵒᵈ) → Ideal A) ((OrderDual.toDual : (a : Ideal A) → (Ideal A)ᵒᵈ) I)) {x}),
  Submodule.colon I {x} ∈ F
Tactic: rcases htors x hx with ⟨K, hK, hincl⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Basic (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
⊢ F.IsGabriel
have mpr : ∀ (I : Ideal A) (h : ∃ J ∈ F, ∀ x ∈ J, Submodule.colon I {x} ∈ F), I ∈ F
Tactic: refine { toIsUniform := h₁, gabriel_closed := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
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}
have 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
Tactic: refine ⟨fun _ ↦ ⟨F.ringFilterBasis, rfl⟩, fun ⟨B, hB⟩ ↦ ⟨fun {I} hI a ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
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
⊢ Submodule.colon I {a} ∈ F
have obtain : ∀ (V : Set A) (hbasis : V ∈ B) (hsub : V ⊆ (fun (x : A) ↦ x * a) ⁻¹' (↑I : Set A)), Submodule.colon I {a} ∈ F
Tactic: obtain ⟨V, hbasis, hsub⟩ := B.mul_right a (U := I) (hB.ge (by simpa))
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
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)
⊢ Submodule.colon I {a} ∈ F
have 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
Tactic: obtain ⟨J, hJ, rfl⟩ := hB.le hbasis
Cleared hypotheses: V, hbasis, hsub
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 a ↔ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
have mp : s ∈ 𝓝 a → ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
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
⊢ s ∈ 𝓝 a ↔ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
have mpr : (∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s) → s ∈ 𝓝 a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IdealFilter.Topology (goal)
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
⊢ ∃ I ∈ F, HVAdd.hVAdd (β := Set (WithIdealFilter F)) a (idealSet I) ⊆ s
have 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
Tactic: rcases ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.1 hs with ⟨t, ht, hts⟩