awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x y : α
I : Ideal α
mp :
  (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) →
    ∃ (a : α), ∃ b ∈ I, a * y + b = x
mpr :
  (∃ (a : α), ∃ b ∈ I, a * y + b = x) →
    ∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x
⊢ (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) ↔
    ∃ (a : α), ∃ b ∈ I, a * y + b = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
ya : α
hya : Membership.mem (γ := Submodule α α) (span {y}) ya
b : α
hb : b ∈ I
mp :
  ∀ (a : α) (hya : Membership.mem (γ := Submodule α α) (span {y}) (a * y)),
    ∃ (a_1 : α), ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b
⊢ ∃ (a : α), ∃ b_1 ∈ I, a * y + b_1 = ya + b

Tactic:
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya

Premises used: Ideal.mem_span_singleton', Iff.mp, rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : Membership.mem (γ := Submodule α α) (span {y}) (a * y)
⊢ ∃ (a_1 : α), ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b

Tactic:
⟨a, b, hb, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : Membership.mem (γ := Submodule α α) (span {y}) (a * y)
⊢ ∃ (a_1 : α), ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b

Tactic:
exact ⟨a, b, hb, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
a b : α
hb : b ∈ I
⊢ ∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = a * y + b

Tactic:
⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', HMul.hMul, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
a b : α
hb : b ∈ I
⊢ ∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = a * y + b

Tactic:
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
I : Ideal α
h : I ≠ ⊤
⊢ Ne.{u + 1} (α := α) 0 1

Tactic:
fun hz =>
  I.ne_top_iff_one.1 h <| hz ▸ I.zero_mem

Premises used: Ideal.ne_top_iff_one, Eq.rec, Ideal.zero_mem, Iff.mp, Not
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x y : α
⊢ Eq (α := Ideal α) (span {x, y}) (span {y, x})

Tactic:
simp only [span_insert, sup_comm]

Premises used: sup_comm, Ideal.span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x y z : α
⊢ Membership.mem (γ := Ideal α) (span {x, y}) z ↔ ∃ (a : α) (b : α), a * x + b * y = z

Tactic:
Submodule.mem_span_pair

Premises used: Set.Mem, Submodule.mem_span_pair
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x : α
rw : Eq (α := Ideal α) (span {0, x}) (span {x})
rw₁ rw₂ : Eq (α := Ideal α) (span {x}) (span {x})
⊢ Eq (α := Ideal α) (span {x, 0}) (span {x})

Tactic:
rw [span_pair_comm, span_insert_zero]

Premises used: Ideal.span_pair_comm, Ideal.span_insert_zero
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
rw : Eq (α := Ideal α) (span (range x)) (span (⋃ (i : ι), {x i}))
rw₁ rw₂ : Eq (α := Ideal α) (span (range x)) (span (range x))
⊢ Eq (α := Ideal α) (span (range x)) (⨆ (i : ι), span {x i})

Tactic:
rw [← span_iUnion, iUnion_singleton_eq_range]

Premises used: Set.iUnion_singleton_eq_range, Ideal.span_iUnion
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
rw : Eq (α := Ideal α) (span (range x \ {0})) (span (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)))
⊢ Eq (α := Ideal α) (span (range x)) (span (range fun (i : (↑(Function.support x) : Type u_1)) ↦ x (↑i : ι)))

Tactic:
rw [← span_sdiff_singleton_zero (s := range x), Function.support]

Premises used: Ideal.span_sdiff_singleton_zero, Function.support
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
e_s : range x \ {0} = range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)
⊢ Eq (α := Ideal α) (span (range x \ {0})) (span (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)))

Tactic:
congr
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
e_s :
  ∀ (a : α),
    a ∈ range x \ {0} ↔ Membership.mem (γ := Set α) (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)) a
⊢ range x \ {0} = range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)

Tactic:
ext1 a
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
a : α
e_s : (∃ (y : ι), x y = a) ∧ ¬a = 0 ↔ ∃ (y : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)), x (↑y : ι) = a
⊢ a ∈ range x \ {0} ↔ Membership.mem (γ := Set α) (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)) a

Tactic:
simp only [mem_diff, mem_range, mem_singleton_iff]

Premises used: Set.mem_range, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
a : α
h : ∃ (y : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)), x (↑y : ι) = a
j : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)
hj : x (↑j : ι) = a
⊢ ¬a = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
a : α
⊢ (∃ (y : ι), x y = a) ∧ ¬a = 0 ↔ ∃ (y : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)), x (↑y : ι) = a

Tactic:
exact ⟨fun ⟨⟨i, hi⟩, ha⟩ ↦ ⟨⟨i, mem_setOf.mpr (hi ▸ ha)⟩, hi⟩,
    fun ⟨j, hj⟩ ↦ ⟨⟨j.val, hj⟩, by grind⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
x y x_1 : α
rw : x = x_1 * y ↔ x = y * x_1
rw₁ rw₂ : x = y * x_1 ↔ x = y * x_1
⊢ x_1 * y = x ↔ x = y * x_1

Tactic:
rw [eq_comm, mul_comm]

Premises used: eq_comm, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
x y : α
⊢ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x

Tactic:
span_le.trans <| singleton_subset_iff.trans mem_span_singleton

Premises used: Ideal.span_le, Set.singleton_subset_iff, Iff.trans, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
rw : LE.le (α := Ideal α) (span {y}) (span {x}) ∧ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ x ∣ y ∧ y ∣ x
⊢ Eq (α := Ideal α) (span {x}) (span {y}) ↔ Associated x y

Tactic:
rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]

Premises used: and_comm, dvd_dvd_iff_associated, le_antisymm_iff
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
h₁ : LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
h₂ : LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x
⊢ LE.le (α := Ideal α) (span {y}) (span {x}) ∧ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ x ∣ y ∧ y ∣ x

Tactic:
apply and_congr

Premises used: and_congr
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
h₁ h₂ : x ∣ y ↔ x ∣ y
⊢ LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y

Tactic:
rw [span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
h₂ h₃ : y ∣ x ↔ y ∣ x
⊢ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x

Tactic:
rw [span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
x y : α
rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {x}) ↔ x ∣ y
rw₁ : LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
rw₂ rw₃ : x ∣ y ↔ x ∣ y
⊢ Eq (α := Ideal α) (span {x, y}) (span {x}) ↔ x ∣ y

Tactic:
rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton, sup_eq_left, Ideal.span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
x y : α
rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {y}) ↔ y ∣ x
rw₁ : LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x
rw₂ rw₃ : y ∣ x ↔ y ∣ x
⊢ Eq (α := Ideal α) (span {x, y}) (span {y}) ↔ y ∣ x

Tactic:
rw [Ideal.span_insert, sup_eq_right, span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton, sup_eq_right, Ideal.span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
a : α
h2 : IsUnit a
x : α
rw : Eq (α := Ideal α) (span {a * x}) (span {x})
rw₁ rw₂ : Eq (α := Ideal α) (span {x}) (span {x})
⊢ Eq (α := Ideal α) (span {x * a}) (span {x})

Tactic:
rw [mul_comm, span_singleton_mul_left_unit h2]

Premises used: Ideal.span_singleton_mul_left_unit, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
x : α
rw : Eq (α := Ideal α) (span {x}) ⊤ ↔ x ∣ 1
rw₁ : Eq (α := Ideal α) (span {x}) ⊤ ↔ LE.le (α := Ideal α) (span {1}) (span {x})
rw₂ : Eq (α := Ideal α) (span {x}) ⊤ ↔ LE.le (α := Ideal α) ⊤ (span {x})
rw₃ rw₄ : LE.le (α := Ideal α) ⊤ (span {x}) ↔ LE.le (α := Ideal α) ⊤ (span {x})
⊢ Eq (α := Ideal α) (span {x}) ⊤ ↔ IsUnit x

Tactic:
rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]

Premises used: eq_top_iff, Ideal.span_singleton_one, Ideal.span_singleton_le_span_singleton, isUnit_iff_dvd_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
b₁ b₂ : α
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : LE.le (α := Ideal α) (span {b₁}) (span {b₁ * b₂})
rwa : b₁ * b₂ ∣ b₁
rwa₁ rwa₂ rwa₃ rwa₄ : LE.le (α := Ideal α) (span {b₁}) (span {b₁ * b₂})
⊢ b₁ * b₂ ∣ b₁ * 1

Tactic:
rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton, mul_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
x y : α
h : Associated x y
obtain : ∀ (u : αˣ) (h : Associated (y * (↑u : α)) y), y * (↑u : α) ∈ I ↔ y ∈ I
⊢ x ∈ I ↔ y ∈ I

Tactic:
obtain ⟨u, rfl⟩ := h.symm

Premises used: Associated.symm, rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
y : α
u : αˣ
h : Associated (y * (↑u : α)) y
⊢ y * (↑u : α) ∈ I ↔ y ∈ I

Tactic:
I.mul_unit_mem_iff_mem u.isUnit

Premises used: Set.Mem, Ideal.mul_unit_mem_iff_mem, Units.isUnit
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
y : α
u : αˣ
h : Associated (y * (↑u : α)) y
⊢ y * (↑u : α) ∈ I ↔ y ∈ I

Tactic:
exact I.mul_unit_mem_iff_mem u.isUnit

Premises used: Ideal.mul_unit_mem_iff_mem, Units.isUnit
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
s : Set α
⊢ Membership.mem (γ := Ideal α) (span (insert y s)) x ↔ ∃ (a : α), Membership.mem (γ := Ideal α) (span s) (x + a * y)

Tactic:
Submodule.mem_span_insert'

Premises used: Set.Mem, setOf, Submodule.mem_span_insert'
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
h : ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {-x}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x}) x_1
⊢ Eq (α := Ideal α) (span {-x}) (span {x})

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x x_1 : α
h : (∃ (a : α), a * -x = x_1) ↔ ∃ (a : α), a * x = x_1
⊢ Membership.mem (γ := Ideal α) (span {-x}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x}) x_1

Tactic:
simp only [mem_span_singleton']

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x x_1 : α
⊢ (∃ (a : α), a * -x = x_1) ↔ ∃ (a : α), a * x = x_1

Tactic:
⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩

Premises used: HMul.hMul, _private.0.Ideal.span_singleton_neg.match_2, Exists, Eq.rec, _private.0.Ideal.span_singleton_neg.match_1, Iff.intro, neg_mul_neg, Exists.intro, neg_mul_comm, Eq, Neg.neg
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x x_1 : α
⊢ (∃ (a : α), a * -x = x_1) ↔ ∃ (a : α), a * x = x_1

Tactic:
exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
rw : Eq (α := Ideal α) (span {-x} ⊔ span s) (span (insert x s))
rw₁ : Eq (α := Ideal α) (span {x} ⊔ span s) (span (insert x s))
rw₂ rw₃ : Eq (α := Ideal α) (span {x} ⊔ span s) (span {x} ⊔ span s)
⊢ Eq (α := Ideal α) (span (insert (-x) s)) (span (insert x s))

Tactic:
rw [span_insert, span_singleton_neg, span_insert]

Premises used: Ideal.span_insert, Ideal.span_singleton_neg
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {-y, x}) (span {x, y})
rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
rw₂ rw₃ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, -y}) (span {x, y})

Tactic:
rw [span_pair_comm, span_insert_neg, span_pair_comm]

Premises used: Ideal.span_pair_comm, Ideal.span_insert_neg
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
h : ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {x + y, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
⊢ Eq (α := Ideal α) (span {x + y, y}) (span {x, y})

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y x_1 : α
h : (∃ (a : α) (b : α), a * (x + y) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1
⊢ Membership.mem (γ := Ideal α) (span {x + y, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1

Tactic:
simp_rw [mem_span_pair]

Premises used: Ideal.mem_span_pair
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y x_1 : α
h_1 : ∃ (a : α) (b : α), a * (x + y) + b * y = x_1
a b : α
h : a * (x + y) + b * y = x_1
rw : a * x + (a + b) * y = x_1
rw₁ : a * x + (a * y + b * y) = x_1
rw₂ : a * x + a * y + b * y = x_1
rw₃ : a * (x + y) + b * y = x_1
rw₄ rw₅ : x_1 = x_1
⊢ a * x + (b + a) * y = x_1

Tactic:
rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]

Premises used: add_mul, add_assoc, add_comm, mul_add
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y x_1 : α
h_1 : ∃ (a : α) (b : α), a * x + b * y = x_1
a b : α
h : a * x + b * y = x_1
rw : a * x + a * y + (b - a) * y = x_1
rw₁ : a * x + a * y + (b * y - a * y) = x_1
rw₂ : a * x + b * y = x_1
rw₃ rw₄ : x_1 = x_1
⊢ a * (x + y) + (b - a) * y = x_1

Tactic:
rw [mul_add, sub_mul, add_add_sub_cancel, h]

Premises used: add_add_sub_cancel, sub_mul, mul_add
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y x_1 : α
⊢ (∃ (a : α) (b : α), a * (x + y) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1

Tactic:
exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a, by rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a, by rw [mul_add, sub_mul, add_add_sub_cancel, h]⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {y + x, x}) (span {x, y})
rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
rw₂ rw₃ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y + x}) (span {x, y})

Tactic:
rw [span_pair_comm, span_pair_add_right, span_pair_comm]

Premises used: Ideal.span_pair_comm, Ideal.span_pair_add_right
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x + y, y}) (span {x, y})
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {y + x, y}) (span {x, y})

Tactic:
rw [add_comm, span_pair_add_right]

Premises used: add_comm, Ideal.span_pair_add_right
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, x + y}) (span {x, y})

Tactic:
rw [add_comm, span_pair_add_left]

Premises used: Ideal.span_pair_add_left, add_comm
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x - y + y, y}) (span {x, y})
rw₁ rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x - y, y}) (span {x, y})

Tactic:
rw [← span_pair_add_right, sub_add_cancel]

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

Tactic:
rw [← span_pair_add_left, sub_add_cancel]

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

Tactic:
rw [← span_pair_sub_left, sub_sub_cancel_left, span_pair_neg]

Premises used: sub_sub_cancel_left, Ideal.span_pair_sub_left, Ideal.span_pair_neg
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {y - x - y, y}) (span {x, y})
rw₁ : Eq (α := Ideal α) (span {-x, y}) (span {x, y})
rw₂ rw₃ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {y - x, y}) (span {x, y})

Tactic:
rw [← span_pair_sub_right, sub_sub_cancel_left, span_insert_neg]

Premises used: sub_sub_cancel_left, Ideal.span_insert_neg, Ideal.span_pair_sub_right
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
inst_1 : LinearOrder α
inl : ∀ (h : |x| = x), Eq (α := Ideal α) (span {|x|}) (span {x})
inr : ∀ (h : |x| = -x), Eq (α := Ideal α) (span {|x|}) (span {x})
⊢ Eq (α := Ideal α) (span {|x|}) (span {x})

Tactic:
obtain h | h := abs_choice x

Premises used: abs_choice
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
inst_1 : LinearOrder α
h : |x| = x
⊢ Eq (α := Ideal α) (span {|x|}) (span {x})

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
inst_1 : LinearOrder α
h : |x| = -x
⊢ Eq (α := Ideal α) (span {|x|}) (span {x})

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
inst_1 : LinearOrder α
rw : Eq (α := Ideal α) (span {|x|} ⊔ span s) (span (insert x s))
rw₁ : Eq (α := Ideal α) (span {x} ⊔ span s) (span (insert x s))
rw₂ rw₃ : Eq (α := Ideal α) (span {x} ⊔ span s) (span {x} ⊔ span s)
⊢ Eq (α := Ideal α) (span (insert |x| s)) (span (insert x s))

Tactic:
rw [span_insert, span_singleton_abs, span_insert]

Premises used: Ideal.span_singleton_abs, Ideal.span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Ring α
x y : α
inst_1 : LinearOrder α
rw : Eq (α := Ideal α) (span {|y|, x}) (span {x, y})
rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
rw₂ rw₃ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, |y|}) (span {x, y})

Tactic:
rw [span_pair_comm, span_insert_abs, span_pair_comm]

Premises used: Ideal.span_pair_comm, Ideal.span_insert_abs
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
h :
  ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {x + y * z, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
⊢ Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
h : (∃ (a : α) (b : α), a * (x + y * z) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1
⊢ Membership.mem (γ := Ideal α) (span {x + y * z, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1

Tactic:
simp_rw [mem_span_pair]

Premises used: Ideal.mem_span_pair
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
h_1 : ∃ (a : α) (b : α), a * (x + y * z) + b * y = x_1
a b : α
h : a * (x + y * z) + b * y = x_1
rw : a * x + (b + a * z) * y = a * (x + y * z) + b * y
⊢ a * x + (b + a * z) * y = x_1

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
h_1 : ∃ (a : α) (b : α), a * (x + y * z) + b * y = x_1
a b : α
h : a * (x + y * z) + b * y = x_1
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y

Tactic:
ring1
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
h_1 : ∃ (a : α) (b : α), a * x + b * y = x_1
a b : α
h : a * x + b * y = x_1
rw : a * (x + y * z) + (b - a * z) * y = a * x + b * y
⊢ a * (x + y * z) + (b - a * z) * y = x_1

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
h_1 : ∃ (a : α) (b : α), a * x + b * y = x_1
a b : α
h : a * x + b * y = x_1
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y

Tactic:
ring1
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
⊢ (∃ (a : α) (b : α), a * (x + y * z) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1

Tactic:
exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a * z, by rw [← h]; ring1⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a * z, by rw [← h]; ring1⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {y + x * z, x}) (span {x, y})
rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
rw₂ rw₃ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})

Tactic:
rw [span_pair_comm, span_pair_add_right_mul, span_pair_comm]

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

Tactic:
rw [add_comm, span_pair_add_right_mul]

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

Tactic:
rw [add_comm, span_pair_add_left_mul]

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

Tactic:
rw [mul_comm, span_pair_add_right_mul]

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

Tactic:
rw [mul_comm, span_pair_add_left_mul]

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

Tactic:
rw [mul_comm, span_pair_right_mul_add]

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

Tactic:
rw [mul_comm, span_pair_left_mul_add]

Premises used: mul_comm, Ideal.span_pair_left_mul_add