awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.re (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.snd (R := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.snd q.re

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.snd (R := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.snd q.imI

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.snd (R := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.snd q.imJ

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.snd (R := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.snd q.imK

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.fst
      (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.fst d).re

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.fst
      (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.fst d).imI

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.fst
      (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.fst d).imJ

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.fst
      (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.fst d).imK

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.snd
      (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.snd d).re

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.snd
      (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.snd d).imI

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.snd
      (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.snd d).imJ

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
d : DualNumber ℍ[R]
⊢ TrivSqZeroExt.snd
      (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1)
        ((AlgEquiv.symm dualNumberEquiv : (a : DualNumber ℍ[R]) → ℍ[DualNumber R]) d)) =
    (TrivSqZeroExt.snd d).imK

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
(eq_of_sub_eq_zero ?_).symm

Premises used: eq_of_sub_eq_zero, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
refine : a - a * b / b = 0
⊢ a * b / b = a

Tactic:
refine (eq_of_sub_eq_zero ?_).symm

Premises used: eq_of_sub_eq_zero, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
by_contra : ∀ (h : ¬a - a * b / b = 0), False
⊢ a - a * b / b = 0

Tactic:
by_contra h
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
⊢ ¬(a - a * b / b) * b ≺ b

Tactic:
have := mul_right_not_lt b h
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬(a - a * b / b) * b ≺ b
⊢ ¬a * b % b ≺ b

Tactic:
rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this

Premises used: Iff.mpr, HMul.hMul, EuclideanDomain.div_add_mod, HDiv.hDiv, sub_mul, mul_comm, Eq.symm, sub_eq_iff_eq_add'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b % b ≺ b
⊢ False

Tactic:
this (mod_lt _ hb)

Premises used: EuclideanDomain.mod_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b % b ≺ b
⊢ False

Tactic:
exact this (mod_lt _ hb)

Premises used: EuclideanDomain.mod_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
a b : R
rw rw₁ : a - b * (a / b) = a - b * (a / b)
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)

Tactic:
rw [div_add_mod]

Premises used: EuclideanDomain.div_add_mod
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0

Tactic:
exact mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a % b = 0
rw : b ∣ b * (a / b)
⊢ b ∣ a

Tactic:
rw [← div_add_mod a b, h, add_zero]

Premises used: EuclideanDomain.div_add_mod, add_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
rw : b * c = b * (b * c / b)
⊢ a % b = 0

Tactic:
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]

Premises used: EuclideanDomain.div_add_mod, add_left_cancel_iff, add_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
haveI : ∀ (this : (p : Prop) → Decidable p), b * c = b * (b * c / b)
⊢ b * c = b * (b * c / b)

Tactic:
haveI := Classical.dec
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
pos : ∀ (b0 : b = 0), b * c = b * (b * c / b)
neg : ∀ (b0 : ¬b = 0), b * c = b * (b * c / b)
⊢ b * c = b * (b * c / b)

Tactic:
by_cases b0 : b = 0
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

Tactic:
simp only [b0, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
neg neg₁ : b * c = b * c
⊢ b * c = b * (b * c / b)

Tactic:
rw [mul_div_cancel_left₀ _ b0]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a : R
⊢ a % a = 0

Tactic:
mod_eq_zero.2 dvd_rfl

Premises used: Iff.mpr, dvd_rfl, EuclideanDomain.mod_eq_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : c ∣ b
rw : c ∣ b * (a / b) + a % b ↔ c ∣ a
rw₁ : R
rw₂ rw₃ : c ∣ a ↔ c ∣ a
⊢ c ∣ a % b ↔ c ∣ a

Tactic:
rw [← dvd_add_right (h.mul_right _), div_add_mod]

Premises used: Dvd.dvd.mul_right, dvd_add_right, EuclideanDomain.div_add_mod
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a : R
⊢ a % 1 = 0

Tactic:
mod_eq_zero.2 (one_dvd _)

Premises used: Iff.mpr, one_dvd, EuclideanDomain.mod_eq_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
b : R
⊢ 0 % b = 0

Tactic:
mod_eq_zero.2 (dvd_zero _)

Premises used: Iff.mpr, dvd_zero, EuclideanDomain.mod_eq_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0

Tactic:
simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0

Premises used: MulZeroClass.zero_mul, mul_div_cancel_right₀, OfNat.ofNat
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [one_mul] using mul_div_cancel_right₀ 1 a0

Premises used: mul_div_cancel_right₀, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
rw : a = a * b / b
rw₁ rw₂ : a = a
⊢ a = c / b

Tactic:
rw [← h, mul_div_cancel_right₀ _ hb]

Premises used: mul_div_cancel_right₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
rw : b = a * b / a
rw₁ rw₂ : b = b
⊢ b = c / a

Tactic:
rw [← h, mul_div_cancel_left₀ _ ha]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
pos : ∀ (hz : z = 0), x * y / z = x * (y / z)
neg : ∀ (hz : ¬z = 0), x * y / z = x * (y / z)
⊢ x * y / z = x * (y / z)

Tactic:
by_cases hz : z = 0
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
pos : ∀ (h : 0 ∣ y), x * y / 0 = x * (y / 0)
⊢ x * y / z = x * (y / z)

Tactic:
subst hz
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y : R
h : 0 ∣ y
pos : 0 = x * (y / 0)
pos₁ : 0 = x * 0
pos₂ pos₃ : Eq.{u + 1} (α := R) 0 0
⊢ x * y / 0 = x * (y / 0)

Tactic:
rw [div_zero, div_zero, mul_zero]

Premises used: EuclideanDomain.div_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
neg : ∀ (p : R), x * (z * p) / z = x * (z * p / z)
⊢ x * y / z = x * (y / z)

Tactic:
rcases h with ⟨p, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
neg : x * (z * p) / z = x * p
neg₁ : z * (x * p) / z = x * p
neg₂ neg₃ : x * p = x * p
⊢ x * (z * p) / z = x * (z * p / z)

Tactic:
rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]

Premises used: mul_div_cancel_left₀, mul_left_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
rw : b * a / b = a
rw₁ rw₂ : a = a
⊢ b * (a / b) = a

Tactic:
rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]

Premises used: mul_div_cancel_left₀, EuclideanDomain.mul_div_assoc
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p : R
⊢ p / 1 = p

Tactic:
(EuclideanDomain.eq_div_of_mul_eq_left (one_ne_zero' R) (mul_one p)).symm

Premises used: one_ne_zero', EuclideanDomain.eq_div_of_mul_eq_left, mul_one, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
pos : ∀ (hq : q = 0), p / q ∣ p
neg : ∀ (hq : ¬q = 0), p / q ∣ p
⊢ p / q ∣ p

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p = 0

Tactic:
rw [hq, zero_dvd_iff] at hpq

Premises used: zero_dvd_iff
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
hpq₁ : p = 0
⊢ q = 0

Tactic:
rw [hq, zero_dvd_iff] at hpq

Premises used: zero_dvd_iff
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
pos : 0 / q ∣ 0
⊢ p / q ∣ p

Tactic:
rw [hpq]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
h : p = p / q * q
⊢ p / q ∣ p

Tactic:
use q
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
h : p = q * (p / q)
h₁ : p = q * p / q
h₂ : p = p * q / q
h₃ h₄ : p = p
⊢ p = p / q * q

Tactic:
rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]

Premises used: EuclideanDomain.mul_div_assoc, mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : a * b ∣ c
inl : ∀ (h : 0 * b ∣ c), b ∣ c / 0
inr : ∀ (ha : a ≠ 0), b ∣ c / a
⊢ b ∣ c / a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

Tactic:
simp only [div_zero, dvd_zero]

Premises used: dvd_zero, EuclideanDomain.div_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
inr : ∀ (d : R), b ∣ a * b * d / a
⊢ b ∣ c / a

Tactic:
rcases h with ⟨d, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a

Tactic:
⟨d, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
inr : a * b * d / a = b * d
⊢ b ∣ a * b * d / a

Tactic:
refine ⟨d, ?_⟩
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
inr : a * (b * d) / a = b * d
inr₁ inr₂ : b * d = b * d
⊢ a * b * d / a = b * d

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ ha]

Premises used: mul_assoc, mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
rw :
  (if a0 : a = 0 then 0
    else
      have x : 0 % a ≺ a := ⋯;
      gcd (0 % a) a) =
    a
⊢ gcd a 0 = a

Tactic:
rw [gcd]

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
pos : ∀ (h : a = 0), 0 = a
neg :
  ∀ (h : ¬a = 0),
    (have x : 0 % a ≺ a := ⋯;
      gcd (0 % a) a) =
      a
⊢ (if a0 : a = 0 then 0
    else
      have x : 0 % a ≺ a := ⋯;
      gcd (0 % a) a) =
    a

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
h : a = 0
⊢ 0 = a

Tactic:
simp only [h, zero_mod, gcd_zero_left]

Premises used: EuclideanDomain.zero_mod, EuclideanDomain.gcd_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
h : ¬a = 0
⊢ (have x : 0 % a ≺ a := ⋯;
    gcd (0 % a) a) =
    a

Tactic:
simp only [h, zero_mod, gcd_zero_left]

Premises used: EuclideanDomain.zero_mod, EuclideanDomain.gcd_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw :
  (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a
⊢ gcd a b = gcd (b % a) a

Tactic:
rw [gcd]

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
pos : ∀ (h : a = 0), b = gcd (b % a) a
neg :
  ∀ (h : ¬a = 0),
    (have x := ⋯;
      gcd (b % a) a) =
      gcd (b % a) a
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : a = 0
⊢ b = gcd (b % a) a

Tactic:
simp only [h, mod_zero, gcd_zero_right]

Premises used: EuclideanDomain.mod_zero, EuclideanDomain.gcd_zero_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : ¬a = 0
⊢ (have x := ⋯;
    gcd (b % a) a) =
    gcd (b % a) a

Tactic:
rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
pos : ∀ (h : a = 0), b = gcd (b % a) a
neg :
  ∀ (h : ¬a = 0),
    (have x := ⋯;
      gcd (b % a) a) =
      gcd (b % a) a
pos₁ : ∀ (h : a = 0), b = gcd (b % a) a
neg₁ :
  ∀ (h : ¬a = 0),
    (have x := ⋯;
      gcd (b % a) a) =
      gcd (b % a) a
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a

Tactic:
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]

Premises used: EuclideanDomain.mod_zero, EuclideanDomain.gcd_zero_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b_1 b : R
rw : b ∣ 0 ∧ b ∣ b
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b

Tactic:
rw [gcd_zero_left]

Premises used: EuclideanDomain.gcd_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b_1 b : R
⊢ b ∣ 0 ∧ b ∣ b

Tactic:
⟨dvd_zero _, dvd_rfl⟩

Premises used: dvd_zero, And.intro, dvd_rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b_1 b : R
⊢ b ∣ 0 ∧ b ∣ b

Tactic:
exact ⟨dvd_zero _, dvd_rfl⟩
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 a b : R
h : a ≠ 0
h_1 : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
rw : gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

Tactic:
rw [gcd_val]

Premises used: EuclideanDomain.gcd_val
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 a b : R
h : a ≠ 0
h_1 : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b

Tactic:
⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩

Premises used: EuclideanDomain.dvd_mod_iff, And.intro, Iff.mp
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 a b : R
h : a ≠ 0
h_1 : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b

Tactic:
exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ gcd a b ∣ a

Tactic:
(gcd_dvd a b).left

Premises used: EuclideanDomain.gcd_dvd, And.left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ gcd a b ∣ b

Tactic:
(gcd_dvd a b).right

Premises used: EuclideanDomain.gcd_dvd, And.right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
simpa [h] using gcd_dvd a b

Premises used: EuclideanDomain.gcd_dvd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
⊢ Eq.{u + 1} (α := R) (gcd 0 0) 0

Tactic:
gcd_zero_right _

Premises used: EuclideanDomain.gcd_zero_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
⊢ Eq.{u + 1} (α := R) (gcd 0 0) 0

Tactic:
exact gcd_zero_right _

Premises used: EuclideanDomain.gcd_zero_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b c x : R
h : c ∣ 0
H : c ∣ x
⊢ c ∣ gcd 0 x

Tactic:
simpa only [gcd_zero_left] using H

Premises used: EuclideanDomain.gcd_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 c a b : R
h : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
rw : c ∣ gcd (b % a) a
⊢ c ∣ gcd a b

Tactic:
rw [gcd_val]

Premises used: EuclideanDomain.gcd_val
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 c a b : R
h : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a

Tactic:
IH ((dvd_mod_iff ca).2 cb) ca

Premises used: Iff.mpr, EuclideanDomain.dvd_mod_iff
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 c a b : R
h : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a

Tactic:
exact IH ((dvd_mod_iff ca).2 cb) ca

Premises used: Iff.mpr, EuclideanDomain.dvd_mod_iff
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : gcd a b = a
rw : gcd a b ∣ b
⊢ a ∣ b

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b

Tactic:
apply gcd_dvd_right

Premises used: EuclideanDomain.gcd_dvd_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : a ∣ b
rw : gcd (b % a) a = a
rw₁ : gcd 0 a = a
rw₂ rw₃ : a = a
⊢ gcd a b = a

Tactic:
rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]

Premises used: Iff.mpr, EuclideanDomain.gcd_zero_left, EuclideanDomain.gcd_val, EuclideanDomain.mod_eq_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ gcd 1 a = 1

Tactic:
gcd_eq_left.2 (one_dvd _)

Premises used: EuclideanDomain.gcd_eq_left, Iff.mpr, one_dvd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ gcd a a = a

Tactic:
gcd_eq_left.2 dvd_rfl

Premises used: EuclideanDomain.gcd_eq_left, Iff.mpr, dvd_rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y x_1 s t s' t' : R
rw : (x_1, s', t').1 = gcd 0 x_1
rw₁ rw₂ : (x_1, s', t').1 = x_1
⊢ (xgcdAux 0 s t x_1 s' t').1 = gcd 0 x_1

Tactic:
rw [xgcd_zero_left, gcd_zero_left]

Premises used: EuclideanDomain.gcd_zero_left, EuclideanDomain.xgcd_zero_left