mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α : Type u_6} [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: case h.zero
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ 0
⊢ f 0 = ⊥

pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥

Tactic:
·

Goal state after:
case h.zero
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ 0
⊢ f 0 = ⊥
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥

Tactic:
·

Goal state after:
case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))

pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : β) → R i)

pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)

Tactic:
·

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : β) → R i)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)

Tactic:
·

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)

Tactic:
·

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R S
f✝ : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R
inst✝² : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst✝¹ : RingHomSurjective f
I : Ideal R
inst✝ : I.IsTwoSided
b : S
a : R
ha : a ∈ ↑I
⊢ f.toSemilinearMap a * b ∈ Submodule.map f.toSemilinearMap I

Tactic:
obtain ⟨b, rfl⟩ := f.surjective b

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R S
f✝ : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R
inst✝² : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst✝¹ : RingHomSurjective f
I : Ideal R
inst✝ : I.IsTwoSided
a : R
ha : a ∈ ↑I
b : R
⊢ f.toSemilinearMap a * f b ∈ Submodule.map f.toSemilinearMap I
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case inl
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : r * (Pi.evalRingHom R j) x + y = 1
⊢ 1 j = (update 0 j r * x + update 1 j y) j

pp: case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j

Tactic:
·

Goal state after:
case inl
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : r * (Pi.evalRingHom R j) x + y = 1
⊢ 1 j = (update 0 j r * x + update 1 j y) j
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j

Tactic:
·

Goal state after:
case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y

pp: case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Tactic:
·

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I

Tactic:
·

Goal state after:
case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ J < map f K

pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ φ (map f K) = K

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ J < map f K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mpr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)

pp: case mp
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

Tactic:
·

Goal state after:
case mpr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ φ (map f K) = K

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ φ (map f K) = K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ x ∈ ↑I • Set.range f, ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

pp: case mp.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = 0

pp: case mp.refine_3
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    x ∈ span R (↑I • Set.range f) →
      y ∈ span R (↑I • Set.range f) →
        (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
          (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = y) →
            ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x + y

pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ x ∈ ↑I • Set.range f, ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
⊢ (Finsupp.single i y) j ∈ I

pp: case mp.refine_1.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ ((Finsupp.single i y).sum fun i c ↦ c • f i) = (fun x1 x2 ↦ x1 • x2) y (f i)

Tactic:
·

Goal state after:
case mp.refine_1.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
⊢ (Finsupp.single i y) j ∈ I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : i = j
⊢ y ∈ I

pp: case neg
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I

Tactic:
·

Goal state after:
case pos
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : i = j
⊢ y ∈ I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I

Tactic:
·

Goal state after:
case neg
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f r * f s ∈ map f I * map f J

Tactic:
exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = 0

pp: case mp.refine_3
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    x ∈ span R (↑I • Set.range f) →
      y ∈ span R (↑I • Set.range f) →
        (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
          (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = y) →
            ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x + y

pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = 0