awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
x : A
h :
  Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    ∃ (u : Rˣ), x = (algebraMap R A : (a : R) → A) (↑u : R)
⊢ Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R)) x

Tactic:
simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm]

Premises used: Submonoid.mem_map, IsUnit, ExistsAndEq.existsAndEq, IsUnit.mem_submonoid_iff, eq_comm, true_and
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
x : A
⊢ Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    ∃ (u : Rˣ), x = (algebraMap R A : (a : R) → A) (↑u : R)

Tactic:
span_singleton_eq_one_iff

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Submodule.span, Submodule.span_singleton_eq_one_iff
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
x : A
⊢ Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
    ∃ (u : Rˣ), x = (algebraMap R A : (a : R) → A) (↑u : R)

Tactic:
exact span_singleton_eq_one_iff

Premises used: Submodule.span_singleton_eq_one_iff
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
h :
  ∀ (x : Aˣ),
    Membership.mem (γ := Subgroup Aˣ)
        (MonoidHom.ker (M := (Submodule R A)ˣ) (Units.map (↑(spanSingleton R) : A →* Submodule R A))) x ↔
      Membership.mem (γ := Subgroup Aˣ) (MonoidHom.range (G := Rˣ) (Units.map (↑(algebraMap R A) : R →* A))) x
⊢ Eq (α := Subgroup Aˣ) (MonoidHom.ker (M := (Submodule R A)ˣ) (Units.map (↑(spanSingleton R) : A →* Submodule R A)))
    (MonoidHom.range (G := Rˣ) (Units.map (↑(algebraMap R A) : R →* A)))

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
x : Aˣ
⊢ Membership.mem (γ := Subgroup Aˣ)
      (MonoidHom.ker (M := (Submodule R A)ˣ) (Units.map (↑(spanSingleton R) : A →* Submodule R A))) x ↔
    Membership.mem (γ := Subgroup Aˣ) (MonoidHom.range (G := Rˣ) (Units.map (↑(algebraMap R A) : R →* A))) x

Tactic:
simpa [Units.ext_iff, eq_comm] using span_singleton_eq_one_iff

Premises used: Units.ext_iff, eq_comm, Submodule.span_singleton_eq_one_iff
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
hm : m ∈ M
hn : n ∈ N
⊢ n * m ∈ M * N

Tactic:
mul_comm m n ▸ mul_mem_mul hm hn

Premises used: Submodule.mul_mem_mul, Set.Mem, Eq.rec, mul_comm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ M * N = N * M

Tactic:
le_antisymm (mul_le.2 fun _r hrm _s hsn => mul_mem_mul_rev hsn hrm)
    (mul_le.2 fun _r hrn _s hsm => mul_mem_mul_rev hsm hrn)

Premises used: Iff.mpr, le_antisymm, Submodule.mul_le, Submodule.mul_mem_mul_rev
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i))

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
refine_1 : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ ∅, span R (M i)) (span R (∏ i ∈ ∅, M i))
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i)) →
        Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s, span R (M i)) (span R (∏ i ∈ insert a s, M i))
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i))

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ ∅, span R (M i)) (span R (∏ i ∈ ∅, M i))

Tactic:
simp [one_eq_span, Set.singleton_one]

Premises used: Set.singleton_one, Submodule.one_eq_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
refine_2 :
  ∀ (s : Finset ι),
    a ∉ s →
      Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i)) →
        Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s, span R (M i)) (span R (∏ i ∈ insert a s, M i))
⊢ ∀ (s : Finset ι),
    a ∉ s →
      Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s, span R (M i)) (span R (∏ i ∈ s, M i)) →
        Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s, span R (M i)) (span R (∏ i ∈ insert a s, M i))

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a : ι
s_1 : Finset ι
H : a ∉ s_1
ih : Eq.{v + 1} (α := Submodule R A) (∏ i ∈ s_1, span R (M i)) (span R (∏ i ∈ s_1, M i))
refine_2 : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (∏ i ∈ insert a s_1, M i)
refine_2₁ : HMul.hMul (α := Submodule R A) (span R (M a)) (∏ x ∈ s_1, span R (M x)) = span R (M a * ∏ x ∈ s_1, M x)
refine_2₂ : HMul.hMul (α := Submodule R A) (span R (M a)) (span R (∏ i ∈ s_1, M i)) = span R (M a * ∏ x ∈ s_1, M x)
refine_2₃ refine_2₄ : Eq (α := Submodule R A) (span R (M a * ∏ i ∈ s_1, M i)) (span R (M a * ∏ x ∈ s_1, M x))
⊢ Eq.{v + 1} (α := Submodule R A) (∏ i ∈ insert a s_1, span R (M i)) (span R (∏ i ∈ insert a s_1, M i))

Tactic:
rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

Premises used: Finset.prod_insert, Submodule.span_mul_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
rw : Eq (α := Submodule R A) (span R (∏ i ∈ s, {x i})) (R ∙ ∏ i ∈ s, x i)
rw₁ rw₂ : Eq (α := Submodule R A) (R ∙ ∏ i ∈ s, x i) (R ∙ ∏ i ∈ s, x i)
⊢ Eq (α := Submodule R A) (∏ i ∈ s, R ∙ x i) (R ∙ ∏ i ∈ s, x i)

Tactic:
rw [prod_span, Set.finsetProd_singleton]

Premises used: Submodule.prod_span, Set.finsetProd_singleton
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s * t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
simp_rw₁ :
  span R
        (HMul.hMul (α := Set A) (β := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
          ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)) *
      P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) *
      (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P)
simp_rw₂ :
  span R
        (HMul.hMul (α := Set A) (β := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
          ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)) *
      P =
    HMul.hMul (α := Submodule R A) (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s))
        (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t)) *
      P
⊢ (s * t) • P = s • t • P

Tactic:
simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]

Premises used: SetSemiring.down_mul, mul_assoc, Submodule.span_mul_span, HSMul.hSMul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 1) * P = P
simp_rw₁ : span R 1 * P = P
simp_rw₂ : 1 * P = P
⊢ HSMul.hSMul (α := SetSemiring A) 1 P = P

Tactic:
simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_mul]

Premises used: SetSemiring.down_one, Submodule.one_eq_span_one_set, HSMul.hSMul, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
simp_rw :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) (s + t)) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₁ :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s ∪ (SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₂ :
  (span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) ⊔
        span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t)) *
      P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
simp_rw₃ :
  span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P ⊔
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P =
    span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P +
      span R ((SetSemiring.down : (a : SetSemiring A) → Set A) t) * P
⊢ (s + t) • P = s • P + t • P

Tactic:
simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]

Premises used: Submodule.span_union, Submodule.sup_mul, SetSemiring.down_add, HSMul.hSMul, Submodule.add_eq_sup
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
simp_rw : span R ((SetSemiring.down : (a : SetSemiring A) → Set A) 0) * P = 0
simp_rw₁ : span R ∅ * P = 0
simp_rw₂ : ⊥ * P = 0
simp_rw₃ : Eq.{v + 1} (α := Submodule R A) ⊥ 0
⊢ HSMul.hSMul (α := SetSemiring A) 0 P = 0

Tactic:
simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]

Premises used: Submodule.bot_mul, HSMul.hSMul, Submodule.span_empty, bot_eq_zero, SetSemiring.down_zero
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
s : SetSemiring A
P : Submodule R A
⊢ s • P = span R ((SetSemiring.down : (a : SetSemiring A) → Set A) s) * P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : SetSemiring A
M N : Submodule R A
h₁ :
  Subset (α := Set A) ((SetSemiring.down : (a : SetSemiring A) → Set A) s : Set A)
    ((SetSemiring.down : (a : SetSemiring A) → Set A) t : Set A)
h₂ : M ≤ N
⊢ s • M ≤ t • N

Tactic:
mul_le_mul' (span_mono h₁) h₂

Premises used: Set.Mem, Submodule.span_mono, mul_le_mul'
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
rw :
  HSMul.hSMul (α := SetSemiring A) (β := Submodule R A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A)
    (span R (↑M : Set A))
| HSMul.hSMul (α := SetSemiring A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A) M

Tactic:
rw [← span_eq M]

Premises used: Submodule.span_eq
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
conv_lhs :
  HSMul.hSMul (α := SetSemiring A) (β := Submodule R A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A)
      (span R (↑M : Set A)) =
    map (LinearMap.mulLeft R a) M
⊢ HSMul.hSMul (α := SetSemiring A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A) M =
    map (LinearMap.mulLeft R a) M

Tactic:
conv_lhs => rw [← span_eq M]

Premises used: Submodule.span_eq
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
rw : span R ((fun (x : A) ↦ a * x) '' (↑M : Set A)) = map (LinearMap.mulLeft R a) M
⊢ HSMul.hSMul (α := SetSemiring A) (β := Submodule R A) ((Set.up : (a : Set A) → SetSemiring A) {a} : SetSemiring A)
      (span R (↑M : Set A)) =
    map (LinearMap.mulLeft R a) M

Tactic:
rw [setSemiring_smul_def, SetSemiring.down_up, span_mul_span, singleton_mul]

Premises used: Submodule.span_mul_span, Submodule.setSemiring_smul_def, SetSemiring.down_up, Set.singleton_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
⊢ span R ((fun (x : A) ↦ a * x) '' (↑M : Set A)) = map (LinearMap.mulLeft R a) M

Tactic:
(map (LinearMap.mulLeft R a) M).span_eq

Premises used: setOf, Submodule.span_eq, LinearMap.mulLeft, Set.image, Submodule.map
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
M : Submodule R A
⊢ span R ((fun (x : A) ↦ a * x) '' (↑M : Set A)) = map (LinearMap.mulLeft R a) M

Tactic:
exact (map (LinearMap.mulLeft R a) M).span_eq

Premises used: Submodule.span_eq, LinearMap.mulLeft, Submodule.map
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a b : A
ha : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} a
hb : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} b
y : A
hy : y ∈ J
rw : a * y + b * y ∈ I
⊢ (a + b) * y ∈ I

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a b : A
ha : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} a
hb : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} b
y : A
hy : y ∈ J
⊢ a * y + b * y ∈ I

Tactic:
Submodule.add_mem _ (ha _ hy) (hb _ hy)

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a b : A
ha : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} a
hb : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} b
y : A
hy : y ∈ J
⊢ a * y + b * y ∈ I

Tactic:
exact Submodule.add_mem _ (ha _ hy) (hb _ hy)

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
h : y ∈ J
rw : 0 ∈ I
⊢ 0 * y ∈ I

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
h : y ∈ J
⊢ 0 ∈ I

Tactic:
apply Submodule.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} x
y : A
hy : y ∈ J
rw : r • (x * y) ∈ I
⊢ r • x * y ∈ I

Tactic:
rw [Algebra.smul_mul_assoc]

Premises used: Algebra.smul_mul_assoc
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} x
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I

Tactic:
Submodule.smul_mem _ _ (hx _ hy)

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : Membership.mem (γ := Set A) {x : A | ∀ y ∈ J, x * y ∈ I} x
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I

Tactic:
exact Submodule.smul_mem _ _ (hx _ hy)

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
I J : Submodule R A
⊢ x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl, setOf
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
h_1 : y ∈ x • (↑J : Set A)
y' : A
hy' : y' ∈ (↑J : Set A)
xy'_eq_y : (fun (x_1 : A) ↦ x • x_1) y' = y
rw : (fun (x_1 : A) ↦ x • x_1) y' ∈ (↑I : Set A)
⊢ y ∈ (↑I : Set A)

Tactic:
rw [← xy'_eq_y]
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
h_1 : y ∈ x • (↑J : Set A)
y' : A
hy' : y' ∈ (↑J : Set A)
xy'_eq_y : (fun (x_1 : A) ↦ x • x_1) y' = y
⊢ (fun (x_1 : A) ↦ x • x_1) y' ∈ (↑I : Set A)

Tactic:
h _ hy'

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
h_1 : y ∈ x • (↑J : Set A)
y' : A
hy' : y' ∈ (↑J : Set A)
xy'_eq_y : (fun (x_1 : A) ↦ x • x_1) y' = y
⊢ (fun (x_1 : A) ↦ x • x_1) y' ∈ (↑I : Set A)

Tactic:
exact h _ hy'
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I J K : Submodule R A
⊢ I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl, setOf
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I J K : Submodule R A
rw : (∀ x ∈ I, ∀ z ∈ K, x * z ∈ J) ↔ I * K ≤ J
rw₁ rw₂ : (∀ x ∈ I, ∀ z ∈ K, x * z ∈ J) ↔ ∀ m ∈ I, ∀ n ∈ K, m * n ∈ J
⊢ I ≤ J / K ↔ I * K ≤ J

Tactic:
rw [le_div_iff, mul_le]

Premises used: Submodule.le_div_iff, Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
rw : 1 * I ≤ 1 ↔ I ≤ 1
rw₁ rw₂ : I ≤ 1 ↔ I ≤ 1
⊢ 1 ≤ 1 / I ↔ I ≤ 1

Tactic:
rw [le_div_iff_mul_le, one_mul]

Premises used: Submodule.le_div_iff_mul_le, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I J : Submodule R A
rw : 1 ≤ I / J ↔ J ≤ I
rw₁ : 1 * J ≤ I ↔ J ≤ I
rw₂ rw₃ : J ≤ I ↔ J ≤ I
⊢ 1 ∈ I / J ↔ J ≤ I

Tactic:
rw [← one_le, le_div_iff_mul_le, one_mul]

Premises used: Submodule.le_div_iff_mul_le, Submodule.one_le, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I ≤ I * (1 / I)

Tactic:
simpa using mul_le_mul_right (one_le_one_div.mpr hI) _

Premises used: Iff.mpr, mul_le_mul_right, Submodule.one_le_one_div
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
rw : ∀ m ∈ I, ∀ n ∈ 1 / I, Membership.mem (γ := Submodule R A) 1 (m * n)
⊢ I * (1 / I) ≤ 1

Tactic:
rw [Submodule.mul_le]

Premises used: Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)

Tactic:
rw [Submodule.mem_div_iff_forall_mul_mem] at hn

Premises used: Submodule.mem_div_iff_forall_mul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)
rw : Membership.mem (γ := Submodule R A) 1 (n * m)
⊢ Membership.mem (γ := Submodule R A) 1 (m * n)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)
⊢ Membership.mem (γ := Submodule R A) 1 (n * m)

Tactic:
hn m hm

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, Membership.mem (γ := Submodule R A) 1 (n * y)
⊢ Membership.mem (γ := Submodule R A) 1 (n * m)

Tactic:
exact hn m hm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
h₁ : ∀ (x : B), x ∈ map h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J
⊢ map h.toLinearMap (I / J) = map h.toLinearMap I / map h.toLinearMap J

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
h₁ :
  (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
⊢ x ∈ map h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J

Tactic:
simp only [mem_map, mem_div_iff_forall_mul_mem, AlgEquiv.toLinearMap_apply]

Premises used: Submodule.mem_map, Submodule.mem_div_iff_forall_mul_mem, AlgEquiv.toLinearMap_apply
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommSemiring B
inst_4 : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
h₁ :
  (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) →
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y
h₂ :
  (∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y) →
    ∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x
⊢ (∃ (y : A), (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ (h : (a : A) → B) y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, (h : (a : A) → B) y_1 = y) → ∃ y_1 ∈ I, (h : (a : A) → B) y_1 = x * y

Tactic:
constructor