awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Opposite (goal)
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
have mp : (∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y) →
  ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Opposite (goal)
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
mp :
  (∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y) →
    ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
⊢ (∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
have mpr : (∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y) →
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := sorry, right_inv := sorry } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H_1 : IsCoprime x y
a b : R
H : a * x + b * y = 1
rw : a * x + b * y = 1
⊢ b * y + a * x = 1
have rw₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [add_comm, H]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
h_1 : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ x * (a + b) = 1
have rwa : (a + b) * x = 1
Tactic: rwa [mul_comm, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1
have rwa : b * x + 0 = 1
Tactic: rwa [zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
⊢ x * b = 1
have rwa : ∀ (H : 0 + b * x = 1), x * b = 1
Tactic: rwa [mul_zero, zero_add, mul_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
rwa : ∀ (H : 0 + b * x = 1), x * b = 1
⊢ x * b = 1
have rwa₁ : ∀ (H : b * x = 1), x * b = 1
Tactic: rwa [mul_zero, zero_add, mul_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
rwa : ∀ (H : 0 + b * x = 1), x * b = 1
rwa₁ : ∀ (H : b * x = 1), x * b = 1
⊢ x * b = 1
have rwa₂ : ∀ (H : x * b = 1), x * b = 1
Tactic: rwa [mul_zero, zero_add, mul_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ HMul.hMul (α := R) 1 0 + b * x = 1
have rwa : 0 + b * x = 1
Tactic: rwa [one_mul, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : ℤ
h : IsCoprime a b
⊢ IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)
have rcases : ∀ (u v : ℤ) (H : u * a + v * b = 1), IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)
Tactic: rcases h with ⟨u, v, H⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)
have h : HMul.hMul (α := R) (↑u : R) (↑a : R) + HMul.hMul (α := R) (↑v : R) (↑b : R) = 1
Tactic: use u, v
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ HMul.hMul (α := R) (↑u : R) (↑a : R) + HMul.hMul (α := R) (↑v : R) (↑b : R) = 1
have h : ∀ (H : u * a + v * b = 1), Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw_mod_cast [H]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
inst_1 : Nontrivial R
h : IsCoprime x y
⊢ x ≠ 0 ∨ y ≠ 0
have a : x = 0 → y ≠ 0
Tactic: apply not_or_of_imp
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
⊢ HMul.hMul (α := R) 1 1 + 0 * x = 1
have rw : 1 + 0 * x = 1
Tactic: rw [one_mul, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 1 + 0 * x = 1
⊢ HMul.hMul (α := R) 1 1 + 0 * x = 1
have rw₁ : HAdd.hAdd (α := R) 1 0 = 1
Tactic: rw [one_mul, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 1 + 0 * x = 1
rw₁ : HAdd.hAdd (α := R) 1 0 = 1
⊢ HMul.hMul (α := R) 1 1 + 0 * x = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [one_mul, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
⊢ 0 * x + HMul.hMul (α := R) 1 1 = 1
have rw : 0 * x + 1 = 1
Tactic: rw [one_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 0 * x + 1 = 1
⊢ 0 * x + HMul.hMul (α := R) 1 1 = 1
have rw₁ : HAdd.hAdd (α := R) 0 1 = 1
Tactic: rw [one_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 0 * x + 1 = 1
rw₁ : HAdd.hAdd (α := R) 0 1 = 1
⊢ 0 * x + HMul.hMul (α := R) 1 1 = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [one_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y
have let : ∀ (a b : R) (H : a * x + b * z = 1), x ∣ y
Tactic: let ⟨a, b, H⟩ := H1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y
have rw : x ∣ y * a * x + b * (y * z)
Tactic: rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
⊢ x ∣ z
have let : ∀ (a b : R) (H : a * x + b * y = 1), x ∣ z
Tactic: let ⟨a, b, H⟩ := H1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z
have rw : x ∣ a * z * x + b * (y * z)
Tactic: rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1
have rw : 1 * (c * y + d * z) = 1
Tactic: rw [h1, h2, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
rw : 1 * (c * y + d * z) = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1
have rw₁ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [h1, h2, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
rw : 1 * (c * y + d * z) = 1
rw₁ : HMul.hMul (α := R) 1 1 = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [h1, h2, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)
have rw : ∀ (H1 : IsCoprime y x) (H2 : IsCoprime z x), IsCoprime (y * z) x
Tactic: rw [isCoprime_comm] at H1 H2 ⊢
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x y
H1 : x ∣ z
H2 : y ∣ z
⊢ x * y ∣ z
have obtain : ∀ (a b : R) (h : a * x + b * y = 1), x * y ∣ z
Tactic: obtain ⟨a, b, h⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z
have rw : x * y ∣ z * (a * x) + z * (b * y)
Tactic: rw [← mul_one z, ← h, mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)
have h₁ : x * y ∣ z * (a * x)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
h₁ : x * y ∣ z * (a * x)
⊢ x * y ∣ z * (a * x) + z * (b * y)
have h₂ : x * y ∣ z * (b * y)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)
have h₁ : x * y ∣ a * (x * z)
Tactic: rw [mul_comm z, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)
have h₂ : x * y ∣ z * y * b
Tactic: rw [mul_comm b, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
a b : R
h : a * (x * y) + b * z = 1
⊢ a * y * x + b * z = 1
have rwa : a * x * y + b * z = 1
Tactic: rwa [mul_right_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
⊢ IsCoprime y z
have H₁ : IsCoprime (y * x) z
Tactic: rw [mul_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x y
have rw : ∀ (H : IsCoprime (y * z) x), IsCoprime y x
Tactic: rw [isCoprime_comm] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x z
have H₁ : IsCoprime x (z * y)
Tactic: rw [mul_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
have rw : IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
Tactic: rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
rw : IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
have rw₁ : IsCoprime y x ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
Tactic: rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
rw : IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
rw₁ : IsCoprime y x ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
have rw₂ : IsCoprime x y ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
Tactic: rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
rw : IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
rw₁ : IsCoprime y x ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
rw₂ : IsCoprime x y ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
have rw₃ : IsCoprime x y ∧ IsCoprime x z ↔ IsCoprime x y ∧ IsCoprime x z
Tactic: rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z
have obtain : ∀ (d : R) (h : IsCoprime (x * d) z), IsCoprime x z
Tactic: obtain ⟨d, rfl⟩ := hdvd
Cleared hypotheses: y, h, hdvd
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1
have rw : HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
    (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
  1
Tactic: rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
rw :
  HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
    1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1
have rw₁ : HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) (a * x) : S) ((f : (a : R) → S) (b * y) : S) = 1
Tactic: rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
rw :
  HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
    1
rw₁ : HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) (a * x) : S) ((f : (a : R) → S) (b * y) : S) = 1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1
have rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (a * x + b * y) : S) (1 : S)
Tactic: rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
rw :
  HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
    1
rw₁ : HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) (a * x) : S) ((f : (a : R) → S) (b * y) : S) = 1
rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (a * x + b * y) : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1
have rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
rw :
  HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
    1
rw₁ : HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) (a * x) : S) ((f : (a : R) → S) (b * y) : S) = 1
rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (a * x + b * y) : S) (1 : S)
rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1
have rw₄ : Eq.{v + 1} (α := S) 1 1
Tactic: rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y
have h₁ : IsCoprime (x + y * z) y
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
have rw : ∀ (h : IsCoprime (y + x * z) x), IsCoprime y x
Tactic: rw [isCoprime_comm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
have h₁ : IsCoprime x (y + x * z)
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (y * z + x) y
⊢ IsCoprime x y
have h₁ : IsCoprime (x + y * z) y
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime x y
have h₁ : IsCoprime (x + z * y) y
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (x * z + y)
⊢ IsCoprime x y
have h₁ : IsCoprime x (y + x * z)
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (z * x + y)
⊢ IsCoprime x y
have h₁ : IsCoprime x (y + z * x)
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsRelPrime x (y + x * z)
⊢ IsRelPrime x y
have rw : ∀ (h : IsRelPrime (y + x * z) x), IsRelPrime y x
Tactic: rw [isRelPrime_comm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
h_1 : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1
have rwa : x • (a * y) + b * z = 1
Tactic: rwa [smul_mul_assoc, ← mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
h_1 : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1
have rwa : (x⁻¹ * x) • (a * y) + b * z = 1
Tactic: rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
h_1 : IsCoprime y z
a b : R
h : a * y + b * z = 1
rwa : (x⁻¹ * x) • (a * y) + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1
have rwa₁ : HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 (a * y) + b * z = 1
Tactic: rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
have rw : IsCoprime (x + y * z) y
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
have rw : IsCoprime (y + x * z) x
Tactic: rw [isCoprime_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
have rw : IsCoprime (y + z * x) x
Tactic: rw [isCoprime_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y * z + x) y
have rw : IsCoprime (x + y * z) y
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (z * y + x) y
have rw : IsCoprime (x + z * y) y
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (x * z + y)
have rw : IsCoprime x (y + x * z)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (z * x + y)
have rw : IsCoprime x (y + z * x)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) y
have obtain : ∀ (a b : R) (h : a * x + b * y = 1), IsCoprime (-x) y
Tactic: obtain ⟨a, b, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y
have h₁ : -a * -x + b * y = 1
Tactic: use -a, b
-- 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) y ↔ IsCoprime x y
have rw : IsCoprime (x + -(y * z)) y ↔ IsCoprime 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
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(y * z)) y ↔ IsCoprime x y
⊢ IsCoprime (x - y * z) y ↔ IsCoprime x y
have rw₁ : IsCoprime (x + y * -z) y ↔ IsCoprime 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
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(y * z)) y ↔ IsCoprime x y
rw₁ : IsCoprime (x + y * -z) y ↔ IsCoprime x y
⊢ IsCoprime (x - y * z) y ↔ IsCoprime x y
have rw₂ : IsCoprime x y ↔ IsCoprime x y
Tactic: rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]