awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h : ∀ (i : DistribMulAction N α), SMulCommClass M N α = SMulCommClass M N α
⊢ Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
    fun (x : DistribMulAction N α) ↦ SMulCommClass M N α

Tactic:
funext i
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
i : DistribMulAction N α
h : compHom (M := M × N) α (MonoidHom.inl M N) = fst
⊢ SMulCommClass M N α = SMulCommClass M N α

Tactic:
congr
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
i : DistribMulAction N α
h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = fst

Tactic:
ext m a
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h : ∀ (n : N) (a : α), SMul.smul n a = SMul.smul n a
⊢ compHom (M := M × N) α (MonoidHom.inr M N) = x

Tactic:
ext n a
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
n : N
a : α
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (SMul.smul n a)
| SMul.smul n a

Tactic:
rw [← one_smul M (SMul.smul n a)]

Premises used: one_smul, SMul.smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
n : N
a : α
h : SMul.smul n a = HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (SMul.smul n a)
⊢ SMul.smul n a = SMul.smul n a

Tactic:
conv_rhs => rw [← one_smul M (SMul.smul n a)]

Premises used: one_smul, SMul.smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (SMul.smul n a)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ HEq (α := SMulCommClass M N α) ⋯ snd

Tactic:
proof_irrel_heq ..

Premises used: proof_irrel_heq
-- Module: Mathlib.Algebra.GroupWithZero.Action.Prod
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ HEq (α := SMulCommClass M N α) ⋯ snd

Tactic:
exact proof_irrel_heq ..

Premises used: proof_irrel_heq
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : Zero B
inst_1 : SMulZeroClass M B
this : Zero A := e.zero
⊢ ∀ (a : M), HSMul.hSMul (β := A) a 0 = 0

Tactic:
simp [smul_def, zero_def]

Premises used: Equiv.zero_def, Equiv.smul_def
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : Zero B
inst_1 : SMulZeroClass M B
this : Zero A := e.zero
⊢ SMulZeroClass M A

Tactic:
exact {
    e.smul M with
    smul_zero := by simp [smul_def, zero_def]
  }

Premises used: Equiv.smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : Zero M₀
inst_1 : Zero B
inst_2 : SMulWithZero M₀ B
this : Zero A := e.zero
⊢ ∀ (m : A), HSMul.hSMul.{u_2, u_3, u_3} (α := M₀) 0 m = 0

Tactic:
simp [smul_def, zero_def]

Premises used: Equiv.zero_def, Equiv.smul_def
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : Zero M₀
inst_1 : Zero B
inst_2 : SMulWithZero M₀ B
this : Zero A := e.zero
⊢ SMulWithZero M₀ A

Tactic:
exact {
    e.smulZeroClass M₀ with
    zero_smul := by simp [smul_def, zero_def]
  }

Premises used: Equiv.smulZeroClass
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : MonoidWithZero M₀
inst_1 : Zero B
inst_2 : MulActionWithZero M₀ B
this : Zero A := e.zero
⊢ MulActionWithZero M₀ A

Tactic:
exact { e.smulWithZero M₀, e.mulAction M₀ with }

Premises used: Equiv.smulWithZero, Equiv.mulAction
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : AddZeroClass B
inst_1 : DistribSMul M B
this : AddZeroClass A := e.addZeroClass
⊢ ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

Tactic:
simp [add_def, smul_def, smul_add]

Premises used: Equiv.add_def, Equiv.smul_def, smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : AddZeroClass B
inst_1 : DistribSMul M B
this : AddZeroClass A := e.addZeroClass
⊢ DistribSMul M A

Tactic:
exact {
    e.smulZeroClass M with
    smul_add := by simp [add_def, smul_def, smul_add]
  }

Premises used: Equiv.smulZeroClass
-- Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance
Goal:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst : Monoid M
inst_1 : AddMonoid B
inst_2 : DistribMulAction M B
this : AddMonoid A := e.addMonoid
⊢ DistribMulAction M A

Tactic:
exact { e.distribSMul M, e.mulAction M with }

Premises used: Equiv.distribSMul, Equiv.mulAction
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
α : Type u_6
inst_1 : SMul G₀ α
g : G₀
hg : g ≠ 0
a : α
⊢ mk0 g hg • a = g • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
x : β
⊢ a⁻¹ • a • x = x

Tactic:
inv_smul_smul (Units.mk0 a ha) x

Premises used: inv_smul_smul, Units.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
x : β
⊢ a • a⁻¹ • x = x

Tactic:
smul_inv_smul (Units.mk0 a ha) x

Premises used: smul_inv_smul, Units.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
x y : β
⊢ a⁻¹ • x = y ↔ x = a • y

Tactic:
inv_smul_eq_iff (g := Units.mk0 a ha)

Premises used: inv_smul_eq_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
x y : β
⊢ x = a⁻¹ • y ↔ a • x = y

Tactic:
eq_inv_smul_iff (g := Units.mk0 a ha)

Premises used: eq_inv_smul_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
inst_2 : Mul β
inst_3 : SMulCommClass α β β
inst_4 : IsScalarTower α β β
x y z : β
ha : a ≠ 0
⊢ SemiconjBy x (a • y) (a • z) ↔ SemiconjBy x y z

Tactic:
smul_right_iff (r := Units.mk0 a ha)

Premises used: SemiconjBy.smul_right_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
inst_2 : Mul β
inst_3 : SMulCommClass α β β
inst_4 : IsScalarTower α β β
x y z : β
ha : a ≠ 0
⊢ SemiconjBy (a • x) y z ↔ SemiconjBy x y z

Tactic:
smul_left_iff (r := Units.mk0 a ha)

Premises used: SemiconjBy.smul_left_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
inst_2 : Mul β
inst_3 : SMulCommClass α β β
inst_4 : IsScalarTower α β β
x y : β
ha : a ≠ 0
⊢ Commute x (a • y) ↔ Commute x y

Tactic:
SemiconjBy.smul_right_iff₀ ha

Premises used: Commute, SemiconjBy.smul_right_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
α : Type u_4
β : Type u_5
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
inst_2 : Mul β
inst_3 : SMulCommClass α β β
inst_4 : IsScalarTower α β β
x y : β
ha : a ≠ 0
⊢ Commute (a • x) y ↔ Commute x y

Tactic:
SemiconjBy.smul_left_iff₀ ha

Premises used: Commute, SemiconjBy.smul_left_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Units
Goal:
G : Type u_2
M : Type u_3
inst : Monoid G
inst_1 : AddMonoid M
inst_2 : DistribMulAction G M
u : G
x : M
hu : IsUnit u
⊢ u • x = 0 ↔ x = 0

Tactic:
smul_eq_zero_iff_eq hu.unit

Premises used: smul_eq_zero_iff_eq, IsUnit.unit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ x * (↑1 : M) = x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ x ~ᵤ x

Tactic:
.refl x

Premises used: Associated.refl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Std.Refl.{u_1 + 1} (α := M) Associated

Tactic:
⟨Associated.refl⟩

Premises used: Std.Refl.mk, Associated.refl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x : M
u : Mˣ
rw : x * ((↑u : M) * (↑u⁻¹ : M)) = x
rw₁ : x * 1 = x
rw₂ rw₃ : x = x
⊢ x * (↑u : M) * (↑u⁻¹ : M) = x

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

Premises used: mul_assoc, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Std.Symm.{u_1 + 1} (α := M) Associated

Tactic:
⟨fun _ _ => Associated.symm⟩

Premises used: Std.Symm.mk, Associated.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
⊢ x ~ᵤ y ↔ y ~ᵤ x

Tactic:
⟨Associated.symm, Associated.symm⟩

Premises used: Associated.symm, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x : M
u v : Mˣ
rw : x * ((↑u : M) * (↑v : M)) = x * (↑u : M) * (↑v : M)
rw₁ rw₂ : x * ((↑u : M) * (↑v : M)) = x * ((↑u : M) * (↑v : M))
⊢ x * (↑(u * v) : M) = x * (↑u : M) * (↑v : M)

Tactic:
rw [Units.val_mul, mul_assoc]

Premises used: mul_assoc, Units.val_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ IsTrans M Associated

Tactic:
⟨fun _ _ _ => Associated.trans⟩

Premises used: IsTrans.mk, Associated.trans
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
ha : x ~ᵤ y
obtain :
  ∀ (u : Mˣ) (ha : x * (↑u : M) = y), Associated.{u_3} (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Associated.{u_3} (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
obtain ⟨u, ha⟩ := ha
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) (x * (↑u : M))
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
rw₂ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) (((↑f : M →* N) : (a : M) → N) (↑u : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
rw₃ rw₄ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) y

Tactic:
rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]

Premises used: Units.coe_map, MonoidHom.coe_coe, map_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
⊢ Associated.{u_3} (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a = b
rwa : a * 1 = b
rwa₁ rwa₂ rwa₃ rwa₄ : a = b
⊢ a * (↑1 : M) = b

Tactic:
rwa [Units.val_one, mul_one]

Premises used: Units.val_one, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
⊢ (↑u : M) ~ᵤ 1

Tactic:
⟨u⁻¹, Units.mul_inv u⟩

Premises used: Units.mul_inv, Associated, Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : M
h_1 : IsUnit a
c : Mˣ
h : (↑c : M) = a
⊢ 1 * (↑c : M) = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
h : a ~ᵤ 0
let : ∀ (u : Mˣ) (h : 0 * (↑u : M) = a), a = 0
⊢ a = 0

Tactic:
let ⟨u, h⟩ := h.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
h_1 : a ~ᵤ 0
u : Mˣ
h : 0 * (↑u : M) = a
⊢ a = 0

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
hab : a * b = 1
⊢ a ~ᵤ 1

Tactic:
show (Units.mkOfMulEqOne a b hab : M) ~ᵤ 1 from unit_associated_one

Premises used: unit_associated_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
u : Mˣ
h : a * b * (↑u : M) = 1
⊢ a * (b * (↑u : M)) = 1

Tactic:
simpa [mul_assoc] using h

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
let ⟨u', hu⟩ := hu
  ⟨u'⁻¹, hu ▸ Units.mul_inv_cancel_right _ _⟩

Premises used: HMul.hMul, Eq.rec, Units.mul_inv_cancel_right, _private.0.associated_one_iff_isUnit.match_2, Associated, Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a u : N
hu : IsUnit u
rw : a * u ~ᵤ a
⊢ u * a ~ᵤ a

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
associated_mul_unit_left _ _ hu

Premises used: associated_mul_unit_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
exact associated_mul_unit_left _ _ hu

Premises used: associated_mul_unit_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a u : N
hu : IsUnit u
⊢ a ~ᵤ a * u

Tactic:
(associated_mul_unit_left a u hu).symm

Premises used: Associated.symm, associated_mul_unit_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a u : N
hu : IsUnit u
⊢ a ~ᵤ u * a

Tactic:
(associated_unit_mul_left a u hu).symm

Premises used: Associated.symm, associated_unit_mul_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a u b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b

Tactic:
⟨(associated_mul_unit_right _ _ hu).trans, (associated_mul_unit_left _ _ hu).trans⟩

Premises used: Associated.trans, associated_mul_unit_left, associated_mul_unit_right, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
u a b : N
hu : IsUnit u
rw : a * u ~ᵤ b ↔ a ~ᵤ b
⊢ u * a ~ᵤ b ↔ a ~ᵤ b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b

Tactic:
associated_mul_isUnit_left_iff hu

Premises used: associated_mul_isUnit_left_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b

Tactic:
exact associated_mul_isUnit_left_iff hu

Premises used: associated_mul_isUnit_left_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a b u : N
hu : IsUnit u
⊢ a ~ᵤ b * u ↔ a ~ᵤ b

Tactic:
Associated.comm.trans <| (associated_mul_isUnit_left_iff hu).trans Associated.comm

Premises used: Associated.comm, associated_mul_isUnit_left_iff, Iff.trans
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a u b : N
hu : IsUnit u
⊢ a ~ᵤ u * b ↔ a ~ᵤ b

Tactic:
Associated.comm.trans <| (associated_isUnit_mul_left_iff hu).trans Associated.comm

Premises used: Associated.comm, associated_isUnit_mul_left_iff, Iff.trans
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a b : N
u : Nˣ
⊢ a * (↑u : N) ~ᵤ b ↔ a ~ᵤ b

Tactic:
associated_mul_isUnit_left_iff u.isUnit

Premises used: associated_mul_isUnit_left_iff, Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a b : N
u : Nˣ
⊢ (↑u : N) * a ~ᵤ b ↔ a ~ᵤ b

Tactic:
associated_isUnit_mul_left_iff u.isUnit

Premises used: associated_isUnit_mul_left_iff, Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : Monoid N
a b : N
u : Nˣ
⊢ a ~ᵤ b * (↑u : N) ↔ a ~ᵤ b

Tactic:
associated_mul_isUnit_right_iff u.isUnit

Premises used: associated_mul_isUnit_right_iff, Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
N : Type u_2
inst : CommMonoid N
a b : N
u : Nˣ
⊢ a ~ᵤ (↑u : N) * b ↔ a ~ᵤ b

Tactic:
associated_isUnit_mul_right_iff u.isUnit

Premises used: Units.isUnit, associated_isUnit_mul_right_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : b ~ᵤ c
obtain : ∀ (d : Mˣ), a * b ~ᵤ a * (b * (↑d : M))
⊢ a * b ~ᵤ a * c

Tactic:
obtain ⟨d, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * (↑d : M))

Tactic:
⟨d, mul_assoc _ _ _⟩

Premises used: mul_assoc, Associated, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * (↑d : M))

Tactic:
exact ⟨d, mul_assoc _ _ _⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
obtain : ∀ (d : Mˣ), a * c ~ᵤ a * (↑d : M) * c
⊢ a * c ~ᵤ b * c

Tactic:
obtain ⟨d, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * (↑d : M) * c

Tactic:
⟨d, mul_right_comm _ _ _⟩

Premises used: Associated, mul_right_comm, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * (↑d : M) * c

Tactic:
exact ⟨d, mul_right_comm _ _ _⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a₁ a₂ b₁ b₂ : M
h₁ : a₁ ~ᵤ b₁
h₂ : a₂ ~ᵤ b₂
⊢ a₁ * a₂ ~ᵤ b₁ * b₂

Tactic:
(h₁.mul_right _).trans (h₂.mul_left _)

Premises used: Associated.trans, Associated.mul_left, Associated.mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
⊢ HPow.hPow (β := ℕ) a 0 ~ᵤ HPow.hPow (β := ℕ) b 0

Tactic:
simp [Associated.refl]

Premises used: Associated.refl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a * a ^ n ~ᵤ b * b ^ n

Tactic:
h.mul_mul ih

Premises used: Associated.mul_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
h₁ : a ^ (n + 1) = a * a ^ n
h₂ : b ^ (n + 1) = b * b ^ n
⊢ a ^ (n + 1) ~ᵤ b ^ (n + 1)

Tactic:
convert! h.mul_mul ih

Premises used: Associated.mul_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
h₁ h₂ : a * a ^ n = a * a ^ n
⊢ a ^ (n + 1) = a * a ^ n

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
h₁ h₂ : b * b ^ n = b * b ^ n
⊢ b ^ (n + 1) = b * b ^ n

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
n : ℕ
h : a ~ᵤ b
zero : HPow.hPow (β := ℕ) a 0 ~ᵤ HPow.hPow (β := ℕ) b 0
succ : ∀ (n : ℕ) (ih : a ^ n ~ᵤ b ^ n), a ^ (n + 1) ~ᵤ b ^ (n + 1)
⊢ a ^ n ~ᵤ b ^ n

Tactic:
induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert! h.mul_mul ih <;> rw [pow_succ']

Premises used: Associated.refl, pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
⊢ a ~ᵤ b → a ∣ b

Tactic:
fun ⟨u, hu⟩ =>
  ⟨u, hu.symm⟩

Premises used: Units.val, Dvd.dvd, _private.0.Associated.dvd.match_1, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a ~ᵤ b
⊢ b ∣ a

Tactic:
h.symm.dvd

Premises used: Associated.dvd, Associated.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a

Tactic:
⟨h.dvd, h.symm.dvd⟩

Premises used: Associated.dvd, Associated.symm, And.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a b : M
hab : a ∣ b
hba : b ∣ a
rcases : ∀ (c : M) (hba : a * c ∣ a), a ~ᵤ a * c
⊢ a ~ᵤ b

Tactic:
rcases hab with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c : M
hba : a * c ∣ a
rcases : ∀ (d : M) (a_eq : a = a * c * d), a ~ᵤ a * c
⊢ a ~ᵤ a * c

Tactic:
rcases hba with ⟨d, a_eq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
pos : ∀ (ha0 : a = 0), a ~ᵤ a * c
neg : ∀ (ha0 : ¬a = 0), a ~ᵤ a * c
⊢ a ~ᵤ a * c

Tactic:
by_cases ha0 : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
⊢ a = 0

Tactic:
rw [con, zero_mul] at a_eq

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
a_eq₁ : a = 0
⊢ ¬a = 0

Tactic:
rw [con, zero_mul] at a_eq

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
a_eq₁ : a = 0
ha0₁ : ¬a = 0
⊢ a * c = 0

Tactic:
rw [con, zero_mul] at a_eq

Premises used: MulZeroClass.zero_mul