awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a * 0 / 0 = a
⊢ a * b / b = a
have inr : ∀ (hb : b ≠ 0), a * b / b = a
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have h1 : m - n + n = m
Tactic: have h1 : m - n + n = m := Nat.sub_add_cancel h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m
have rw : a ^ (m - n + n) = a ^ m
Tactic: rw [← pow_add, h1]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
rw : a ^ (m - n + n) = a ^ m
⊢ a ^ (m - n) * a ^ n = a ^ m
have rw₁ : a ^ m = a ^ m
Tactic: rw [← pow_add, h1]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have h2 : a ^ (m - n) * a ^ n = a ^ m
Tactic: have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have inl : HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
inl : HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
have inr : ∀ (ha : a ≠ 0), a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
have inl : 0 = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
Tactic: rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
h : n < m
inl : 0 = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
⊢ HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
have inl₁ : 0 = 0 * (HPow.hPow (α := G₀) 0 n)⁻¹
Tactic: rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
h : n < m
inl : 0 = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
inl₁ : 0 = 0 * (HPow.hPow (α := G₀) 0 n)⁻¹
⊢ HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
have inl₂ : Eq.{u_3 + 1} (α := G₀) 0 0
Tactic: rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₃ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
rw : a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₁ : (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
rw₂ : (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
have rw₃ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
Tactic: rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m - n) = a ^ m / a ^ n
have rw : a ^ (m + -n) = a ^ m / a ^ n
Tactic: rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
rw : a ^ (m + -n) = a ^ m / a ^ n
⊢ a ^ (m - n) = a ^ m / a ^ n
have rw₁ : a ^ m * a ^ (-n) = a ^ m / a ^ n
Tactic: rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
rw : a ^ (m + -n) = a ^ m / a ^ n
rw₁ : a ^ m * a ^ (-n) = a ^ m / a ^ n
⊢ a ^ (m - n) = a ^ m / a ^ n
have rw₂ : a ^ m * (a ^ n)⁻¹ = a ^ m / a ^ n
Tactic: rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
rw : a ^ (m + -n) = a ^ m / a ^ n
rw₁ : a ^ m * a ^ (-n) = a ^ m / a ^ n
rw₂ : a ^ m * (a ^ n)⁻¹ = a ^ m / a ^ n
⊢ a ^ (m - n) = a ^ m / a ^ n
have rw₃ : a ^ m * (a ^ n)⁻¹ = a ^ m * (a ^ n)⁻¹
Tactic: rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
a_1 : ℕ
⊢ a ≠ 0 → HPow.hPow (β := ℤ) a (↑a_1 : ℤ) ≠ 0
have rw : a ≠ 0 → a ^ a_1 ≠ 0
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ a ^ Int.negSucc n ≠ 0
have rw : (a ^ (n + 1))⁻¹ ≠ 0
Tactic: rw [zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ a ^ (-n) * a ^ n = 1
have rw : (a ^ n)⁻¹ * a ^ n = 1
Tactic: rw [zpow_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
⊢ a⁻¹ʳ = a⁻¹
have inl : Eq.{u_3 + 1} (α := G₀) 0⁻¹ʳ 0⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
inl : Eq.{u_3 + 1} (α := G₀) 0⁻¹ʳ 0⁻¹
⊢ a⁻¹ʳ = a⁻¹
have inr : ∀ (ha : a ≠ 0), a⁻¹ʳ = a⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b
have rw : b * a / a = b
Tactic: rw [mul_comm, mul_div_cancel_of_imp h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
rw : b * a / a = b
⊢ a * b / a = b
have rw₁ : b = b
Tactic: rw [mul_comm, mul_div_cancel_of_imp h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a
have rw : a / b * b = a
Tactic: rw [mul_comm, div_mul_cancel_of_imp h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
rw : a / b * b = a
⊢ b * (a / b) = a
have rw₁ : a = a
Tactic: rw [mul_comm, div_mul_cancel_of_imp h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * d = c * b
have rw : a * 1 * d = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
rw : a * 1 * d = c * b
⊢ a * d = c * b
have rw₁ : a * (b / b) * d = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
⊢ a * d = c * b
have rw₂ : a / b * b * d = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
⊢ a * d = c * b
have rw₃ : c / d * b * d = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
rw₃ : c / d * b * d = c * b
⊢ a * d = c * b
have rw₄ : c * b / d * d = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
rw : a * 1 * d = c * b
rw₁ : a * (b / b) * d = c * b
rw₂ : a / b * b * d = c * b
rw₃ : c / d * b * d = c * b
rw₄ : c * b / d * d = c * b
⊢ a * d = c * b
have rw₅ : c * b = c * b
Tactic: rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / b = c / d
have rw : a = c / d * b
Tactic: rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b = c / d ↔ a / c = b / d
have conv_lhs : a = c / d * b ↔ a / c = b / d
Tactic: conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / c = b / d
have rw : a = b / d * c
Tactic: rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a / c = b / d
have conv_rhs : a = c / d * b ↔ a = b / d * c
Tactic: conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = b / d * c
have rw : a = c / d * b ↔ a = c * (b / d)
Tactic: rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
rw : a = c / d * b ↔ a = c * (b / d)
⊢ a = c / d * b ↔ a = b / d * c
have rw₁ : a = c * b / d ↔ a = c * (b / d)
Tactic: rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
rw : a = c / d * b ↔ a = c * (b / d)
rw₁ : a = c * b / d ↔ a = c * (b / d)
⊢ a = c / d * b ↔ a = b / d * c
have rw₂ : a = c * (b / d) ↔ a = c * (b / d)
Tactic: rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
hb : b = 0
⊢ False
have h₁ : 0 = c / d
Tactic: rw [hb, div_zero] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ 1 / (a * b) * a = 1 / b
have rw : 1 * a / (a * b) = 1 / b
Tactic: rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
rw : 1 * a / (a * b) = 1 / b
⊢ 1 / (a * b) * a = 1 / b
have rw₁ : a / (a * b) = 1 / b
Tactic: rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
rw : 1 * a / (a * b) = 1 / b
rw₁ : a / (a * b) = 1 / b
⊢ 1 / (a * b) * a = 1 / b
have rw₂ : b⁻¹ = 1 / b
Tactic: rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
rw : 1 * a / (a * b) = 1 / b
rw₁ : a / (a * b) = 1 / b
rw₂ : b⁻¹ = 1 / b
⊢ 1 / (a * b) * a = 1 / b
have rw₃ : b⁻¹ = b⁻¹
Tactic: rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c / a / (c / b) = b / a
have rw : c * b / (a * c) = b / a
Tactic: rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
rw : c * b / (a * c) = b / a
⊢ c / a / (c / b) = b / a
have rw₁ : b * c / (a * c) = b / a
Tactic: rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
rw : c * b / (a * c) = b / a
rw₁ : b * c / (a * c) = b / a
⊢ c / a / (c / b) = b / a
have rw₂ : b / a = b / a
Tactic: rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ a / b * (c / a) = c / b
have rw : c / a * (a / b) = c / b
Tactic: rw [mul_comm, div_mul_div_cancel₀ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
rw : c / a * (a / b) = c / b
⊢ a / b * (c / a) = c / b
have rw₁ : c / b = c / b
Tactic: rw [mul_comm, div_mul_div_cancel₀ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1
have rw : a * (↑sorry.unit⁻¹ : M) = 1
Tactic: rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
rw : a * (↑⋯.unit⁻¹ : M) = 1
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1
have rw₁ : a = 1 * (↑sorry.unit : M)
Tactic: rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
rw : a * (↑⋯.unit⁻¹ : M) = 1
rw₁ : a = 1 * (↑⋯.unit : M)
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1
have rw₂ : a = (↑sorry.unit : M)
Tactic: rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
rw : a * (↑⋯.unit⁻¹ : M) = 1
rw₁ : a = 1 * (↑⋯.unit : M)
rw₂ : a = (↑⋯.unit : M)
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1
have rw₃ : a = a
Tactic: rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
hf : ∃ (x : G₀), Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) x : M) (1 : M)
a : G₀
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) a : M)
⊢ IsUnit a
have inl : ∀ (h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)), IsUnit.{u_3} (M := G₀) 0
Tactic: rcases eq_or_ne a 0 with (rfl | h)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
hf : ∃ (x : G₀), Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) x : M) (1 : M)
a : G₀
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) a : M)
inl : ∀ (h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)), IsUnit.{u_3} (M := G₀) 0
⊢ IsUnit a
have inr : ∀ (h : a ≠ 0), IsUnit a
Tactic: rcases eq_or_ne a 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
hf : ∃ (x : G₀), Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) x : M) (1 : M)
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)
⊢ IsUnit.{u_3} (M := G₀) 0
have inl : ∀ (t : G₀) (ht : Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)), IsUnit.{u_3} (M := G₀) 0
Tactic: obtain ⟨t, ht⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)
t : G₀
ht : Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
⊢ IsUnit.{u_3} (M := G₀) 0
have inl : Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
Tactic: refine (ht ?_).elim
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (hypothesis)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)
t : G₀
ht : Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
have this : (f : (a : G₀) → M) (t * 0) = HMul.hMul (α := M) (β := M) ((f : (a : G₀) → M) t : M) ((f : (a : G₀) → M) 0 : M)
Tactic: have := map_mul f t 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (hypothesis)
Goal:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : FunLike F G₀ M
inst_3 : MonoidHomClass F G₀ M
f : F
h : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) 0 : M)
t : G₀
ht : Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
this : (f : (a : G₀) → M) (t * 0) = HMul.hMul (α := M) (β := M) ((f : (a : G₀) → M) t : M) ((f : (a : G₀) → M) 0 : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
have this₁ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : G₀) → M) 0 : M) =
  HMul.hMul (α := M) (β := M) ((f : (a : G₀) → M) t : M) ((f : (a : G₀) → M) 0 : M)
Tactic: rw [← one_mul (f (t * 0)), mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
⊢ Ne.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀') ↔ a ≠ 0
have refine : a ≠ 0 → Ne.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀')
Tactic: refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
hx : a ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀')
⊢ False
have lift : ∀ (a : G₀ˣ) (hx : (↑a : G₀) ≠ 0) (H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')), False
Tactic: lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx
Cleared hypotheses: a, hx, H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
⊢ False
have apply : Eq.{u_4 + 1} (α := M₀') 1 0
Tactic: apply one_ne_zero (α := M₀')