awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
⊢ (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
DivisionSemiring.nnratCast_def _

Premises used: DivisionSemiring.nnratCast_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
a : K
⊢ q • a = (↑q : K) * a

Tactic:
DivisionSemiring.nnqsmul_def q a

Premises used: DivisionSemiring.nnqsmul_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
rw : HMul.hMul (α := K) (↑q : K) 1 = (↑q : K)
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) (↑q : K) (↑q : K)
⊢ HSMul.hSMul (β := K) q 1 = (↑q : K)

Tactic:
rw [NNRat.smul_def, mul_one]

Premises used: mul_one, NNRat.smul_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
⊢ (↑q : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
DivisionRing.ratCast_def _

Premises used: DivisionRing.ratCast_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionRing K
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : a.natAbs.Coprime b
⊢ (↑{ num := a, den := b, den_nz := h1, reduced := h2 } : K) = HDiv.hDiv (α := K) (↑a : K) (↑b : K)

Tactic:
cast_def _

Premises used: Rat.cast_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
K : Type u_1
inst : DivisionRing K
a : ℚ
x : K
⊢ a • x = (↑a : K) * x

Tactic:
DivisionRing.qsmul_def a x

Premises used: DivisionRing.qsmul_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
A : Type u_2
inst : DivisionRing A
m : ℚ
rw : HMul.hMul (α := A) (↑m : A) 1 = (↑m : A)
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) (↑m : A) (↑m : A)
⊢ HSMul.hSMul (β := A) m 1 = (↑m : A)

Tactic:
rw [Rat.smul_def, mul_one]

Premises used: mul_one, Rat.smul_def
-- Module: Mathlib.Algebra.Field.Defs
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Equiv
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : Semiring A
inst_1 : Semiring B
inst_2 : FunLike F A B
inst_3 : MonoidWithZeroHomClass F A B
f : F
inst_4 : IsLocalHom.{u_1, u_2, u_3} (R := A) (S := B) f
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hB : IsField B
x y : A
rw : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) = (f : (a : A) → B) (y * x)
rw₁ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
rw₂ rw₃ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (x * y) : B) ((f : (a : A) → B) (y * x) : B)

Tactic:
rw [map_mul, map_mul, hB.mul_comm]

Premises used: IsField.mul_comm, map_mul
-- Module: Mathlib.Algebra.Field.Equiv
Goal:
A : Type u_1
B : Type u_2
inst : Semiring A
inst_1 : Semiring B
hB : IsField B
e : A ≃* B
⊢ IsField A

Tactic:
IsLocalHom.isField e.injective hB

Premises used: IsLocalHom.isField, MulEquiv.injective
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0

Tactic:
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
rw : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]

Premises used: Commute.geom_sum₂_mul, mul_div_cancel_right₀
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0

Tactic:
have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
rw : ∑ i ∈ range n, x ^ i = (∑ i ∈ range n, x ^ i) * (x - 1) / (x - 1)
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) (∑ i ∈ range n, x ^ i) (∑ i ∈ range n, x ^ i)
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]

Premises used: geom_sum_mul, mul_div_cancel_right₀
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0

Tactic:
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
rw : ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i))
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

Premises used: mul_div_cancel_right₀, Commute.geom_sum₂_Ico_mul
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

Tactic:
simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right, Finset.sum_Ico_eq_sub, geom_sum_eq, div_sub_div_same
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

Tactic:
simpa [geom_sum_Ico hx hmn] using neg_div_neg_eq (x ^ m - x ^ n) (1 - x)

Premises used: HSub.hSub, neg_div_neg_eq, HPow.hPow, OfNat.ofNat, geom_sum_Ico
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
rwa : 1 / x ≠ 1
rwa₁ : ¬1 / x = 1
rwa₂ : ¬1 * x = 1
rwa₃ rwa₄ rwa₅ rwa₆ : ¬x = 1
⊢ x⁻¹ ≠ 1

Tactic:
rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]

Premises used: div_eq_iff_mul_eq, Ne, inv_eq_one_div, one_mul
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ x⁻¹ ≠ 1

Tactic:
have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
⊢ x⁻¹ - 1 ≠ 0

Tactic:
have h₂ : x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
⊢ x - 1 ≠ 0

Tactic:
have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ x * (x ^ Nat.zero)⁻¹ = (x ^ Nat.zero)⁻¹ * x

Tactic:
simp
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n_1 : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x
rw₁ : x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₂ : x * (x ^ n)⁻¹ * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₃ : (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x
rw₄ : (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
rw₅ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x
rw₆ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * (x⁻¹ * x)
rw₇ rw₈ : (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * 1
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x

Tactic:
rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]

Premises used: mul_inv_cancel₀, mul_assoc, mul_inv_rev, inv_mul_cancel₀, pow_succ'
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x

Tactic:
have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
    Nat.recOn n (by simp) fun n h => by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc,
    mul_inv_cancel₀ h₃]

Premises used: mul_inv_cancel₀, mul_assoc, div_eq_iff_mul_eq, geom_sum_eq, mul_right_inj'
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
simp : (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
⊢ 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)

Tactic:
simp only [inv_pow, sub_eq_add_neg, mul_add, one_mul, mul_neg, add_mul, mul_inv_cancel₀ hx0,
    neg_mul, mul_assoc, mul_one, add_comm, neg_add_rev, neg_neg, h₄, add_left_comm]

Premises used: neg_add_rev, add_mul, mul_inv_cancel₀, add_left_comm, mul_assoc, sub_eq_add_neg, neg_neg, inv_pow, add_comm, mul_add, neg_mul, mul_one, one_mul, mul_neg
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
rw : -x + (x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
rw₁ : -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
rw₂ rw₃ : -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1)) = -x + ((x ^ n)⁻¹ * x + (-(x ^ n)⁻¹ + 1))
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)

Tactic:
rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]

Premises used: add_assoc, add_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : Field K
x y : K
h : x ≠ y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
(Commute.all x y).geom_sum₂ h n

Premises used: Commute.geom_sum₂, Commute.all
-- Module: Mathlib.Algebra.Field.GeomSum
Goal:
K : Type u_2
inst : Field K
x y : K
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
(Commute.all x y).geom_sum₂_Ico hxy hmn

Premises used: Commute.geom_sum₂_Ico, Commute.all
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Field R
⊢ IsField R

Tactic:
Semifield.toIsField _

Premises used: Semifield.toIsField
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
⊢ Nontrivial R

Tactic:
⟨h.exists_pair_ne⟩

Premises used: Nontrivial.mk, IsField.exists_pair_ne
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x x_1 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
obtain : ∀ (x_2 : R) (hx : a * x_2 = 1), x = x_1
⊢ x = x_1

Tactic:
obtain ⟨x, hx⟩ := h.mul_inv_cancel ha

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x_1 x_2 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x_1) ((fun (x : R) ↦ a * x) x_2)
x : R
hx : a * x = 1
⊢ x_1 = x_2

Tactic:
simpa [← mul_assoc, h.mul_comm, hx] using congr_arg (x * ·) hb

Premises used: HMul.hMul, mul_assoc, IsField.mul_comm, congr_arg
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x x_1 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
obtain : ∀ (x_2 : R) (hx : a * x_2 = 1), x = x_1
⊢ x = x_1

Tactic:
obtain ⟨x, hx⟩ := h.mul_inv_cancel ha

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
x_1 x_2 : R
hb : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x_1) ((fun (x : R) ↦ x * a) x_2)
x : R
hx : a * x = 1
⊢ x_1 = x_2

Tactic:
simpa [mul_assoc, hx] using congr_arg (· * x) hb

Premises used: HMul.hMul, mul_assoc, congr_arg
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semifield R
⊢ IsDomain R

Tactic:
(Semifield.toIsField _).isDomain

Premises used: Semifield.toIsField, IsField.isDomain
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
inst_1 : Subsingleton R
⊢ ¬IsField R

Tactic:
fun h =>
  let ⟨_, _, h⟩ := h.exists_pair_ne
  h (Subsingleton.elim _ _)

Premises used: False, _private.0.not_isField_of_subsingleton.match_1, IsField.exists_pair_ne, Subsingleton.elim, Not
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ a * choose (p := fun (x : R) ↦ a * x = 1) ⋯ = 1

Tactic:
Classical.choose_spec (h.mul_inv_cancel ha)

Premises used: Classical.choose_spec, IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
h₁ : (if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) ⋯) = choose (p := fun (x : R) ↦ a * x = 1) ⋯
⊢ (a * if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) ⋯) = 1

Tactic:
convert! Classical.choose_spec (h.mul_inv_cancel ha)

Premises used: Classical.choose_spec, IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) ⋯) = choose (p := fun (x : R) ↦ a * x = 1) ⋯

Tactic:
dif_neg ha

Premises used: dif_neg
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else choose (p := fun (x : R) ↦ a * x = 1) ⋯) = choose (p := fun (x : R) ↦ a * x = 1) ⋯

Tactic:
exact dif_neg ha

Premises used: dif_neg
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
hex : ∃ (x_1 : R), x * x_1 = 1
hunique : ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
⊢ ∃! y : R, x * y = 1

Tactic:
apply existsUnique_of_exists_of_unique

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ (x_1 : R), x * x_1 = 1

Tactic:
hf.mul_inv_cancel hx

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ (x_1 : R), x * x_1 = 1

Tactic:
exact hf.mul_inv_cancel hx

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : y = y * 1
rw₁ rw₂ : y = y
⊢ y = y * (x * z)

Tactic:
rw [hxz, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : y * x * z = x * y * z
rw₁ rw₂ : x * y * z = x * y * z
⊢ y * (x * z) = x * y * z

Tactic:
rw [← mul_assoc, hf.mul_comm y x]

Premises used: mul_assoc, IsField.mul_comm
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
rw : 1 * z = z
rw₁ rw₂ : z = z
⊢ x * y * z = z

Tactic:
rw [hxy, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Field.IsField
Goal:
R : Type u
inst : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
y₁ : y = y * (x * z)
y₂ : y * (x * z) = x * y * z
y₃ : x * y * z = z
⊢ y = z

Tactic:
calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

Premises used: HMul.hMul
-- Module: Mathlib.Algebra.Field.ModEq
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
⊢ a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]

Tactic:
simp [modEq_iff_nsmul, add_div' _ _ _ hc, div_left_inj' hc, mul_assoc]

Premises used: mul_assoc, add_div', div_left_inj', AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Field.ModEq
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c p : K
hc : c ≠ 0
rw : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p * c⁻¹]
rw₁ : a * c ≡ b * c [PMOD p] ↔ a / c⁻¹ ≡ b / c⁻¹ [PMOD p]
rw₂ : a * c ≡ b * c [PMOD p] ↔ a * c ≡ b / c⁻¹ [PMOD p]
rw₃ rw₄ : a * c ≡ b * c [PMOD p] ↔ a * c ≡ b * c [PMOD p]
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]

Tactic:
rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]

Premises used: AddCommGroup.div_modEq_div, div_eq_mul_inv, inv_ne_zero, div_inv_eq_mul
-- Module: Mathlib.Algebra.Field.ModEq
Goal:
K : Type u_1
inst : Semifield K
a b c p : K
hc : c ≠ 0
⊢ c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]

Tactic:
simp [mul_comm c, hc]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Field.NegOnePow
Goal:
K : Type u_1
n : ℤ
inst : DivisionRing K
inl : ∀ (k : ℤ), (↑(↑(2 * k).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k)
inr : ∀ (k : ℤ), (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k + 1)
⊢ (↑(↑n.negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩

Premises used: Int.even_or_odd', rfl
-- Module: Mathlib.Algebra.Field.NegOnePow
Goal:
K : Type u_1
inst : DivisionRing K
k : ℤ
⊢ (↑(↑(2 * k).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k)

Tactic:
simp [zpow_mul, zpow_ofNat]

Premises used: zpow_mul, zpow_ofNat
-- Module: Mathlib.Algebra.Field.NegOnePow
Goal:
K : Type u_1
inst : DivisionRing K
k : ℤ
⊢ Ne.{u_1 + 1} (α := K) (-1) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Field.NegOnePow
Goal:
K : Type u_1
inst : DivisionRing K
k : ℤ
inr : (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (β := ℕ) (-1) 2 ^ k * -1
⊢ (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (-1) (2 * k + 1)

Tactic:
rw [zpow_add_one₀ (by simp), zpow_mul, zpow_ofNat]

Premises used: zpow_add_one₀, zpow_mul, zpow_ofNat
-- Module: Mathlib.Algebra.Field.NegOnePow
Goal:
K : Type u_1
inst : DivisionRing K
k : ℤ
⊢ (↑(↑(2 * k + 1).negOnePow : ℤ) : K) = HPow.hPow (α := K) (β := ℕ) (-1) 2 ^ k * -1

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : NNRatCast α
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ) (op (↑q : α)) (↑q : αᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : NNRatCast α
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := α) (unop (↑q : αᵐᵒᵖ)) (↑q : α)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : RatCast α
q : ℚ
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ) (op (↑q : α)) (↑q : αᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : RatCast α
q : ℚ
⊢ Eq.{u_1 + 1} (α := α) (unop (↑q : αᵐᵒᵖ)) (↑q : α)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : (↑q : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₂ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : (↑q : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₅ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₆ rw₇ : HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))

Tactic:
rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]

Premises used: Nat.cast_comm, NNRat.cast_def, MulOpposite.unop_nnratCast, div_eq_mul_inv, MulOpposite.unop_natCast, MulOpposite.unop_div
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (unop (↑q.den : αᵐᵒᵖ))⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (unop (↑q.num : αᵐᵒᵖ))
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.den : α)⁻¹ (↑q.num : α)
rw₅ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
rw₆ rw₇ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
⊢ unop (↑q : αᵐᵒᵖ) = unop (HDiv.hDiv (α := αᵐᵒᵖ) (↑q.num : αᵐᵒᵖ) (↑q.den : αᵐᵒᵖ))

Tactic:
rw [unop_ratCast, Rat.cast_def, unop_div,
    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]

Premises used: Int.commute_cast, MulOpposite.unop_ratCast, div_eq_mul_inv, Rat.cast_def, MulOpposite.unop_intCast, MulOpposite.unop_natCast, MulOpposite.unop_div
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₂ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
rw₅ rw₆ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))

Tactic:
rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]

Premises used: NNRat.cast_def, AddOpposite.unop_nnratCast, div_eq_mul_inv, AddOpposite.unop_natCast, AddOpposite.unop_div
-- Module: Mathlib.Algebra.Field.Opposite
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (↑q.den : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
rw₅ rw₆ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))

Tactic:
rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]

Premises used: AddOpposite.unop_intCast, AddOpposite.unop_ratCast, div_eq_mul_inv, AddOpposite.unop_natCast, Rat.cast_def, AddOpposite.unop_div