awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
hfg : ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x
x : N ⧸ f.range
mpr :
  ∀ (x : N),
    Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) (Submodule.Quotient.mk x) : P) (0 : P) ↔
      Eq (α := N ⧸ f.range) (Submodule.Quotient.mk x) 0
⊢ Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0

Tactic:
obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x

Premises used: Submodule.Quotient.mk_surjective, rfl
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
hfg : ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x
x : N
⊢ Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) (Submodule.Quotient.mk x) : P) (0 : P) ↔
    Eq (α := N ⧸ f.range) (Submodule.Quotient.mk x) 0

Tactic:
simpa using hfg x
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ Function.Injective.{u_4 + 1, u_6 + 1} (α := N ⧸ f.range) (β := P) (⇑(f.range.liftQ g ⋯) : (a : N ⧸ f.range) → P)

Tactic:
simpa only [← LinearMap.ker_eq_bot, ker_eq_bot_range_liftQ_iff, exact_iff] using h

Premises used: LinearMap.ker_eq_bot, LinearMap.exact_iff, LinearMap.ker_eq_bot_range_liftQ_iff
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : N
⊢ Eq.{u_4 + 1} (α := N ⧸ f.range)
    (((h.linearEquivOfSurjective hg).symm : (a : P) → N ⧸ f.range) ((g : (a : N) → P) x) : N ⧸ f.range)
    (Submodule.Quotient.mk x : N ⧸ f.range)

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.Algebra.Field.Action.ConjAct
Goal:
K : Type u_1
inst : DivisionRing K
⊢ ∀ (a : ConjAct K), HSMul.hSMul (β := K) a 0 = 0

Tactic:
simp [smul_def]

Premises used: ConjAct.smul_def
-- Module: Mathlib.Algebra.Field.Action.ConjAct
Goal:
K : Type u_1
inst : DivisionRing K
⊢ ∀ (a : ConjAct K) (x y : K), a • (x + y) = a • x + a • y

Tactic:
simp [smul_def, mul_add, add_mul]

Premises used: ConjAct.smul_def, add_mul, mul_add
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
simp_rw : (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹
⊢ (a + b) / c = a / c + b / c

Tactic:
simp_rw [div_eq_mul_inv, add_mul]

Premises used: add_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
rw : (b + a) / b = b / b + a / b
rw₁ rw₂ : b / b + a / b = b / b + a / b
⊢ (b + a) / b = 1 + a / b

Tactic:
rw [← div_self h, add_div]

Premises used: div_self, add_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
rw : (a + b) / b = a / b + b / b
rw₁ rw₂ : a / b + b / b = a / b + b / b
⊢ (a + b) / b = a / b + 1

Tactic:
rw [← div_self h, add_div]

Premises used: div_self, add_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ 1 + a / b = (b + a) / b

Tactic:
(same_add_div h).symm

Premises used: same_add_div, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ a / b + 1 = (a + b) / b

Tactic:
(div_add_same h).symm

Premises used: div_add_same, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹

Tactic:
let _ := invertibleOfNonzero ha; let _ := invertibleOfNonzero hb; invOf_add_invOf a b

Premises used: invertibleOfNonzero, invOf_add_invOf
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

Tactic:
simpa only [one_div] using (inv_add_inv' ha hb).symm

Premises used: inv_add_inv', one_div, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
c a b : K
hc : c ≠ 0
rw : a * c + b / c * c = a * c + b
rw₁ rw₂ : a * c + b = a * c + b
⊢ (a + b / c) * c = a * c + b

Tactic:
rw [right_distrib, div_mul_cancel₀ _ hc]

Premises used: div_mul_cancel₀, right_distrib
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
rw : b + a / c = b * c / c + a / c
rw₁ rw₂ : b + a / c = b + a / c
⊢ b + a / c = (b * c + a) / c

Tactic:
rw [add_div, mul_div_cancel_right₀ _ hc]

Premises used: mul_div_cancel_right₀, add_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
rwa : b + a / c = (a + b * c) / c
rwa₁ : (b * c + a) / c = (a + b * c) / c
hc₁ : c ≠ 0
rwa₂ : (a + b * c) / c = (a + b * c) / c
hc₂ : c ≠ 0
rwa₃ : (a + b * c) / c = (a + b * c) / c
hc₃ hc₄ hc₅ : c ≠ 0
⊢ a / c + b = (a + b * c) / c

Tactic:
rwa [add_comm, add_div', add_comm]

Premises used: add_comm, add_div'
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
rw₁ : a / b + c / d = a / b + b * c / (b * d)
rw₂ : a / b + c / d = a / b + c * b / (b * d)
rw₃ : a / b + c / d = a / b + c * b / (d * b)
rw₄ rw₅ : a / b + c / d = a / b + c / d
⊢ a / b + c / d = (a * d + b * c) / (b * d)

Tactic:
rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]

Premises used: mul_div_mul_right, Commute.eq, add_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : (1 * b + a * 1) / (a * b) = (a + b) / (a * b)
rw₁ : (b + a * 1) / (a * b) = (a + b) / (a * b)
rw₂ : (b + a) / (a * b) = (a + b) / (a * b)
rw₃ rw₄ : (a + b) / (a * b) = (a + b) / (a * b)
⊢ 1 / a + 1 / b = (a + b) / (a * b)

Tactic:
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]

Premises used: Commute.div_add_div, add_comm, mul_one, Commute.one_right, one_mul
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : 1 / a + b⁻¹ = (a + b) / (a * b)
rw₁ : 1 / a + 1 / b = (a + b) / (a * b)
rw₂ rw₃ : (a + b) / (a * b) = (a + b) / (a * b)
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]

Premises used: inv_eq_one_div, Commute.one_div_add_one_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : a * 2 / 2 = a
rw₁ rw₂ : a = a
⊢ (a + a) / 2 = a

Tactic:
rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]

Premises used: mul_div_cancel_right₀, two_ne_zero, mul_two
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : (a + a) / 2 = a
rw₁ rw₂ : a = a
⊢ a / 2 + a / 2 = a

Tactic:
rw [← add_div, add_self_div_two]

Premises used: add_div, add_self_div_two
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
rw : -(a / a) = -1
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) (-1) (-1)
⊢ a / -a = -1

Tactic:
rw [div_neg_eq_neg_div, div_self h]

Premises used: div_neg_eq_neg_div, div_self
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
rw : -(a / a) = -1
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) (-1) (-1)
⊢ -a / a = -1

Tactic:
rw [neg_div, div_self h]

Premises used: neg_div, div_self
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b c : K
rw : a / c + -(b / c) = (a - b) / c
rw₁ : a / c + -b / c = (a - b) / c
rw₂ : (a + -b) / c = (a - b) / c
rw₃ rw₄ : (a + -b) / c = (a + -b) / c
⊢ a / c - b / c = (a - b) / c

Tactic:
rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]

Premises used: neg_div, sub_eq_add_neg, add_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b

Tactic:
simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm

Premises used: div_sub_div_same, Eq.symm, div_self
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
h : b ≠ 0
⊢ 1 - a / b = (b - a) / b

Tactic:
(same_sub_div h).symm

Premises used: same_sub_div, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1

Tactic:
simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm

Premises used: div_sub_div_same, Eq.symm, div_self
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
h : b ≠ 0
⊢ a / b - 1 = (a - b) / b

Tactic:
(div_sub_same h).symm

Premises used: div_sub_same, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b c : K
⊢ (a - b) / c = a / c - b / c

Tactic:
(div_sub_div_same _ _ _).symm

Premises used: div_sub_div_same, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹

Tactic:
let _ := invertibleOfNonzero ha; let _ := invertibleOfNonzero hb; invOf_sub_invOf a b

Premises used: invOf_sub_invOf, invertibleOfNonzero
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

Tactic:
simpa only [one_div] using (inv_sub_inv' ha hb).symm

Premises used: inv_sub_inv', one_div, Eq.symm
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
inl : Eq.{u_1 + 1} (α := K) 0⁻¹ 0 ↔ Eq.{u_1 + 1} (α := K) 0 (-1) ∨ Eq.{u_1 + 1} (α := K) 0 0 ∨ Eq.{u_1 + 1} (α := K) 0 1
inr : ∀ (ha : a ≠ 0), a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
⊢ Eq.{u_1 + 1} (α := K) 0⁻¹ 0 ↔ Eq.{u_1 + 1} (α := K) 0 (-1) ∨ Eq.{u_1 + 1} (α := K) 0 0 ∨ Eq.{u_1 + 1} (α := K) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
ha : a ≠ 0
inr : a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
rw [← mul_eq_one_iff_inv_eq₀ ha, ← pow_two, sq_eq_one_iff]

Premises used: sq_eq_one_iff, pow_two, mul_eq_one_iff_inv_eq₀
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
ha : a ≠ 0
inr : a = 1 ∨ a = -1 → a = -1 ∨ a = 0 ∨ a = 1
inr₁ : a = -1 ∨ a = 0 ∨ a = 1 → a = 1 ∨ a = -1
inr₂ : a = 1 → a = -1 ∨ a = 0 ∨ a = 1
inr₃ : a = -1 → a = -1 ∨ a = 0 ∨ a = 1
inr₄ : a = 1 → a = -1 ∨ a = 0 ∨ a = 1
inr₅ : a = -1 → a = -1 ∨ a = 0 ∨ a = 1
inr₆ : a = 1 → ¬a = -1 → a = 0 ∨ a = 1
inr₇ : a = -1 → ¬a = -1 → a = 0 ∨ a = 1
inr₈ : a = -1 → a = 1 ∨ a = -1
inr₉ : a = 0 → a = 1 ∨ a = -1
inr₁₀ : a = 1 → a = 1 ∨ a = -1
inr₁₁ : a = -1 → a = 1 ∨ a = -1
inr₁₂ : a = 1 → a = 1 ∨ a = -1
inr₁₃ : a = -1 → ¬a = 1 → a = -1
inr₁₄ : a = 1 → ¬a = 1 → a = -1
inr₁₅ inr₁₆ : a = 1 → ¬a = -1 → a = 0 ∨ a = 1
inr₁₇ : a = 1 → ¬a = -1 → ¬a = 0 → a = 1
inr₁₈ : a = -1 → ¬a = -1 → a = 0 ∨ a = 1
inr₁₉ : a = 1 → ¬a = 1 → a = -1
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
tauto
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a : K
rw : a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
rw₁ rw₂ : a = -1 ∨ a = 0 ∨ a = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
rw [eq_comm, inv_eq_self₀]

Premises used: eq_comm, inv_eq_self₀
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : DivisionRing K
a b c d : K
⊢ IsDomain K

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd

Premises used: neg_div, sub_eq_add_neg, Commute.div_add_div, Commute.neg_right, mul_neg
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]

Premises used: inv_eq_one_div, Commute.div_sub_div, mul_one, Commute.one_right, one_mul
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : a = a / 2 + a / 2
rw₁ rw₂ : a = a
⊢ a - a / 2 = a / 2

Tactic:
rw [sub_eq_iff_eq_add, add_halves]

Premises used: add_halves, sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : -(a - a / 2) = -(a / 2)
rw₁ rw₂ : -(a / 2) = -(a / 2)
⊢ a / 2 - a = -(a / 2)

Tactic:
rw [← neg_sub, sub_half]

Premises used: neg_sub, sub_half
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Semifield K
b d a c : K
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)

Tactic:
(Commute.all b _).div_add_div (Commute.all _ _) hb hd

Premises used: Commute.div_add_div, Commute.all
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Semifield K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)

Tactic:
(Commute.all a _).one_div_add_one_div ha hb

Premises used: Commute.all, Commute.one_div_add_one_div
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Semifield K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)

Tactic:
(Commute.all a _).inv_add_inv ha hb

Premises used: Commute.all, Commute.inv_add_inv
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
⊢ HPow.hPow (β := ℤ) a 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
pos : ∀ (h : a = 0), a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
neg : ∀ (h : ¬a = 0), a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
h : a = 0
pos : HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
pos₁ : a ^ (n + 1) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
pos₂ : a ^ (n + 1) = a ^ n * a
pos₃ pos₄ : a ^ n * a = a ^ n * a
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]

Premises used: zpow_natCast, pow_succ, Int.natCast_add_one
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
h : ¬a = 0
neg neg₁ : HPow.hPow (β := ℤ) a (↑n : ℤ) * a = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
rw [zpow_add_one₀ h]

Premises used: zpow_add_one₀
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℤ
⊢ a ^ (-n) = (a ^ n)⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
a b c d : K
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
(Commute.all b _).div_sub_div (Commute.all _ _) hb hd

Premises used: Commute.div_sub_div, Commute.all
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
rw : 1 / a - b⁻¹ = (b - a) / (a * b)
rw₁ : 1 / a - 1 / b = (b - a) / (a * b)
rw₂ : (1 * b - a * 1) / (a * b) = (b - a) / (a * b)
rw₃ : (b - a * 1) / (a * b) = (b - a) / (a * b)
rw₄ rw₅ : (b - a) / (a * b) = (b - a) / (a * b)
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]

Premises used: inv_eq_one_div, mul_one, div_sub_div, one_mul
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c

Tactic:
simpa using div_sub_div b a one_ne_zero hc

Premises used: div_sub_div, one_ne_zero
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c

Tactic:
simpa using div_sub_div a b hc one_ne_zero

Premises used: div_sub_div, one_ne_zero
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
⊢ IsDomain K

Tactic:
{ DivisionRing.isDomain with }

Premises used: DivisionRing.isDomain
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
q : ℚ≥0
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₁ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₂ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = f (↑q.num : K) / f (↑q.den : K)
rw₃ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = (↑q.num : L) / f (↑q.den : K)
rw₄ rw₅ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))

Tactic:
rw [nnratCast, NNRat.cast_def, div, natCast, natCast]

Premises used: NNRat.cast_def
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
q : ℚ≥0
a : K
rw : q • f a = f ((↑q : K) * a)
rw₁ : (↑q : L) * f a = f ((↑q : K) * a)
rw₂ : (↑q : L) * f a = f (↑q : K) * f a
rw₃ rw₄ : (↑q : L) * f a = (↑q : L) * f a
⊢ f (q • a) = f ((↑q : K) * a)

Tactic:
rw [nnqsmul, NNRat.smul_def, mul, nnratCast]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
rw₁ : (↑q : L) = f (↑q.num : K) / f (↑q.den : K)
rw₂ : (↑q : L) = (↑q.num : L) / f (↑q.den : K)
rw₃ : (↑q : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
rw₄ rw₅ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))

Tactic:
rw [ratCast, div, intCast, natCast, Rat.cast_def]

Premises used: Rat.cast_def
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Zero K
inst_1 : Add K
inst_2 : Neg K
inst_3 : Sub K
inst_4 : One K
inst_5 : Mul K
inst_6 : Inv K
inst_7 : Div K
inst_8 : SMul ℕ K
inst_9 : SMul ℤ K
inst_10 : SMul ℚ≥0 K
inst_11 : SMul ℚ K
inst_12 : Pow K ℕ
inst_13 : Pow K ℤ
inst_14 : NatCast K
inst_15 : IntCast K
inst_16 : NNRatCast K
inst_17 : RatCast K
f : K → L
hf : Injective f
inst_18 : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : K) = (↑n : L)
intCast : ∀ (n : ℤ), f (↑n : K) = (↑n : L)
nnratCast : ∀ (q : ℚ≥0), f (↑q : K) = (↑q : L)
ratCast : ∀ (q : ℚ), f (↑q : K) = (↑q : L)
q : ℚ
a : K
rw : q • f a = f ((↑q : K) * a)
rw₁ : q • f a = f (↑q : K) * f a
rw₂ : (↑q : L) * f a = f (↑q : K) * f a
rw₃ rw₄ : (↑q : L) * f a = (↑q : L) * f a
⊢ f (q • a) = f ((↑q : K) * a)

Tactic:
rw [qsmul, mul, Rat.smul_def, ratCast]

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : RatCast K
n : ℚ
⊢ Eq.{u_1 + 1} (α := Kᵒᵈ) ((toDual : (a : K) → Kᵒᵈ) (↑n : K) : Kᵒᵈ) ((↑n : Kᵒᵈ) : Kᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : RatCast K
n : ℚ
⊢ Eq.{u_1 + 1} (α := K) ((ofDual : (a : Kᵒᵈ) → K) (↑n : Kᵒᵈ) : K) ((↑n : K) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : RatCast K
n : ℚ
⊢ Eq.{u_1 + 1} (α := Lex K) ((toLex : (a : K) → Lex K) (↑n : K) : Lex K) ((↑n : Lex K) : Lex K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Basic
Goal:
K : Type u_1
inst : RatCast K
n : ℚ
⊢ Eq.{u_1 + 1} (α := K) ((ofLex : (a : Lex K) → K) (↑n : Lex K) : K) ((↑n : K) : K)

Tactic:
rfl

Premises used: rfl