awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (x - z * y) y ↔ IsCoprime x y
have rw : IsCoprime (x + -(z * y)) y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(z * y)) y ↔ IsCoprime x y
⊢ IsCoprime (x - z * y) y ↔ IsCoprime x y
have rw₁ : IsCoprime (x + -z * y) y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(z * y)) y ↔ IsCoprime x y
rw₁ : IsCoprime (x + -z * y) y ↔ IsCoprime x y
⊢ IsCoprime (x - z * y) y ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (y - x * z) ↔ IsCoprime x y
have rw : IsCoprime x (y + -(x * z)) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(x * z)) ↔ IsCoprime x y
⊢ IsCoprime x (y - x * z) ↔ IsCoprime x y
have rw₁ : IsCoprime x (y + x * -z) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(x * z)) ↔ IsCoprime x y
rw₁ : IsCoprime x (y + x * -z) ↔ IsCoprime x y
⊢ IsCoprime x (y - x * z) ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (y - z * x) ↔ IsCoprime x y
have rw : IsCoprime x (y + -(z * x)) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(z * x)) ↔ IsCoprime x y
⊢ IsCoprime x (y - z * x) ↔ IsCoprime x y
have rw₁ : IsCoprime x (y + -z * x) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(z * x)) ↔ IsCoprime x y
rw₁ : IsCoprime x (y + -z * x) ↔ IsCoprime x y
⊢ IsCoprime x (y - z * x) ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y
have rw : IsCoprime (-x + y * z) y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + y * z) y ↔ IsCoprime x y
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y
have rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + y * z) y ↔ IsCoprime x y
rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y
have rw : IsCoprime (-x + z * y) y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + z * y) y ↔ IsCoprime x y
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y
have rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + z * y) y ↔ IsCoprime x y
rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (x * z - y) ↔ IsCoprime x y
have rw : IsCoprime x (x * z + -y) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (x * z + -y) ↔ IsCoprime x y
⊢ IsCoprime x (x * z - y) ↔ IsCoprime x y
have rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (x * z + -y) ↔ IsCoprime x y
rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
⊢ IsCoprime x (x * z - y) ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (z * x - y) ↔ IsCoprime x y
have rw : IsCoprime x (z * x + -y) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (z * x + -y) ↔ IsCoprime x y
⊢ IsCoprime x (z * x - y) ↔ IsCoprime x y
have rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (z * x + -y) ↔ IsCoprime x y
rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
⊢ IsCoprime x (z * x - y) ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (x + 1) y
have obtain : ∀ (z : R), IsCoprime (y * z + 1) y
Tactic: obtain ⟨z, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
y z : R
⊢ IsCoprime (y * z + 1) y
have rw : IsCoprime 1 y
Tactic: rw [mul_add_left_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (x - 1) y
have rw : IsCoprime (-x + 1) y
Tactic: rw [← neg_sub, neg_left_iff, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : 0 ≤ x
⊢ IsCoprime |x| y ↔ IsCoprime x y
have inl : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : x < 0
⊢ IsCoprime |x| y ↔ IsCoprime x y
have inr : IsCoprime (-x) y ↔ IsCoprime x y
Tactic: rw [abs_of_neg h, IsCoprime.neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : x < 0
inr : IsCoprime (-x) y ↔ IsCoprime x y
⊢ IsCoprime |x| y ↔ IsCoprime x y
have inr₁ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [abs_of_neg h, IsCoprime.neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
⊢ IsCoprime |x| y ↔ IsCoprime x y
have x₁ : 0 ≤ x ∨ x < 0
Tactic: cases le_or_gt 0 x with
  | inl h => rw [abs_of_nonneg h]
  | inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
⊢ IsCoprime x |y| ↔ IsCoprime x y
have rw : IsCoprime |y| x ↔ IsCoprime x y
Tactic: rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
rw : IsCoprime |y| x ↔ IsCoprime x y
⊢ IsCoprime x |y| ↔ IsCoprime x y
have rw₁ : IsCoprime y x ↔ IsCoprime x y
Tactic: rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
rw : IsCoprime |y| x ↔ IsCoprime x y
rw₁ : IsCoprime y x ↔ IsCoprime x y
⊢ IsCoprime x |y| ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
⊢ False
have ha : HPow.hPow (β := ℕ) a 2 = 0
Tactic: obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
⊢ False
have hb : HPow.hPow (β := ℕ) b 2 = 0
Tactic: obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
⊢ False
have h₁ : IsCoprime 0 b
Tactic: obtain rfl := eq_zero_of_pow_eq_zero ha
Cleared hypotheses: a, h, h', ha
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
h₁ : IsCoprime 0 b
⊢ False
have h'₁ : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
Tactic: obtain rfl := eq_zero_of_pow_eq_zero ha
Cleared hypotheses: a, h, h', ha
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
h₁ : IsCoprime 0 b
h'₁ : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
⊢ False
have ha₁ : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
Tactic: obtain rfl := eq_zero_of_pow_eq_zero ha
Cleared hypotheses: a, h, h', ha
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
b : R
hb : HPow.hPow (β := ℕ) b 2 = 0
h : IsCoprime 0 b
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
ha hb₁ : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
⊢ False
have h₁ : IsCoprime.{u_1} (R := R) 0 0
Tactic: obtain rfl := eq_zero_of_pow_eq_zero hb
Cleared hypotheses: b, hb, h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
b : R
hb : HPow.hPow (β := ℕ) b 2 = 0
h : IsCoprime 0 b
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
ha hb₁ : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
h₁ : IsCoprime.{u_1} (R := R) 0 0
⊢ False
have h'₁ : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (α := R) (β := ℕ) 0 2 = 0
Tactic: obtain rfl := eq_zero_of_pow_eq_zero hb
Cleared hypotheses: b, hb, h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
m n : ℕ
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1
have refine_1 : IsCoprime m n → ∀ (a b : ℕ) (H : a * m + b * n = 1), m = 1 ∨ n = 1
Tactic: refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
m n : ℕ
refine_1 : IsCoprime m n → ∀ (a b : ℕ) (H : a * m + b * n = 1), m = 1 ∨ n = 1
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1
have refine_2 : ∀ (h : m = 1 ∨ n = 1), IsCoprime m n
Tactic: refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
m n : ℕ
h : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1
have H₁ : (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)
Tactic: simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n
have refine_2 : IsCoprime 1 n
Tactic: obtain rfl | rfl := h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
m n : ℕ
h : m = 1 ∨ n = 1
refine_2 : IsCoprime 1 n
⊢ IsCoprime m n
have refine_2₁ : IsCoprime m 1
Tactic: obtain rfl | rfl := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : Semifield R
m n : R
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
have inl : IsCoprime m 0 ↔ m ≠ 0 ∨ Ne.{u_1 + 1} (α := R) 0 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : Semifield R
m n : R
inl : IsCoprime m 0 ↔ m ≠ 0 ∨ Ne.{u_1 + 1} (α := R) 0 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
have inr : ∀ (hn : n ≠ 0), IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
have inr : IsCoprime m n
Tactic: suffices IsCoprime m n by simpa [hn]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n
have inr : 0 * m + n⁻¹ * n = 1
Tactic: refine ⟨0, n⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (x - y * z) y ↔ IsRelPrime x y
have rw : IsRelPrime (x + -(y * z)) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(y * z)) y ↔ IsRelPrime x y
⊢ IsRelPrime (x - y * z) y ↔ IsRelPrime x y
have rw₁ : IsRelPrime (x + y * -z) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(y * z)) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (x + y * -z) y ↔ IsRelPrime x y
⊢ IsRelPrime (x - y * z) y ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (x - z * y) y ↔ IsRelPrime x y
have rw : IsRelPrime (x + -(z * y)) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(z * y)) y ↔ IsRelPrime x y
⊢ IsRelPrime (x - z * y) y ↔ IsRelPrime x y
have rw₁ : IsRelPrime (x + -z * y) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(z * y)) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (x + -z * y) y ↔ IsRelPrime x y
⊢ IsRelPrime (x - z * y) y ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (y - x * z) ↔ IsRelPrime x y
have rw : IsRelPrime x (y + -(x * z)) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(x * z)) ↔ IsRelPrime x y
⊢ IsRelPrime x (y - x * z) ↔ IsRelPrime x y
have rw₁ : IsRelPrime x (y + x * -z) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(x * z)) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (y + x * -z) ↔ IsRelPrime x y
⊢ IsRelPrime x (y - x * z) ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (y - z * x) ↔ IsRelPrime x y
have rw : IsRelPrime x (y + -(z * x)) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(z * x)) ↔ IsRelPrime x y
⊢ IsRelPrime x (y - z * x) ↔ IsRelPrime x y
have rw₁ : IsRelPrime x (y + -z * x) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(z * x)) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (y + -z * x) ↔ IsRelPrime x y
⊢ IsRelPrime x (y - z * x) ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y
have rw : IsRelPrime (-x + y * z) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + y * z) y ↔ IsRelPrime x y
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y
have rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + y * z) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y
have rw : IsRelPrime (-x + z * y) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + z * y) y ↔ IsRelPrime x y
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y
have rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + z * y) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (x * z - y) ↔ IsRelPrime x y
have rw : IsRelPrime x (x * z + -y) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (x * z + -y) ↔ IsRelPrime x y
⊢ IsRelPrime x (x * z - y) ↔ IsRelPrime x y
have rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (x * z + -y) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
⊢ IsRelPrime x (x * z - y) ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (z * x - y) ↔ IsRelPrime x y
have rw : IsRelPrime x (z * x + -y) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (z * x + -y) ↔ IsRelPrime x y
⊢ IsRelPrime x (z * x - y) ↔ IsRelPrime x y
have rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (z * x + -y) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
⊢ IsRelPrime x (z * x - y) ↔ IsRelPrime x y
have rw₂ : IsRelPrime x y ↔ IsRelPrime x y
Tactic: rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (x + 1) y
have obtain : ∀ (z : R), IsRelPrime (y * z + 1) y
Tactic: obtain ⟨z, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
y z : R
⊢ IsRelPrime (y * z + 1) y
have rw : IsRelPrime 1 y
Tactic: rw [mul_add_left_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (x - 1) y
have rw : IsRelPrime (-x + 1) y
Tactic: rw [← neg_sub, neg_left_iff, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
⊢ Eq.{u_2 + 1} (α := Ideal R) (⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) ⊤ ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
have haveI : ∀ (this : DecidableEq ι),
  Eq.{u_2 + 1} (α := Ideal R) (⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) ⊤ ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Tactic: haveI : DecidableEq ι := Classical.decEq ι
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
have refine_1 : ∀ (a : ι),
  (∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)),
      Eq.{u_2 + 1} (α := R) (∑ i ∈ {a}, (↑(μ i) : R)) 1) ↔
    (↑{a} : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Tactic: refine h.cons_induction ?_ ?_