awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₃ rw₄ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]

Premises used: inv_pow, inv_inv, pow_sub₀, inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₃ rw₄ : (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]

Premises used: pow_sub_of_lt, inv_pow, Inv.inv, inv_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₃ rw₄ : a ^ m * (a ^ n)⁻¹ = a ^ m * (a ^ n)⁻¹
⊢ a ^ (m - n) = a ^ m / a ^ n

Tactic:
rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]

Premises used: Int.sub_eq_add_neg, div_eq_mul_inv, zpow_add₀, zpow_neg
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) = a ^ m / a ^ n

Tactic:
simpa using zpow_sub₀ ha m n

Premises used: zpow_sub₀, Nat.cast
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) (↑n : ℤ) 1 = a ^ n / a

Tactic:
simpa using zpow_sub₀ ha n 1

Premises used: zpow_sub₀, Nat.cast, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ HSub.hSub (α := ℤ) 1 (↑n : ℤ) = a / a ^ n

Tactic:
simpa using zpow_sub₀ ha 1 n

Premises used: zpow_sub₀, Nat.cast, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
a_1 : ℕ
rw : a ≠ 0 → a ^ a_1 ≠ 0
⊢ a ≠ 0 → HPow.hPow (β := ℤ) a (↑a_1 : ℤ) ≠ 0

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
a_1 : ℕ
⊢ a ≠ 0 → a ^ a_1 ≠ 0

Tactic:
pow_ne_zero _

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
a_1 : ℕ
⊢ a ≠ 0 → a ^ a_1 ≠ 0

Tactic:
exact pow_ne_zero _

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
rw : (a ^ (n + 1))⁻¹ ≠ 0
⊢ a ^ Int.negSucc n ≠ 0

Tactic:
rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0

Tactic:
inv_ne_zero (pow_ne_zero _ ha)

Premises used: pow_ne_zero, inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (pow_ne_zero _ ha)

Premises used: pow_ne_zero, inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ n = 0 → a = 0

Tactic:
not_imp_not.1 (zpow_ne_zero _)

Premises used: Iff.mp, zpow_ne_zero, not_imp_not
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0

Tactic:
⟨eq_zero_of_zpow_eq_zero, fun ha => ha.symm ▸ zero_zpow _ hn⟩

Premises used: zero_zpow, Eq.rec, eq_zero_of_zpow_eq_zero, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
hn : n ≠ 0
⊢ a ^ n ≠ 0 ↔ a ≠ 0

Tactic:
(zpow_eq_zero_iff hn).ne

Premises used: zpow_eq_zero_iff, Iff.ne
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
rw : (a ^ n)⁻¹ * a ^ n = 1
⊢ a ^ (-n) * a ^ n = 1

Tactic:
rw [zpow_neg]

Premises used: zpow_neg
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Tactic:
inv_mul_cancel₀ (zpow_ne_zero n ha)

Premises used: zpow_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Tactic:
exact inv_mul_cancel₀ (zpow_ne_zero n ha)

Premises used: zpow_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
inl : Eq.{u_3 + 1} (α := G₀) 0⁻¹ʳ 0⁻¹
inr : ∀ (ha : a ≠ 0), a⁻¹ʳ = a⁻¹
⊢ a⁻¹ʳ = a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
⊢ Eq.{u_3 + 1} (α := G₀) 0⁻¹ʳ 0⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹

Tactic:
Ring.inverse_unit (Units.mk0 a ha)

Premises used: Units.mk0, Ring.inverse_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹

Tactic:
exact Ring.inverse_unit (Units.mk0 a ha)

Premises used: Units.mk0, Ring.inverse_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
⊢ Eq.{u_3 + 1} (α := G₀ → G₀) inverse Inv.inv

Tactic:
funext Ring.inverse_eq_inv

Premises used: Ring.inverse_eq_inv, funext
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b : G₀
⊢ a / (a * b) = b⁻¹

Tactic:
ha.isUnit.div_mul_cancel_left _

Premises used: Ne.isUnit, IsUnit.div_mul_cancel_left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
rw : b * a / a = b
rw₁ rw₂ : b = b
⊢ a * b / a = b

Tactic:
rw [mul_comm, mul_div_cancel_of_imp h]

Premises used: mul_comm, mul_div_cancel_of_imp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
rw : a / b * b = a
rw₁ rw₂ : a = a
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel_of_imp h]

Premises used: div_mul_cancel_of_imp, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c * a / (c * b) = a / b

Tactic:
hc.isUnit.mul_div_mul_left _ _

Premises used: IsUnit.mul_div_mul_left, Ne.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₅ rw₆ : c * b = c * b
⊢ a * d = c * b

Tactic:
rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]

Premises used: div_mul_cancel₀, div_mul_eq_mul_div, mul_comm_div, mul_one, div_self
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
hb.isUnit.div_eq_div_iff hd.isUnit

Premises used: Ne.isUnit, IsUnit.div_eq_div_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hd : d ≠ 0
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
hb.isUnit.mul_inv_eq_mul_inv_iff hd.isUnit

Premises used: Ne.isUnit, IsUnit.mul_inv_eq_mul_inv_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hd : d ≠ 0
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
hb.isUnit.inv_mul_eq_inv_mul_iff hd.isUnit

Premises used: IsUnit.inv_mul_eq_inv_mul_iff, Ne.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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 / b = c / d

Tactic:
rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]

Premises used: div_mul_cancel₀, mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
conv_lhs : a = c / d * b ↔ a / c = b / d
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]

Premises used: div_mul_cancel₀, mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
rw : a = b / d * c
| a / c = b / d

Tactic:
rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]

Premises used: div_mul_cancel₀, mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
conv_rhs : a = c / d * b ↔ a = b / d * c
⊢ a = c / d * b ↔ a / c = b / d

Tactic:
conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]

Premises used: div_mul_cancel₀, mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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)
rw₂ rw₃ : a = c * (b / d) ↔ a = c * (b / d)
⊢ a = c / d * b ↔ a = b / d * c

Tactic:
rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, div_mul_eq_mul_div, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
⊢ 0 = c / d

Tactic:
rw [hb, div_zero] at h

Premises used: div_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
h₁ : 0 = c / d
⊢ b = 0

Tactic:
rw [hb, div_zero] at h

Premises used: div_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : 0 = c / d
hb : b = 0
⊢ False

Tactic:
div_ne_zero hc hd h.symm

Premises used: div_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : 0 = c / d
hb : b = 0
⊢ False

Tactic:
exact div_ne_zero hc hd h.symm

Premises used: div_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a / (a / b) = b

Tactic:
ha.isUnit.div_div_cancel

Premises used: Ne.isUnit, IsUnit.div_div_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a / b / a = b⁻¹

Tactic:
ha.isUnit.div_div_cancel_left

Premises used: Ne.isUnit, IsUnit.div_div_cancel_left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₃ rw₄ : b⁻¹ = b⁻¹
⊢ 1 / (a * b) * a = 1 / b

Tactic:
rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]

Premises used: div_mul_cancel_left₀, div_mul_eq_mul_div, one_div, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
rw₂ rw₃ : b / a = b / a
⊢ c / a / (c / b) = b / a

Tactic:
rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]

Premises used: mul_div_mul_right, div_div_div_eq, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
rw : c / a * (a / b) = c / b
rw₁ rw₂ : c / b = c / b
⊢ a / b * (c / a) = c / b

Tactic:
rw [mul_comm, div_mul_div_cancel₀ ha]

Premises used: mul_comm, div_mul_div_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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
change : (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1

Tactic:
change (a * if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹) = 1

Premises used: HMul.hMul, dite, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
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)
rw₃ rw₄ : a = a
⊢ (a * if h0 : a = 0 then 0 else (↑⋯.unit⁻¹ : M)) = 1

Tactic:
rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec]

Premises used: Units.mul_inv_eq_iff_eq_mul, dif_neg, IsUnit.unit_spec, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Equiv
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ Function.Bijective (β := G₀) fun (x : G₀) ↦ a * x

Tactic:
(Equiv.mulLeft₀ a ha).bijective

Premises used: Equiv.bijective, Equiv.mulLeft₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Equiv
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ Function.Bijective (β := G₀) fun (x : G₀) ↦ x * a

Tactic:
(Equiv.mulRight₀ a ha).bijective

Premises used: Equiv.bijective, Equiv.mulRight₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Equiv
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x : G₀
⊢ (fun (x : G₀) ↦ x * a) ((fun (x : G₀) ↦ x / a) x) = x

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Equiv
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x : G₀
⊢ (fun (x : G₀) ↦ x / a) ((fun (x : G₀) ↦ x * a) x) = x

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Equiv
Goal:
G₀ : Type u_1
inst : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
x : G₀
⊢ (fun (x : G₀) ↦ a / x) ((fun (x : G₀) ↦ a / x) x) = x

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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
inr : ∀ (h : a ≠ 0), IsUnit a
⊢ IsUnit a

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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)
inl : ∀ (t : G₀) (ht : Ne.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)), IsUnit.{u_3} (M := G₀) 0
⊢ IsUnit.{u_3} (M := G₀) 0

Tactic:
obtain ⟨t, ht⟩ := hf
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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

Tactic:
(ht ?_).elim

Premises used: False.elim
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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)
inl : Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)
⊢ IsUnit.{u_3} (M := G₀) 0

Tactic:
refine (ht ?_).elim

Premises used: False.elim
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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)
⊢ (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
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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)
⊢ 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

Premises used: HMul.hMul, MulZeroClass.mul_zero, OfNat.ofNat, DFunLike.coe, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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 :
  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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)

Tactic:
(h.mul_right_cancel this).symm

Premises used: IsUnit.mul_right_cancel, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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 :
  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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : G₀) → M) t : M) (1 : M)

Tactic:
exact (h.mul_right_cancel this).symm

Premises used: IsUnit.mul_right_cancel, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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_1 : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) a : M)
h : a ≠ 0
⊢ IsUnit a

Tactic:
⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩

Premises used: mul_inv_cancel₀, IsUnit, Inv.inv, Units.mk, Exists.intro, inv_mul_cancel₀, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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_1 : IsUnit.{u_1} (M := M) ((f : (a : G₀) → M) a : M)
h : a ≠ 0
⊢ IsUnit a

Tactic:
exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
M : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst : MonoidWithZero M₀
inst_1 : Monoid M
inst_2 : GroupWithZero G₀
inst_3 : FunLike F G₀ M₀
inst_4 : MonoidWithZeroHomClass F G₀ M₀
inst_5 : Nontrivial M₀
f : F
⊢ Ne.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 0 : M₀) (1 : M₀)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c d : G₀
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
hbd.div_eq_div_iff_of_isUnit hb.isUnit hd.isUnit

Premises used: Ne.isUnit, Commute.div_eq_div_iff_of_isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c d : G₀
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
hbd.mul_inv_eq_mul_inv_iff_of_isUnit hb.isUnit hd.isUnit

Premises used: Ne.isUnit, Commute.mul_inv_eq_mul_inv_iff_of_isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c d : G₀
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c

Tactic:
hbd.inv_mul_eq_inv_mul_iff_of_isUnit hb.isUnit hd.isUnit

Premises used: Ne.isUnit, Commute.inv_mul_eq_inv_mul_iff_of_isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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

Tactic:
⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩

Premises used: Eq.rec, map_zero, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀
refine : a ≠ 0 → Ne.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀')
⊢ Ne.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀') ↔ a ≠ 0

Tactic:
refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
⊢ IsUnit a

Tactic:
isUnit_iff_ne_zero.mpr hx

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
lift :
  ∀ (a : G₀ˣ) (hx : (↑a : G₀) ≠ 0) (H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')), False
⊢ False

Tactic:
lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
apply : Eq.{u_4 + 1} (α := M₀') 1 0
⊢ False

Tactic:
apply one_ne_zero (α := M₀')

Premises used: one_ne_zero