awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
⊢ u = 1

Tactic:
rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy

Premises used: eq_comm, pow_eq_one_iff_left, IsLeftRegular.mul_left_eq_self_iff, Units.val_eq_one, Units.val_pow_eq_pow_val, mul_pow
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
hxy₁ : u = 1
⊢ x * (↑u : M) = y

Tactic:
rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy

Premises used: eq_comm, pow_eq_one_iff_left, IsLeftRegular.mul_left_eq_self_iff, Units.val_eq_one, Units.val_pow_eq_pow_val, mul_pow
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
hxy₁ : u = 1
hu₁ : x * (↑u : M) = y
⊢ IsLeftRegular (x ^ n)

Tactic:
rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy

Premises used: eq_comm, pow_eq_one_iff_left, IsLeftRegular.mul_left_eq_self_iff, Units.val_eq_one, Units.val_pow_eq_pow_val, mul_pow
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * (↑u : M) = y
hx : IsLeftRegular (x ^ n)
rwa : ∀ (hu : x * (↑1 : M) = y) (hx : IsLeftRegular (x ^ n)), x = y
rwa₁ : ∀ (hu : x * 1 = y) (hx : IsLeftRegular (x ^ n)), x = y
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hu : x = y) (hx : IsLeftRegular (x ^ n)), x = y
⊢ x = y

Tactic:
rwa [hxy, Units.val_one, mul_one] at hu

Premises used: Units.val_one, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ SemigroupWithZero α

Tactic:
apply e.injective.semigroupWithZero _

Premises used: Function.Injective.semigroupWithZero, Equiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
mul₁ :
  ∀ (a b : α),
    (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)
⊢ MulZeroClass α

Tactic:
apply e.injective.mulZeroClass _

Premises used: Function.Injective.mulZeroClass, Equiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a b : α
⊢ (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a b : α
⊢ (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (a b : α),
    (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)
⊢ MulZeroOneClass α

Tactic:
apply e.injective.mulZeroOneClass _

Premises used: Function.Injective.mulZeroOneClass, Equiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a b : α
⊢ (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a b : α
⊢ (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul :
  ∀ (x_2 y : α),
    (e : (a : α) → β) (x_2 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_2 : β) ((e : (a : α) → β) y : β)
npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ MonoidWithZero α

Tactic:
apply e.injective.monoidWithZero _

Premises used: Function.Injective.monoidWithZero, Equiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
x_2 y : α
⊢ (e : (a : α) → β) (x_2 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_2 : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
x_2 y : α
⊢ (e : (a : α) → β) (x_2 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_2 : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
x_2 : α
n : ℕ
⊢ (e : (a : α) → β) (x_2 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_2 : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
x_2 : α
n : ℕ
⊢ (e : (a : α) → β) (x_2 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_2 : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul :
  ∀ (x_1 y : α),
    (e : (a : α) → β) (x_1 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y : β)
npow : ∀ (x_1 : α) (n : ℕ), (e : (a : α) → β) (x_1 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_1 : β) n
⊢ CommMonoidWithZero α

Tactic:
apply e.injective.commMonoidWithZero _

Premises used: Function.Injective.commMonoidWithZero, Equiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
x_1 y : α
⊢ (e : (a : α) → β) (x_1 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
x_1 y : α
⊢ (e : (a : α) → β) (x_1 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
x_1 : α
n : ℕ
⊢ (e : (a : α) → β) (x_1 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_1 : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.TransferInstance
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
x_1 : α
n : ℕ
⊢ (e : (a : α) → β) (x_1 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_1 : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.GroupWithZero.ULift
Goal:
α : Type u
inst : MulZeroOneClass α
a b : ULift.{u_1, u} α
⊢ (Equiv.ulift : (a : ULift α) → α) (a * b) =
    HMul.hMul (α := α) (β := α) ((Equiv.ulift : (a : ULift α) → α) a : α) ((Equiv.ulift : (a : ULift α) → α) b : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
u : M₀ˣ
⊢ (↑u : M₀) ≠ 0

Tactic:
left_ne_zero_of_mul_eq_one u.mul_inv

Premises used: Units.mul_inv, left_ne_zero_of_mul_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * (↑u : M₀) = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_left h ↑u⁻¹

Premises used: Units.val, mul_eq_zero_of_left, Inv.inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : (↑u : M₀) * a = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_right (↑u⁻¹) h

Premises used: mul_eq_zero_of_right
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
a : M₀
ha : IsUnit a
⊢ a ≠ 0

Tactic:
let ⟨u, hu⟩ := ha
  hu ▸ u.ne_zero

Premises used: Eq.rec, Units.ne_zero, Ne, _private.0.IsUnit.ne_zero.match_1, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
ha : IsUnit a
⊢ a * b = 0 ↔ b = 0

Tactic:
let ⟨u, hu⟩ := ha
  hu ▸ u.mul_right_eq_zero

Premises used: HMul.hMul, Eq.rec, Units.mul_right_eq_zero, _private.0.IsUnit.ne_zero.match_1, Iff, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
hb : IsUnit b
⊢ a * b = 0 ↔ a = 0

Tactic:
let ⟨u, hu⟩ := hb
  hu ▸ u.mul_left_eq_zero

Premises used: HMul.hMul, Eq.rec, _private.0.IsUnit.ne_zero.match_1, Iff, OfNat.ofNat, Units.mul_left_eq_zero, Eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
h : IsUnit.{u_2} (M := M₀) 0
a : M₀
a0 : 0 * a = 1
inv_val : a * 0 = 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (a0 : Eq.{u_2 + 1} (α := M₀) 0 1), a * 0 = 1 → Eq.{u_2 + 1} (α := M₀) 0 1
⊢ Eq.{u_2 + 1} (α := M₀) 0 1

Tactic:
rwa [zero_mul] at a0

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ ¬IsUnit.{u_2} (M := M₀) 0

Tactic:
mt isUnit_zero_iff.1 zero_ne_one

Premises used: mt, zero_ne_one, isUnit_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (if h : IsUnit (↑u : M₀) then (↑h.unit⁻¹ : M₀) else 0) = (↑u⁻¹ : M₀)
rw₁ : (↑⋯.unit⁻¹ : M₀) = (↑u⁻¹ : M₀)
rw₂ rw₃ : (↑u⁻¹ : M₀) = (↑u⁻¹ : M₀)
⊢ (↑u : M₀)⁻¹ʳ = (↑u⁻¹ : M₀)

Tactic:
rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]

Premises used: dif_pos, Ring.inverse, Units.isUnit, IsUnit.unit_of_val_units
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x⁻¹ʳ = (↑h.unit⁻¹ : M₀)

Tactic:
dif_pos h

Premises used: dif_pos, Ring.inverse
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : ¬IsUnit x
⊢ x⁻¹ʳ = 0

Tactic:
dif_neg h

Premises used: Ring.inverse, dif_neg
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : IsUnit x
rcases : ∀ (u : M₀ˣ), (↑u : M₀) * (↑u : M₀)⁻¹ʳ = 1
⊢ x * x⁻¹ʳ = 1

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u : M₀) * (↑u⁻¹ : M₀) = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := M₀) 1 1
⊢ (↑u : M₀) * (↑u : M₀)⁻¹ʳ = 1

Tactic:
rw [inverse_unit, Units.mul_inv]

Premises used: Units.mul_inv, Ring.inverse_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : IsUnit x
rcases : ∀ (u : M₀ˣ), (↑u : M₀)⁻¹ʳ * (↑u : M₀) = 1
⊢ x⁻¹ʳ * x = 1

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u⁻¹ : M₀) * (↑u : M₀) = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := M₀) 1 1
⊢ (↑u : M₀)⁻¹ʳ * (↑u : M₀) = 1

Tactic:
rw [inverse_unit, Units.inv_mul]

Premises used: Units.inv_mul, Ring.inverse_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x * x⁻¹ʳ) = y
rw₁ : y * 1 = y
rw₂ rw₃ : y = y
⊢ y * x * x⁻¹ʳ = y

Tactic:
rw [mul_assoc, mul_inverse_cancel x h, mul_one]

Premises used: mul_assoc, Ring.mul_inverse_cancel, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x⁻¹ʳ * x) = y
rw₁ : y * 1 = y
rw₂ rw₃ : y = y
⊢ y * x⁻¹ʳ * x = y

Tactic:
rw [mul_assoc, inverse_mul_cancel x h, mul_one]

Premises used: Ring.inverse_mul_cancel, mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x * x⁻¹ʳ * y = y
rw₁ : 1 * y = y
rw₂ rw₃ : y = y
⊢ x * (x⁻¹ʳ * y) = y

Tactic:
rw [← mul_assoc, mul_inverse_cancel x h, one_mul]

Premises used: mul_assoc, Ring.mul_inverse_cancel, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x⁻¹ʳ * x * y = y
rw₁ : 1 * y = y
rw₂ rw₃ : y = y
⊢ x⁻¹ʳ * (x * y) = y

Tactic:
rw [← mul_assoc, inverse_mul_cancel x h, one_mul]

Premises used: Ring.inverse_mul_cancel, mul_assoc, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
rw : y = x * (x⁻¹ʳ * y)
rw₁ rw₂ : y = y
⊢ y = x * z

Tactic:
rw [← h1, mul_inverse_cancel_left _ _ h]

Premises used: Ring.mul_inverse_cancel_left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
rw : x⁻¹ʳ * (x * z) = z
rw₁ rw₂ : z = z
⊢ x⁻¹ʳ * y = z

Tactic:
rw [h1, inverse_mul_cancel_left _ _ h]

Premises used: Ring.inverse_mul_cancel_left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
rw : y * z⁻¹ʳ * z = y
rw₁ rw₂ : y = y
⊢ x * z = y

Tactic:
rw [h1, inverse_mul_cancel_right _ _ h]

Premises used: Ring.inverse_mul_cancel_right
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
rw : x = x * z * z⁻¹ʳ
rw₁ rw₂ : x = x
⊢ x = y * z⁻¹ʳ

Tactic:
rw [← h1, mul_inverse_cancel_right _ _ h]

Premises used: Ring.mul_inverse_cancel_right
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ Eq.{u_2 + 1} (α := M₀) 1⁻¹ʳ 1

Tactic:
inverse_unit 1

Premises used: Ring.inverse_unit, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ Nontrivial M₀

Tactic:
nontriviality
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
h : Nontrivial M₀
⊢ Eq.{u_2 + 1} (α := M₀) 0⁻¹ʳ 0

Tactic:
inverse_non_unit _ not_isUnit_zero

Premises used: not_isUnit_zero, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
h : Nontrivial M₀
⊢ Eq.{u_2 + 1} (α := M₀) 0⁻¹ʳ 0

Tactic:
exact inverse_non_unit _ not_isUnit_zero

Premises used: not_isUnit_zero, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a
obtain : ∀ (u : M₀ˣ), (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)
⊢ a⁻¹ʳ⁻¹ʳ = a

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u⁻¹ : M₀)⁻¹ʳ = (↑u : M₀)
rw₁ : (↑u⁻¹⁻¹ : M₀) = (↑u : M₀)
rw₂ rw₃ : (↑u : M₀) = (↑u : M₀)
⊢ (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)

Tactic:
rw [inverse_unit, inverse_unit, inv_inv]

Premises used: Ring.inverse_unit, inv_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
inl : Subsingleton M₀ → IsUnit a
inr : Nontrivial M₀ → IsUnit a
⊢ IsUnit a

Tactic:
cases subsingleton_or_nontrivial M₀

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h_1 : Subsingleton M₀
⊢ IsUnit a⁻¹ʳ

Tactic:
h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h_1 : Subsingleton M₀
⊢ IsUnit a

Tactic:
convert! h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h_1 : Nontrivial M₀
inr : ∀ (h : ¬IsUnit a), ¬IsUnit a⁻¹ʳ
⊢ IsUnit a

Tactic:
contrapose h