mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
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_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
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n

pp: case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
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_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
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p

pp: case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z

pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z

Tactic:
hxy.1

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : 0 ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y)

pp: case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)

Tactic:
·

Goal state after:
case neg.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)

Tactic:
·

Goal state after:
case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

pp: case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
h : m + 1 ≤ n
⊢ I ^ n ≤ I ^ (m + 1)

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

pp: case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥

Tactic:
·

Goal state after:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥

Tactic:
·

Goal state after:
case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0

pp: case mpr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ x = 0 ∨ y = 0 → lcm x y = 0

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
⊢ ∀ (m : M), r • m = 0

pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
⊢ ∀ (m : ι →₀ M), r • m = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : ι →₀ M), r • m = 0
⊢ ∀ (m : M), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
⊢ ∀ (m : ι →₀ M), r • m = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
⊢ ∀ (m : ι →₀ M), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0

pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : Π₀ (i : ι), M i), r • m = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0

pp: case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0

Tactic:
·

Goal state after:
case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0

Tactic:
·

Goal state after:
case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : Π₀ (i : ι), M i), r • m = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : Π₀ (i : ι), M i), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * I ^ 0

pp: case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * I ^ 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
r s : R
inst✝ : (span {r}).IsTwoSided
⊢ span {r} * span {s} = span {r * s}

Tactic:
by
  rw [span_mul_span', Set.singleton_mul_singleton]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
ih : span {s} ^ 0 = span {s ^ 0}
⊢ span {s} ^ (0 + 1) = span {s ^ (0 + 1)}

pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
ih : span {s} ^ n = span {s ^ n}
ne : n ≠ 0
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}

Tactic:
·

Goal state after:
case succ.inl
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
ih : span {s} ^ 0 = span {s ^ 0}
⊢ span {s} ^ (0 + 1) = span {s ^ (0 + 1)}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
·

Goal state after:
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
x y : R
h1 : y ∣ x
h2 : y * 0 ∣ x
⊢ x / (y * 0) = x / y / 0

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ x / (y * z) = x / y / z

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
x y : R
h1 : y ∣ x
h2 : y * 0 ∣ x
⊢ x / (y * 0) = x / y / 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
x z : R
h1 : 0 ∣ x
h2 : z ∣ x / 0
⊢ x / 0 / z = x / (0 * z)

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
hy : y ≠ 0
⊢ x / y / z = x / (y * z)

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : EuclideanDomain R
x z : R
h1 : 0 ∣ x
h2 : z ∣ x / 0
⊢ x / 0 / z = x / (0 * z)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ y * (x / y)
hy : y ≠ 0
⊢ x / y / z = x / (y * z)

Tactic:
EuclideanDomain.mul_div_cancel' hy h1

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hy : y ≠ 0
⊢ x / y / z = x / (y * z)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0

pp: case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
·

Goal state after:
case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
·

Goal state after:
case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
·

Goal state after:
case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0

Tactic:
·

Goal state after:
case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0