awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x - y * z + y * z, y}) (span {x, y})
z₁ : α
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})

Tactic:
rw [← span_pair_add_right_mul, sub_add_cancel]

Premises used: Ideal.span_pair_add_right_mul, sub_add_cancel
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y - x * z + x * z}) (span {x, y})
z₁ : α
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})

Tactic:
rw [← span_pair_add_left_mul, sub_add_cancel]

Premises used: Ideal.span_pair_add_left_mul, sub_add_cancel
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x - y * z, y}) (span {x, y})
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x - z * y, y}) (span {x, y})

Tactic:
rw [mul_comm, span_pair_sub_right_mul]

Premises used: mul_comm, Ideal.span_pair_sub_right_mul
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y - x * z}) (span {x, y})
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y - z * x}) (span {x, y})

Tactic:
rw [mul_comm, span_pair_sub_left_mul]

Premises used: Ideal.span_pair_sub_left_mul, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
rw :
  Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔ ∃ (a : R), a * (1 - e) = x
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔
    Membership.mem (γ := Submodule R R) (Ideal.span {1 - e}) x

Tactic:
rw [Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.Ideal.Span
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
rw₃ rw₄ : x = x
⊢ x * (1 - e) = x

Tactic:
rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]

Premises used: mul_sub, sub_zero, mul_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
refine :
  ∀ (h : ∃ (a : R), a * (1 - e) = x),
    Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x ↔ ∃ (a : R), a * (1 - e) = x

Tactic:
refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : ∃ (a : R), a * (1 - e) = x
obtain : ∀ (x : R), Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) (x * (1 - e))
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) x

Tactic:
obtain ⟨x, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
x : R
change : x * (1 - e) * e = 0
⊢ Membership.mem (γ := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R e)) (x * (1 - e))

Tactic:
change x * (1 - e) * e = 0

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Span
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x * (1 - e) * e = 0

Tactic:
rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

Premises used: sub_self, mul_assoc, MulZeroClass.mul_zero, sub_mul, one_mul
-- Module: Mathlib.RingTheory.Ideal.Span
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})
rw₁ rw₂ : Eq (α := Submodule R R) (Ideal.span {e}) (Ideal.span {e})
⊢ Eq (α := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e))) (Ideal.span {e})

Tactic:
rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]

Premises used: IsIdempotentElem.one_sub, IsIdempotentElem.ker_toSpanSingleton_eq_span, sub_sub_cancel
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
R : Type u_1
inst : Semiring R
x : R
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {x})

Tactic:
⟨x, rfl⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
mpr : F.IsTorsionQuot L K → F.IsTorsionQuot (L ⊓ K) K
⊢ F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K

Tactic:
constructor
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
mp : ∀ (I : Ideal A) (hI : I ∈ F) (hI_le : I ≤ Submodule.colon (L ⊓ K) {k}), ∃ I ∈ F, I ≤ Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}

Tactic:
rcases h k hk with ⟨I, hI, hI_le⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
⊢ 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)
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon L {k}

Tactic:
simpa [hcol] using hI_le
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}

Tactic:
exact ⟨I, hI, (by simpa [hcol] using hI_le)⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
mpr : ∀ (I : Ideal A) (hI : I ∈ F) (hI_le : I ≤ Submodule.colon L {k}), ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
rcases h k hk with ⟨I, hI, hI_le⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
⊢ 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)
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
simpa [hcol] using hI_le
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
exact ⟨I, hI, (by simpa [hcol] using hI_le)⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module A M
⊢ F.IsTorsion M ↔ ∀ (m : M), F.IsTorsionElem m

Tactic:
Iff.rfl

Premises used: Iff.rfl, IdealFilter.IsTorsion
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot L K ↔ ∀ k ∈ (↑K : Set A), ∃ I ∈ F, I ≤ Submodule.colon L {k}

Tactic:
Iff.rfl

Premises used: IdealFilter.IsTorsionQuot, Iff.rfl
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
obtain : ∀ (J : Ideal A) (hJ : J ∈ (↑F : Set (Ideal A))), ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}

Tactic:
obtain ⟨J, hJ⟩ := F.nonempty

Premises used: Order.PFilter.nonempty
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
J : Ideal A
hJ : J ∈ (↑F : Set (Ideal A))
⊢ ⊤ = Submodule.colon I {x}

Tactic:
simpa [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I : Ideal A
x : A
hx : x ∈ I
J : Ideal A
hJ : J ∈ (↑F : Set (Ideal A))
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon I {x}

Tactic:
exact ⟨J, hJ, le_of_le_of_eq le_top (by simpa [eq_comm])⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I J K : Ideal A
hIJ : I ≤ J
hIK : F.IsTorsionQuot I K
⊢ F.IsTorsionQuot J K

Tactic:
fun _ h ↦ (hIK _ h).imp fun _ ↦ And.imp_right (le_trans · (Submodule.colon_mono hIJ .rfl))

Premises used: IdealFilter.IsTorsionQuot, Exists.imp, Set.Subset.rfl, Submodule.colon_mono, And.imp_right, le_trans
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I J K : Ideal A
hJK : J ≤ K
hIK : F.IsTorsionQuot I K
⊢ F.IsTorsionQuot I J

Tactic:
fun x hx ↦ hIK x (hJK hx)

Premises used: IdealFilter.IsTorsionQuot
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
I J K L : Ideal A
hIK : F.IsTorsionQuot I K
hIJ : I ≤ J
hLK : L ≤ K
⊢ F.IsTorsionQuot J L

Tactic:
(hIK.mono_left hIJ).anti_right hLK

Premises used: IdealFilter.IsTorsionQuot.anti_right, IdealFilter.IsTorsionQuot.mono_left
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
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}
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}

Tactic:
obtain ⟨I', hI'F, hI'x⟩ := hI x hx
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
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}
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}

Tactic:
obtain ⟨J', hJ'F, hJ'x⟩ := hJ x hx
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
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:
⟨_, F.inf_mem hI'F hJ'F, (inf_le_inf hI'x hJ'x).trans Submodule.inf_colon.ge⟩

Premises used: Eq.ge, inf_le_inf, Order.PFilter.inf_mem, And.intro, Exists.intro, LE.le.trans, Submodule.inf_colon
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
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:
exact ⟨_, F.inf_mem hI'F hJ'F, (inf_le_inf hI'x hJ'x).trans Submodule.inf_colon.ge⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}

Tactic:
Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le

Premises used: Order.IsPFilter.of_def
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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}
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
⊢ Order.IsPFilter.{u_1} (P := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
refine Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
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}
⊢ Set.Nonempty.{u_1} (α := Ideal A) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
obtain ⟨J, hJ⟩ := G.nonempty

Premises used: Order.PFilter.nonempty
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
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:
⟨J, J, hJ, isTorsionQuot_self F J⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, IdealFilter.isTorsionQuot_self
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
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:
exact ⟨J, J, hJ, isTorsionQuot_self F J⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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

Tactic:
⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩

Premises used: inf_le_right, And.intro, Exists.intro, inf_le_left, Min.min
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
directed : Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} (I ⊓ J)
⊢ ∃ (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

Tactic:
refine ⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
⊢ Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} (I ⊓ J)

Tactic:
⟨K ⊓ L, G.inf_mem hK hL,
      (hIK.anti_right inf_le_left).inf (hJL.anti_right inf_le_right)⟩

Premises used: Set.Mem, setOf, inf_le_right, Order.PFilter.inf_mem, And.intro, Exists.intro, inf_le_left, IdealFilter.IsTorsionQuot.inf, IdealFilter.IsTorsionQuot.anti_right, Min.min
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
⊢ Membership.mem (γ := Set (Ideal A)) {L : Ideal A | ∃ K ∈ G, F.IsTorsionQuot L K} (I ⊓ J)

Tactic:
exact ⟨K ⊓ L, G.inf_mem hK hL,
      (hIK.anti_right inf_le_left).inf (hJL.anti_right inf_le_right)⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
I J : Ideal A
hIJ : I ≤ J
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
⊢ 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

Tactic:
⟨K, hK, hIK⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
I J : Ideal A
hIJ : I ≤ J
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.mono_left hIJ⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, IdealFilter.IsTorsionQuot.mono_left
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F G : IdealFilter A
I J : Ideal A
hIJ : I ≤ J
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:
exact ⟨K, hK, hIK.mono_left hIJ⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
mp : F.IsGabriel → F.IsUniform ∧ F • F = F
mpr : F.IsUniform ∧ F • F = F → F.IsGabriel
⊢ F.IsGabriel ↔ F.IsUniform ∧ F • F = F

Tactic:
constructor
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
⊢ F.IsUniform ∧ F • F = F

Tactic:
⟨hF.toIsUniform, ?_⟩

Premises used: And.intro, IdealFilter.IsGabriel.toIsUniform
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
mp : F • F = F
⊢ F.IsUniform ∧ F • F = F

Tactic:
refine ⟨hF.toIsUniform, ?_⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
mp : ∀ (I : Ideal A), I ∈ (↑(F • F) : Set (Ideal A)) ↔ I ∈ (↑F : Set (Ideal A))
⊢ F • F = F

Tactic:
ext I
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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))
mp₁ : I ∈ (↑F : Set (Ideal A)) → I ∈ (↑(F • F) : Set (Ideal A))
⊢ I ∈ (↑(F • F) : Set (Ideal A)) ↔ I ∈ (↑F : Set (Ideal A))

Tactic:
constructor
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ (↑(F • F) : Set (Ideal A))
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))
⊢ I ∈ (↑F : Set (Ideal A))

Tactic:
rcases hI with ⟨J, hJ, htors⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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))

Tactic:
hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩

Premises used: Set.Mem, And.intro, Exists.intro, IdealFilter.IsGabriel.gabriel_closed
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
mp : ∀ (x : A) (hx : x ∈ J), Submodule.colon I {x} ∈ F
⊢ I ∈ (↑F : Set (Ideal A))

Tactic:
refine hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, IdealFilter.IsGabriel.gabriel_closed
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
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
⊢ Submodule.colon I {x} ∈ F

Tactic:
rcases htors x hx with ⟨K, hK, hincl⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
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:
Order.PFilter.mem_of_le hincl hK

Premises used: Set.Mem, Order.PFilter.mem_of_le
-- Module: Mathlib.RingTheory.IdealFilter.Basic
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
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:
exact Order.PFilter.mem_of_le hincl hK

Premises used: Order.PFilter.mem_of_le
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ (↑F : Set (Ideal A))
⊢ I ∈ (↑(F • F) : Set (Ideal A))

Tactic:
⟨I, hI, isTorsionQuot_self F I⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, IdealFilter.isTorsionQuot_self
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ (↑F : Set (Ideal A))
⊢ I ∈ (↑(F • F) : Set (Ideal A))

Tactic:
exact ⟨I, hI, isTorsionQuot_self F I⟩
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
⊢ F.IsGabriel

Tactic:
{ toIsUniform := h₁, gabriel_closed := ?_ }

Premises used: IdealFilter.IsGabriel.mk
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
mpr : ∀ (I : Ideal A) (h : ∃ J ∈ F, ∀ x ∈ J, Submodule.colon I {x} ∈ F), I ∈ F
⊢ F.IsGabriel

Tactic:
refine { toIsUniform := h₁, gabriel_closed := ?_ }
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
I J : Ideal A
hJ : J ∈ F
hcolon : ∀ x ∈ J, Submodule.colon I {x} ∈ F
x : A
hx : x ∈ J
⊢ Submodule.colon I {x} ≤
    Submodule.colon (M := A)
      ((OrderDual.ofDual : (a : (Ideal A)ᵒᵈ) → Ideal A) ((OrderDual.toDual : (a : Ideal A) → (Ideal A)ᵒᵈ) I)) {x}

Tactic:
simp
-- Module: Mathlib.RingTheory.IdealFilter.Basic
Goal:
A : Type u_1
inst : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
I J : Ideal A
hJ : J ∈ F
hcolon : ∀ x ∈ J, Submodule.colon I {x} ∈ F
⊢ I ∈ F

Tactic:
exact h₂.le ⟨J, hJ, fun x hx ↦ ⟨I.colon {x}, hcolon x hx, by simp⟩⟩

Premises used: Submodule.colon, Eq.le, And.intro, Exists.intro, Singleton.singleton
-- 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:
⟨I ⊓ J, ⟨I ⊓ J, Order.PFilter.inf_mem hI hJ, rfl⟩, fun _ h ↦ h⟩

Premises used: Order.PFilter.inf_mem, SetLike.coe, And.intro, Exists.intro, Min.min, rfl