awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
rw : -(a / a) = -1
⊢ -a / a = -1
have rw₁ : Eq.{u_1 + 1} (α := K) (-1) (-1)
Tactic: rw [neg_div, div_self h]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c
have rw : a / c + -(b / c) = (a - b) / c
Tactic: rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a b c : K
rw : a / c + -(b / c) = (a - b) / c
⊢ a / c - b / c = (a - b) / c
have rw₁ : a / c + -b / c = (a - b) / c
Tactic: rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a / c - b / c = (a - b) / c
have rw₂ : (a + -b) / c = (a - b) / c
Tactic: rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a / c - b / c = (a - b) / c
have rw₃ : (a + -b) / c = (a + -b) / c
Tactic: rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
have 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
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr : ∀ (ha : a ≠ 0), a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr : a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ ha, ← pow_two, sq_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
ha : a ≠ 0
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr : a = 1 ∨ a = -1 → a = -1 ∨ a = 0 ∨ a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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 = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₁ : a = -1 ∨ a = 0 ∨ a = 1 → a = 1 ∨ a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₂ : a = 1 → a = -1 ∨ a = 0 ∨ a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₃ : a = -1 → a = -1 ∨ a = 0 ∨ a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₆ : a = 1 → ¬a = -1 → a = 0 ∨ a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₇ : a = -1 → ¬a = -1 → a = 0 ∨ a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₈ : a = -1 → a = 1 ∨ a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₉ : a = 0 → a = 1 ∨ a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₁₀ : a = 1 → a = 1 ∨ a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₁₃ : a = -1 → ¬a = 1 → a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₁₄ : a = 1 → ¬a = 1 → a = -1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
have inr₁₇ : a = 1 → ¬a = -1 → ¬a = 0 → a = 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1
have rw : a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Tactic: rw [eq_comm, inv_eq_self₀]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
rw : a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1
have rw₁ : a = -1 ∨ a = 0 ∨ a = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Tactic: rw [eq_comm, inv_eq_self₀]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
⊢ a - a / 2 = a / 2
have rw : a = a / 2 + a / 2
Tactic: rw [sub_eq_iff_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : a = a / 2 + a / 2
⊢ a - a / 2 = a / 2
have rw₁ : a = a
Tactic: rw [sub_eq_iff_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
⊢ a / 2 - a = -(a / 2)
have rw : -(a - a / 2) = -(a / 2)
Tactic: rw [← neg_sub, sub_half]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : -(a - a / 2) = -(a / 2)
⊢ a / 2 - a = -(a / 2)
have rw₁ : -(a / 2) = -(a / 2)
Tactic: rw [← neg_sub, sub_half]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have pos : ∀ (h : a = 0), a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have neg : ∀ (h : ¬a = 0), a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have pos : HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
Tactic: rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have pos₁ : a ^ (n + 1) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
Tactic: rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have pos₂ : a ^ (n + 1) = a ^ n * a
Tactic: rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have pos₃ : a ^ n * a = a ^ n * a
Tactic: rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
a : K
n : ℕ
h : ¬a = 0
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have neg : HPow.hPow (β := ℤ) a (↑n : ℤ) * a = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
Tactic: rw [zpow_add_one₀ h]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
have rw : 1 / 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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
have rw₁ : 1 / a - 1 / b = (b - a) / (a * b)
Tactic: rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
have rw₂ : (1 * b - a * 1) / (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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
have rw₃ : (b - a * 1) / (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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
have rw₄ : (b - a) / (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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw : (↑q : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
Tactic: rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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))
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₁ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
Tactic: rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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))
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₂ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = f (↑q.num : K) / f (↑q.den : K)
Tactic: rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₃ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = (↑q.num : L) / f (↑q.den : K)
Tactic: rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ f (↑q : K) = f (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K))
have rw₄ : HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L) = HDiv.hDiv (α := L) (↑q.num : L) (↑q.den : L)
Tactic: rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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
⊢ f (q • a) = f ((↑q : K) * a)
have rw : q • f a = f ((↑q : K) * a)
Tactic: rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ f (q • a) = f ((↑q : K) * a)
have rw₁ : (↑q : L) * f a = f ((↑q : K) * a)
Tactic: rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
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)
⊢ f (q • a) = f ((↑q : K) * a)
have rw₂ : (↑q : L) * f a = f (↑q : K) * f a
Tactic: rw [nnqsmul, NNRat.smul_def, mul, nnratCast]