awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsField R ↔ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

Tactic:
⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot.ne' h_top.ne⟩

Premises used: _private.0.Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.match_1, IsField, LT.lt.ne', Iff.intro, Ring.not_isField_of_ne_of_ne, Not, LT.lt.ne
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
refine : ∀ (h : ¬IsField R), ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
⊢ ¬IsField R ↔ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot.ne' h_top.ne⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
obtain : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hIm : I.IsMaximal), ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
⊢ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

Tactic:
obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h

Premises used: Ring.exists_maximal_of_not_isField
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

Tactic:
⟨I, bot_lt_iff_ne_bot.mpr hI, lt_top_iff_ne_top.mpr hIm.ne_top⟩

Premises used: Iff.mpr, bot_lt_iff_ne_bot, lt_top_iff_ne_top, And.intro, Exists.intro, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

Tactic:
exact ⟨I, bot_lt_iff_ne_bot.mpr hI, lt_top_iff_ne_top.mpr hIm.ne_top⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsField R ↔ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime

Tactic:
⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩

Premises used: _private.0.Ring.not_isField_iff_exists_prime.match_1, IsField, Iff.intro, Ideal.IsPrime.ne_top, Ring.not_isField_of_ne_of_ne, Not
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
refine : ∀ (h : ¬IsField R), ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
⊢ ¬IsField R ↔ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
obtain : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hIm : I.IsMaximal), ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime

Tactic:
obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h

Premises used: Ring.exists_maximal_of_not_isField
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime

Tactic:
⟨I, hI, hIm.isPrime⟩

Premises used: Ideal.IsMaximal.isPrime, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime

Tactic:
exact ⟨I, hI, hIm.isPrime⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inl : Subsingleton R → (IsField R ↔ IsSimpleOrder.{u_5} (Ideal R))
inr : Nontrivial R → (IsField R ↔ IsSimpleOrder.{u_5} (Ideal R))
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
        (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩

Premises used: False.elim, false_of_nontrivial_of_subsingleton, Ideal, Iff.intro, not_isField_of_subsingleton
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
exact
      ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
        (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
inr : (∃ (I : Ideal R), ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder.{u_5} (Ideal R)
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]

Premises used: not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
inr : (∀ (I : Ideal R), ¬⊥ < I ∨ ¬I < ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)
⊢ (∃ (I : Ideal R), ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder.{u_5} (Ideal R)

Tactic:
contrapose! +distrib
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
inr : (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)
⊢ (∀ (I : Ideal R), ¬⊥ < I ∨ ¬I < ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
simp_rw [not_lt_top_iff, not_bot_lt_iff]

Premises used: not_lt_top_iff, not_bot_lt_iff
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
⟨fun h => ⟨h⟩, fun h => h.2⟩

Premises used: IsSimpleOrder.mk, Iff.intro, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.2⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
not_field : ¬IsField R
max : Ideal.IsMaximal.{u_5} (α := R) ⊥
obtain : ∀ (I : Ideal R) (hIbot : ⊥ < I) (hItop : I < ⊤), False
⊢ False

Tactic:
obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field

Premises used: Iff.mp, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
not_field : ¬IsField R
max : Ideal.IsMaximal.{u_5} (α := R) ⊥
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False

Tactic:
hIbot.ne (max.eq_of_le hItop.ne bot_le)

Premises used: Ideal.IsMaximal.eq_of_le, bot_le, LT.lt.ne
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
not_field : ¬IsField R
max : Ideal.IsMaximal.{u_5} (α := R) ⊥
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False

Tactic:
exact hIbot.ne (max.eq_of_le hItop.ne bot_le)

Premises used: Ideal.IsMaximal.eq_of_le, bot_le, LT.lt.ne
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
⊢ ⊥ < M

Tactic:
(Ring.ne_bot_of_isMaximal_of_not_isField hm non_field).bot_lt

Premises used: Ring.ne_bot_of_isMaximal_of_not_isField, Ne.bot_lt
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
h :
  ∀ (x_1 : S),
    Membership.mem (γ := Submodule R S) (LinearMap.range (LinearMap.mulLeft R x)) x_1 ↔
      Membership.mem (γ := Submodule R S) (Submodule.restrictScalars R (span {x})) x_1
⊢ Eq (α := Submodule R S) (LinearMap.range (LinearMap.mulLeft R x)) (Submodule.restrictScalars R (span {x}))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
x_1 : S
⊢ Membership.mem (γ := Submodule R S) (LinearMap.range (LinearMap.mulLeft R x)) x_1 ↔
    Membership.mem (γ := Submodule R S) (Submodule.restrictScalars R (span {x})) x_1

Tactic:
simp [mem_span_singleton', mul_comm]

Premises used: Ideal.mem_span_singleton', mul_comm
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ (↑((basisSpanSingleton b hx : (a : ι) → ↥(span {x})) i) : S) = HMul.hMul (β := S) x ((b : (a : ι) → S) i : S)

Tactic:
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
    Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
    LinearEquiv.restrictScalars_apply, LinearMap.mulLeft_apply]

Premises used: LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, LinearEquiv.ofInjective_apply, LinearMap.mulLeft_apply, Module.Basis.map_apply, LinearEquiv.coe_ofEq_apply, Ideal.basisSpanSingleton, Submodule.restrictScalarsEquiv_apply
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
N : Type u_4
inst_4 : Semiring N
inst_5 : Module N S
inst_6 : SMulCommClass R N S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ Eq (α := S)
    ((AddHom.toFun (LinearMap.toAddHom (↑(b.constr N) : (ι → S) →ₗ[N] S →ₗ[R] S))
            (Function.comp (β := ↥(span {x}))
              (Subtype.val (p := fun (x_1 : S) ↦ Membership.mem (γ := Ideal S) (span {x}) x_1))
              (⇑(basisSpanSingleton b hx) : (a : ι) → ↥(span {x}))) :
          (a : S) → S)
        ((b : (a : ι) → S) i : S) :
      S)
    ((((Algebra.lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : ι) → S) i : S) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal S
b : Basis.{u_1, u_2, u_3} ι R ↥I
x : S
⊢ x ∈ I ↔ ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul (β := S) x (↑((b : (a : ι) → ↥I) i) : S)

Tactic:
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff

Premises used: Module.Basis.mem_submodule_iff, LinearEquiv.symm, Set.Mem, LinearEquiv.restrictScalars, Module.Basis.map, Submodule.restrictScalarsEquiv
-- Module: Mathlib.RingTheory.Ideal.Basis
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
I : Ideal S
b : Basis.{u_1, u_2, u_3} ι R ↥I
x : S
⊢ x ∈ I ↔ ∃ (c : ι → R), x = ∑ i : ι, HSMul.hSMul (β := S) (c i) (↑((b : (a : ι) → ↥I) i) : S)

Tactic:
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff'

Premises used: LinearEquiv.symm, Set.Mem, LinearEquiv.restrictScalars, Module.Basis.map, Module.Basis.mem_submodule_iff', Submodule.restrictScalarsEquiv
-- Module: Mathlib.RingTheory.Ideal.BigOperators
Goal:
α : Type u
inst : Semiring α
I : Ideal α
ι : Type u_1
t : Finset ι
f : ι → α
⊢ (∀ c ∈ t, f c ∈ I) → ∑ i ∈ t, f i ∈ I

Tactic:
Submodule.sum_mem I

Premises used: Set.Mem, Submodule.sum_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
a b : R
ha : Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} a
hb : Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} b
⊢ (↑N : Set M) + (↑N : Set M) = (↑N : Set M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
⊢ 0 ⊆ (↑N : Set M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
r : R
simp : ∀ {x : R}, (∀ ⦃b : M⦄, b ∈ S → x • b ∈ (↑N : Set M)) → ∀ ⦃b : M⦄, b ∈ S → r • x • b ∈ (↑N : Set M)
⊢ ∀ {x : R},
    Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} x →
      Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} (r • x)

Tactic:
simp only [Set.mem_setOf_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]

Premises used: Set.mem_setOf_eq, smul_eq_mul, SemigroupAction.mul_smul, Set.smul_set_subset_iff
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
r x : R
hx : ∀ ⦃b : M⦄, b ∈ S → x • b ∈ (↑N : Set M)
y : M
hy : y ∈ S
⊢ r • x • y ∈ (↑N : Set M)

Tactic:
N.smul_mem _ (hx hy)

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
r x : R
hx : ∀ ⦃b : M⦄, b ∈ S → x • b ∈ (↑N : Set M)
y : M
hy : y ∈ S
⊢ r • x • y ∈ (↑N : Set M)

Tactic:
exact N.smul_mem _ (hx hy)

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
⊢ r ∈ N.colon S ↔ ∀ s ∈ S, r • s ∈ N

Tactic:
Set.smul_set_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.smul_set_subset_iff
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : M
r : R
⊢ r ∈ N.colon {x} ↔ r • x ∈ N

Tactic:
simp [mem_colon, forall_eq]

Premises used: forall_eq, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N N₁ N₂ : Submodule R M
S S₁ S₂ : Set M
P : Submodule R M
r s : R
hr : r ∈ N.colon (↑P : Set M)
p : M
hp : p ∈ (r * s) • (↑P : Set M)
obtain : ∀ (p : M) (hp : p ∈ (↑P : Set M)), (fun (x : M) ↦ (r * s) • x) p ∈ (↑N : Set M)
⊢ p ∈ (↑N : Set M)

Tactic:
obtain ⟨p, hp, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N N₁ N₂ : Submodule R M
S S₁ S₂ : Set M
P : Submodule R M
r s : R
hr : r ∈ N.colon (↑P : Set M)
p : M
hp : p ∈ (↑P : Set M)
⊢ (fun (x : M) ↦ (r * s) • x) p ∈ (↑N : Set M)

Tactic:
hr ⟨_, P.smul_mem _ hp, (mul_smul ..).symm⟩

Premises used: And.intro, Exists.intro, Eq.symm, SemigroupAction.mul_smul, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N N₁ N₂ : Submodule R M
S S₁ S₂ : Set M
P : Submodule R M
r s : R
hr : r ∈ N.colon (↑P : Set M)
p : M
hp : p ∈ (↑P : Set M)
⊢ (fun (x : M) ↦ (r * s) • x) p ∈ (↑N : Set M)

Tactic:
exact hr ⟨_, P.smul_mem _ hp, (mul_smul ..).symm⟩

Premises used: And.intro, Exists.intro, Eq.symm, SemigroupAction.mul_smul, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
simp_rw : ∀ (x : R), (∀ (s : R), Membership.mem (γ := Set R) Set.univ s → x * s ∈ I) ↔ x ∈ I
⊢ colon I Set.univ = I

Tactic:
simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]

Premises used: SetLike.ext_iff, Submodule.mem_colon, smul_eq_mul
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ ∀ (x : R), (∀ (s : R), Membership.mem (γ := Set R) Set.univ s → x * s ∈ I) ↔ x ∈ I

Tactic:
fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩

Premises used: trivial, Eq.rec, Ideal.mul_mem_right, Iff.intro, mul_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ ∀ (x : R), (∀ (s : R), Membership.mem (γ := Set R) Set.univ s → x * s ∈ I) ↔ x ∈ I

Tactic:
exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
h : ∀ (x : R), Membership.mem (γ := Ideal R) (colon ⊥ (↑N : Set M)) x ↔ x ∈ N.annihilator
⊢ colon ⊥ (↑N : Set M) = N.annihilator

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : R
⊢ Membership.mem (γ := Ideal R) (colon ⊥ (↑N : Set M)) x ↔ x ∈ N.annihilator

Tactic:
simp [mem_colon, mem_annihilator]

Premises used: Submodule.mem_annihilator, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
S₁ S₂ : Set M
hn : N₁ ≤ N₂
hs : S₁ ⊆ S₂
⊢ N₁.colon S₂ ≤ N₂.colon S₁

Tactic:
fun _ hrns ↦ mem_colon.mpr fun s₁ hs₁ ↦ hn <| mem_colon.mp hrns s₁ <| hs hs₁

Premises used: Iff.mpr, Set.Mem, Iff.mp, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
S : Set R
inst_1 : I.IsTwoSided
⊢ I ≤ colon I S

Tactic:
colon_univ.symm.trans_le (colon_mono le_rfl S.subset_univ)

Premises used: le_rfl, Set.subset_univ, Eq.trans_le, Submodule.colon_univ, Submodule.colon_mono, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι₁ : Sort u_3
f : ι₁ → Submodule R M
ι₂ : Sort u_4
g : ι₂ → Set M
⊢ Eq.{u_1 + 1} (α := Ideal R) (colon.{u_1, u_2} (M := M) (⨅ (i : ι₁), f i) (⋃ (j : ι₂), g j))
    (⨅ (i : ι₁), ⨅ (j : ι₂), (f i).colon (g j))

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
S : Set M
h : S ⊆ (↑N₂ : Set M)
⊢ (N₁ ⊓ N₂).colon S = N₁.colon S

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
⊢ N.colon S = ⊤ ↔ S ⊆ (↑N : Set M)

Tactic:
aesop (add simp [mem_colon, Ideal.eq_top_iff_one])

Premises used: Ideal.eq_top_iff_one, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ : Submodule R M
S : Set M
⊢ (N₁ ⊓ N₂).colon S = N₁.colon S ⊓ N₂.colon S

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
ι : Sort u_3
f : ι → Submodule R M
⊢ Eq.{u_1 + 1} (α := Ideal R) (colon (⨅ (i : ι), f i) S) (⨅ (i : ι), (f i).colon S)

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
ι : Type u_3
s : Finset ι
f : ι → Submodule R M
⊢ (s.inf f).colon S = s.inf fun (i : ι) ↦ (f i).colon S

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
⊢ Eq.{u_1 + 1} (α := Ideal R) (colon ⊤ S) ⊤

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S₁ S₂ : Set M
⊢ N.colon (S₁ ∪ S₂) = N.colon S₁ ⊓ N.colon S₂

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
ι : Sort u_3
f : ι → Set M
⊢ N.colon (⋃ (i : ι), f i) = ⨅ (i : ι), N.colon (f i)

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.colon ∅ = ⊤

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.colon {0} = ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.colon (↑⊥ : Set M) = ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
⊢ r ∈ N.colon S ↔ S ≤ (↑(comap (HSMul.hSMul (β := M →ₗ[R] M) r LinearMap.id) N) : Set M)

Tactic:
mem_colon

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N N' : Submodule R M
r : R
⊢ r ∈ N.colon (↑N' : Set M) ↔ r • N' ≤ N

Tactic:
aesop (add simp SetLike.coe_subset_coe)

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
⊢ Eq (α := Ideal R) (colon ⊥ S) (annihilator (span R S))

Tactic:
aesop (add simp [mem_colon, mem_annihilator_span])

Premises used: Submodule.mem_annihilator_span, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
⊢ N.colon (↑(span R S) : Set M) = N.colon S

Tactic:
(colon_mono le_rfl subset_span).antisymm fun r h ↦ mem_colon.mpr fun s hs ↦ ?_

Premises used: Iff.mpr, le_rfl, LE.le.antisymm, Submodule.colon_mono, Submodule.mem_colon, Submodule.subset_span
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
refine : ∀ (r : R) (h : r ∈ N.colon S) (s : M) (hs : s ∈ (↑(span R S) : Set M)), r • s ∈ N
⊢ N.colon (↑(span R S) : Set M) = N.colon S

Tactic:
refine (colon_mono le_rfl subset_span).antisymm fun r h ↦ mem_colon.mpr fun s hs ↦ ?_

Premises used: Iff.mpr, le_rfl, LE.le.antisymm, Submodule.colon_mono, Submodule.mem_colon, Submodule.subset_span
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s x : M
h_1 : x ∈ S
⊢ r • x ∈ N

Tactic:
aesop (add simp mem_colon)

Premises used: Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
⊢ HSMul.hSMul (β := M) r 0 ∈ N

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s x y : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
hy : Membership.mem (γ := Submodule R M) (span R S) y
h_1 : r • x ∈ N
h_2 : r • y ∈ N
⊢ r • (x + y) ∈ N

Tactic:
aesop
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
h_1 : r • x ∈ N
⊢ r • a • x ∈ N

Tactic:
simp_all [smul_mem, smul_comm r]

Premises used: SMulCommClass.smul_comm, Submodule.smul_mem