awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
⊢ LE.le (α := Ideal α) (span {y}) (span {x}) ∧ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ x ∣ y ∧ y ∣ x
have h₁ : LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
h₁ : LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
⊢ LE.le (α := Ideal α) (span {y}) (span {x}) ∧ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ x ∣ y ∧ y ∣ x
have h₂ : LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
⊢ LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
have h₁ : x ∣ y ↔ x ∣ y
Tactic: rw [span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
⊢ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x
have h₂ : y ∣ x ↔ y ∣ x
Tactic: rw [span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y : α
⊢ Eq (α := Ideal α) (span {x, y}) (span {x}) ↔ x ∣ y
have rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {x}) ↔ x ∣ y
Tactic: rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y : α
rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {x}) ↔ x ∣ y
⊢ Eq (α := Ideal α) (span {x, y}) (span {x}) ↔ x ∣ y
have rw₁ : LE.le (α := Ideal α) (span {y}) (span {x}) ↔ x ∣ y
Tactic: rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ Eq (α := Ideal α) (span {x, y}) (span {x}) ↔ x ∣ y
have rw₂ : x ∣ y ↔ x ∣ y
Tactic: rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y : α
⊢ Eq (α := Ideal α) (span {x, y}) (span {y}) ↔ y ∣ x
have rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {y}) ↔ y ∣ x
Tactic: rw [Ideal.span_insert, sup_eq_right, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y : α
rw : Eq (α := Ideal α) (span {x} ⊔ span {y}) (span {y}) ↔ y ∣ x
⊢ Eq (α := Ideal α) (span {x, y}) (span {y}) ↔ y ∣ x
have rw₁ : LE.le (α := Ideal α) (span {x}) (span {y}) ↔ y ∣ x
Tactic: rw [Ideal.span_insert, sup_eq_right, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ Eq (α := Ideal α) (span {x, y}) (span {y}) ↔ y ∣ x
have rw₂ : y ∣ x ↔ y ∣ x
Tactic: rw [Ideal.span_insert, sup_eq_right, span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ Eq (α := Ideal α) (span {x * a}) (span {x})
have rw : Eq (α := Ideal α) (span {a * x}) (span {x})
Tactic: rw [mul_comm, span_singleton_mul_left_unit h2]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
a : α
h2 : IsUnit a
x : α
rw : Eq (α := Ideal α) (span {a * x}) (span {x})
⊢ Eq (α := Ideal α) (span {x * a}) (span {x})
have rw₁ : Eq (α := Ideal α) (span {x}) (span {x})
Tactic: rw [mul_comm, span_singleton_mul_left_unit h2]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x : α
⊢ Eq (α := Ideal α) (span {x}) ⊤ ↔ IsUnit x
have rw : Eq (α := Ideal α) (span {x}) ⊤ ↔ x ∣ 1
Tactic: rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x : α
rw : Eq (α := Ideal α) (span {x}) ⊤ ↔ x ∣ 1
⊢ Eq (α := Ideal α) (span {x}) ⊤ ↔ IsUnit x
have rw₁ : Eq (α := Ideal α) (span {x}) ⊤ ↔ LE.le (α := Ideal α) (span {1}) (span {x})
Tactic: rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x}) ⊤ ↔ IsUnit x
have rw₂ : Eq (α := Ideal α) (span {x}) ⊤ ↔ LE.le (α := Ideal α) ⊤ (span {x})
Tactic: rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x}) ⊤ ↔ IsUnit x
have rw₃ : LE.le (α := Ideal α) ⊤ (span {x}) ↔ LE.le (α := Ideal α) ⊤ (span {x})
Tactic: rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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₂})
⊢ b₁ * b₂ ∣ b₁ * 1
have rwa : b₁ * b₂ ∣ b₁
Tactic: rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
x y : α
h : Associated x y
⊢ x ∈ I ↔ y ∈ I
have obtain : ∀ (u : αˣ) (h : Associated (y * (↑u : α)) y), y * (↑u : α) ∈ I ↔ y ∈ I
Tactic: obtain ⟨u, rfl⟩ := h.symm
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
⊢ Eq (α := Ideal α) (span {-x}) (span {x})
have h : ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {-x}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x}) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x x_1 : α
⊢ Membership.mem (γ := Ideal α) (span {-x}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x}) x_1
have h : (∃ (a : α), a * -x = x_1) ↔ ∃ (a : α), a * x = x_1
Tactic: simp only [mem_span_singleton']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
⊢ Eq (α := Ideal α) (span (insert (-x) s)) (span (insert x s))
have rw : Eq (α := Ideal α) (span {-x} ⊔ span s) (span (insert x s))
Tactic: rw [span_insert, span_singleton_neg, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
rw : Eq (α := Ideal α) (span {-x} ⊔ span s) (span (insert x s))
⊢ Eq (α := Ideal α) (span (insert (-x) s)) (span (insert x s))
have rw₁ : Eq (α := Ideal α) (span {x} ⊔ span s) (span (insert x s))
Tactic: rw [span_insert, span_singleton_neg, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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))
⊢ Eq (α := Ideal α) (span (insert (-x) s)) (span (insert x s))
have rw₂ : Eq (α := Ideal α) (span {x} ⊔ span s) (span {x} ⊔ span s)
Tactic: rw [span_insert, span_singleton_neg, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x, -y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {-y, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_neg, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {-y, x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, -y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_neg, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x, -y}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_neg, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x + y, y}) (span {x, y})
have h : ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {x + y, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y x_1 : α
⊢ Membership.mem (γ := Ideal α) (span {x + y, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
have h : (∃ (a : α) (b : α), a * (x + y) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1
Tactic: simp_rw [mem_span_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * x + (b + a) * y = x_1
have rw : a * x + (a + b) * y = x_1
Tactic: rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * x + (b + a) * y = x_1
have rw₁ : a * x + (a * y + b * y) = x_1
Tactic: rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * x + (b + a) * y = x_1
have rw₂ : a * x + a * y + b * y = x_1
Tactic: rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * x + (b + a) * y = x_1
have rw₄ : x_1 = x_1
Tactic: rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * (x + y) + (b - a) * y = x_1
have rw : a * x + a * y + (b - a) * y = x_1
Tactic: rw [mul_add, sub_mul, add_add_sub_cancel, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * (x + y) + (b - a) * y = x_1
have rw₁ : a * x + a * y + (b * y - a * y) = x_1
Tactic: rw [mul_add, sub_mul, add_add_sub_cancel, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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
⊢ a * (x + y) + (b - a) * y = x_1
have rw₃ : x_1 = x_1
Tactic: rw [mul_add, sub_mul, add_add_sub_cancel, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
have rw : Eq (α := Ideal α) (span {y + x, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {y + x, x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {y + x, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x + y, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x + y, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {y + x, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x, x + y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x, y + x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, x + y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x - y, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x - y + y, y}) (span {x, y})
Tactic: rw [← span_pair_add_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x - y + y, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x - y, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_add_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x, y - x}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y - x + x}) (span {x, y})
Tactic: rw [← span_pair_add_left, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x, y - x + x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y - x}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_add_left, sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {x, x - y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, x - y - x}) (span {x, y})
Tactic: rw [← span_pair_sub_left, sub_sub_cancel_left, span_pair_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {x, x - y - x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, x - y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, -y}) (span {x, y})
Tactic: rw [← span_pair_sub_left, sub_sub_cancel_left, span_pair_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x, x - y}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_sub_left, sub_sub_cancel_left, span_pair_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
⊢ Eq (α := Ideal α) (span {y - x, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {y - x - y, y}) (span {x, y})
Tactic: rw [← span_pair_sub_right, sub_sub_cancel_left, span_insert_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
rw : Eq (α := Ideal α) (span {y - x - y, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {y - x, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {-x, y}) (span {x, y})
Tactic: rw [← span_pair_sub_right, sub_sub_cancel_left, span_insert_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {y - x, y}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [← span_pair_sub_right, sub_sub_cancel_left, span_insert_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
inst_1 : LinearOrder α
⊢ Eq (α := Ideal α) (span {|x|}) (span {x})
have inl : ∀ (h : |x| = x), Eq (α := Ideal α) (span {|x|}) (span {x})
Tactic: obtain h | h := abs_choice x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
inst_1 : LinearOrder α
inl : ∀ (h : |x| = x), Eq (α := Ideal α) (span {|x|}) (span {x})
⊢ Eq (α := Ideal α) (span {|x|}) (span {x})
have inr : ∀ (h : |x| = -x), Eq (α := Ideal α) (span {|x|}) (span {x})
Tactic: obtain h | h := abs_choice x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
inst_1 : LinearOrder α
⊢ Eq (α := Ideal α) (span (insert |x| s)) (span (insert x s))
have rw : Eq (α := Ideal α) (span {|x|} ⊔ span s) (span (insert x s))
Tactic: rw [span_insert, span_singleton_abs, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x : α
s : Set α
inst_1 : LinearOrder α
rw : Eq (α := Ideal α) (span {|x|} ⊔ span s) (span (insert x s))
⊢ Eq (α := Ideal α) (span (insert |x| s)) (span (insert x s))
have rw₁ : Eq (α := Ideal α) (span {x} ⊔ span s) (span (insert x s))
Tactic: rw [span_insert, span_singleton_abs, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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))
⊢ Eq (α := Ideal α) (span (insert |x| s)) (span (insert x s))
have rw₂ : Eq (α := Ideal α) (span {x} ⊔ span s) (span {x} ⊔ span s)
Tactic: rw [span_insert, span_singleton_abs, span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
inst_1 : LinearOrder α
⊢ Eq (α := Ideal α) (span {x, |y|}) (span {x, y})
have rw : Eq (α := Ideal α) (span {|y|, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_abs, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Ring α
x y : α
inst_1 : LinearOrder α
rw : Eq (α := Ideal α) (span {|y|, x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, |y|}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_abs, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x, |y|}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [span_pair_comm, span_insert_abs, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})
have h : ∀ (x_1 : α), Membership.mem (γ := Ideal α) (span {x + y * z, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z x_1 : α
⊢ Membership.mem (γ := Ideal α) (span {x + y * z, y}) x_1 ↔ Membership.mem (γ := Ideal α) (span {x, y}) x_1
have h : (∃ (a : α) (b : α), a * (x + y * z) + b * y = x_1) ↔ ∃ (a : α) (b : α), a * x + b * y = x_1
Tactic: simp_rw [mem_span_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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 = x_1
have rw : a * x + (b + a * z) * y = a * (x + y * z) + b * y
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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 = x_1
have rw : a * (x + y * z) + (b - a * z) * y = a * x + b * y
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
have rw : Eq (α := Ideal α) (span {y + x * z, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right_mul, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {y + x * z, x}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {y, x}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right_mul, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
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})
⊢ Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
have rw₂ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [span_pair_comm, span_pair_add_right_mul, span_pair_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {y * z + x, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_right_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {y * z + x, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_right_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x, x * z + y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x, y + x * z}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x, x * z + y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [add_comm, span_pair_add_left_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
⊢ Eq (α := Ideal α) (span {x + z * y, y}) (span {x, y})
have rw : Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_add_right_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommRing α
x y z : α
rw : Eq (α := Ideal α) (span {x + y * z, y}) (span {x, y})
⊢ Eq (α := Ideal α) (span {x + z * y, y}) (span {x, y})
have rw₁ : Eq (α := Ideal α) (span {x, y}) (span {x, y})
Tactic: rw [mul_comm, span_pair_add_right_mul]