awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
refine_1 : ∀ (he : (a0, b0) = (a1, b1)), False
refine_2 : UniqueMul A B (a1, b1).1 (a1, b1).2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : (a0, b0) = (a1, b1)
⊢ a0 = a1 ∧ b0 = b1

Tactic:
rw [Prod.mk_inj] at he

Premises used: Prod.mk_inj
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
refine_1 :
  ∀ (ha1 : a1 ∈ A) (b1 : G) (he0 : (A * B).min' ⋯ = (A * B).max' ⋯) (hb1 : b1 ∈ B) (he1 : a1 * b1 = (A * B).min' ⋯)
    (this : UniqueMul A B a0 b0) (he : a0 = a1 ∧ b0 = b1), False
⊢ False

Tactic:
rw [he.1, he.2, he1] at he0

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
refine_1 : ∀ (a2 b2 : G) (h2 : (a2, b2) ∈ A ×ˢ B) (hne : (a2, b2) ≠ (a0, b0)), False
⊢ False

Tactic:
obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)

Premises used: Prod.mk, Finset.exists_mem_ne
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2) ∈ A ×ˢ B
hne : (a2, b2) ≠ (a0, b0)
⊢ (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B

Tactic:
rw [mem_product] at h2

Premises used: Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2) ∈ A ×ˢ B
hne : (a2, b2) ≠ (a0, b0)
h2₁ : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
⊢ (a2, b2) ≠ (a0, b0)

Tactic:
rw [mem_product] at h2

Premises used: Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
⊢ False

Tactic:
(min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0

Premises used: Finset.min'_lt_max', And.right, And.left, LT.lt.ne, Finset.mul_mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
refine_1 : ∀ (he : a0 * b0 = (a2, b2).1 * (a2, b2).2), (a2, b2) = (a0, b0)
⊢ False

Tactic:
refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0

Premises used: Finset.min'_lt_max', And.right, And.left, LT.lt.ne, Finset.mul_mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he_1 : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
he : a0 * b0 = (a2, b2).1 * (a2, b2).2
⊢ (a2, b2) = (a0, b0)

Tactic:
Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)

Premises used: Iff.mpr, Prod.ext_iff, And.right, And.left, Eq.symm
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he_1 : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
he : a0 * b0 = (a2, b2).1 * (a2, b2).2
⊢ (a2, b2) = (a0, b0)

Tactic:
exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)

Premises used: Iff.mpr, Prod.ext_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
refine_2 : ∀ (hl : b < b1), a = (a1, b1).1 ∧ b = (a1, b1).2
refine_2₁ :
  ∀ (hb1 : b ∈ B) (he1 : a1 * b = (A * B).min' ⋯) (he : a * b = (a1, b).1 * (a1, b).2), a = (a1, b).1 ∧ b = (a1, b).2
refine_2₂ : ∀ (hl : b1 < b), a = (a1, b1).1 ∧ b = (a1, b1).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
obtain hl | rfl | hl := lt_trichotomy b b1

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b < b1
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
exact ((he1 ▸ mul_lt_mul_right hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb hb1 : b ∈ B
he1 : a1 * b = (A * B).min' ⋯
he : a * b = (a1, b).1 * (a1, b).2
⊢ a = (a1, b).1 ∧ b = (a1, b).2

Tactic:
⟨mul_right_cancel he, rfl⟩

Premises used: And.intro, mul_right_cancel, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb hb1 : b ∈ B
he1 : a1 * b = (A * B).min' ⋯
he : a * b = (a1, b).1 * (a1, b).2
⊢ a = (a1, b).1 ∧ b = (a1, b).2

Tactic:
exact ⟨mul_right_cancel he, rfl⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b1 < b
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
exact ((he1 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsLeftCancelMul G
inst_3 : LinearOrder G
inst_4 : MulRightStrictMono G
⊢ TwoUniqueProds G

Tactic:
let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective
  let _ : MulLeftStrictMono Gᵐᵒᵖ :=
    { elim := fun _ _ _ bc ↦ mul_lt_mul_left (α := G) bc (unop _) }
  of_mulOpposite of_covariant_right

Premises used: CovariantClass.mk, TwoUniqueProds.of_covariant_right, LinearOrder.lift', TwoUniqueProds.of_mulOpposite, mul_lt_mul_left, MulOpposite.unop, MulOpposite.unop_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_2
G : ι → Type u_1
inst_2 : (i : ι) → AddZeroClass (G i)
inst_3 : ∀ (i : ι), TwoUniqueSums.{u_1} (G i)
⊢ TwoUniqueSums (Π₀ (i : ι), G i)

Tactic:
TwoUniqueSums.of_injective_addHom
    DFinsupp.coeFnAddMonoidHom.toAddHom DFunLike.coe_injective inferInstance

Premises used: AddMonoidHom.toAddHom, inferInstance, DFinsupp.coeFnAddMonoidHom, DFunLike.coe_injective, TwoUniqueSums.of_injective_addHom
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_1
G : Type u_2
inst_2 : AddZeroClass G
inst_3 : TwoUniqueSums G
⊢ TwoUniqueSums (ι →₀ G)

Tactic:
TwoUniqueSums.of_injective_addHom
    Finsupp.coeFnAddHom.toAddHom DFunLike.coe_injective inferInstance

Premises used: AddMonoidHom.toAddHom, inferInstance, Finsupp.coeFnAddHom, DFunLike.coe_injective, TwoUniqueSums.of_injective_addHom
-- Module: Mathlib.Algebra.Group.UniqueProds.VectorSpace
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Module ℚ G
⊢ TwoUniqueSums G

Tactic:
TwoUniqueSums.of_injective_addHom _ (Module.Basis.ofVectorSpace ℚ G).repr.injective inferInstance

Premises used: Rat, inferInstance, Module.Basis.repr, Module.Basis.ofVectorSpace, TwoUniqueSums.of_injective_addHom, LinearEquiv.injective
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u_1
inst : Unique α
inst_1 : One α
⊢ Eq.{u_1 + 1} (α := α) default 1

Tactic:
Unique.default_eq 1

Premises used: Unique.default_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b : α) * (↑b⁻¹ : α)) = a
rw₁ : a * 1 = a
rw₂ rw₃ : a = a
⊢ a * (↑b : α) * (↑b⁻¹ : α) = a

Tactic:
rw [mul_assoc, mul_inv, mul_one]

Premises used: mul_assoc, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b⁻¹ : α) * (↑b : α)) = a
rw₁ : a * 1 = a
rw₂ rw₃ : a = a
⊢ a * (↑b⁻¹ : α) * (↑b : α) = a

Tactic:
rw [mul_assoc, inv_mul, mul_one]

Premises used: mul_assoc, Units.inv_mul, mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : (↑a : α) * b = (↑a : α) * c
⊢ b = c

Tactic:
simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h

Premises used: HMul.hMul, congr_arg, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
a : αˣ
b c : α
h : b * (↑a : α) = c * (↑a : α)
⊢ b = c

Tactic:
simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h

Premises used: HMul.hMul, Units.mul_inv_cancel_right, congr_arg
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a = b * (↑c⁻¹ : α)
rw : b * (↑c⁻¹ : α) * (↑c : α) = b
rw₁ rw₂ : b = b
⊢ a * (↑c : α) = b

Tactic:
rw [h, inv_mul_cancel_right]

Premises used: Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a * (↑c : α) = b
rw : a = a * (↑c : α) * (↑c⁻¹ : α)
rw₁ rw₂ : a = a
⊢ a = b * (↑c⁻¹ : α)

Tactic:
rw [← h, mul_inv_cancel_right]

Premises used: Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = (↑b⁻¹ : α) * c
rw : (↑b : α) * ((↑b⁻¹ : α) * c) = c
rw₁ rw₂ : c = c
⊢ (↑b : α) * a = c

Tactic:
rw [h, mul_inv_cancel_left]

Premises used: Units.mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : (↑b : α) * a = c
rw : a = (↑b⁻¹ : α) * ((↑b : α) * a)
rw₁ rw₂ : a = a
⊢ a = (↑b⁻¹ : α) * c

Tactic:
rw [← h, inv_mul_cancel_left]

Premises used: Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a * (↑b⁻¹ : α) = c
rw : a = a * (↑b⁻¹ : α) * (↑b : α)
rw₁ rw₂ : a = a
⊢ a = c * (↑b : α)

Tactic:
rw [← h, inv_mul_cancel_right]

Premises used: Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = c * (↑b : α)
rw : c * (↑b : α) * (↑b⁻¹ : α) = c
rw₁ rw₂ : c = c
⊢ a * (↑b⁻¹ : α) = c

Tactic:
rw [h, mul_inv_cancel_right]

Premises used: Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
rw rw₁ : (↑u⁻¹ : α) = (↑u⁻¹ : α)
⊢ (↑u⁻¹ : α) = 1 * (↑u⁻¹ : α)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
rw : a * (↑u : α) * (↑u⁻¹ : α) = a
rw₁ rw₂ : a = a
⊢ 1 * (↑u⁻¹ : α) = a

Tactic:
rw [← h, mul_inv_cancel_right]

Premises used: Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
rw rw₁ : (↑u⁻¹ : α) = (↑u⁻¹ : α)
⊢ (↑u⁻¹ : α) = (↑u⁻¹ : α) * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
rw : (↑u⁻¹ : α) * ((↑u : α) * a) = a
rw₁ rw₂ : a = a
⊢ (↑u⁻¹ : α) * 1 = a

Tactic:
rw [← h, inv_mul_cancel_left]

Premises used: Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
⊢ a = (↑u⁻¹ : α)

Tactic:
(Units.inv_eq_of_mul_eq_one_right h).symm

Premises used: Units.inv_eq_of_mul_eq_one_right, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
⊢ a = (↑u⁻¹ : α)

Tactic:
(Units.inv_eq_of_mul_eq_one_left h).symm

Premises used: Units.inv_eq_of_mul_eq_one_left, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
⊢ a * (↑u⁻¹ : α) = 1 ↔ a = (↑u : α)

Tactic:
⟨inv_inv u ▸ Units.eq_inv_of_mul_eq_one_right, fun h => mul_inv_of_eq h.symm⟩

Premises used: Units.mul_inv_of_eq, Eq.rec, Units.eq_inv_of_mul_eq_one_right, inv_inv, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
⊢ (↑u⁻¹ : α) * a = 1 ↔ (↑u : α) = a

Tactic:
⟨inv_inv u ▸ Units.inv_eq_of_mul_eq_one_right, inv_mul_of_eq⟩

Premises used: Units.inv_eq_of_mul_eq_one_right, Eq.rec, inv_inv, Units.inv_mul_of_eq, Iff.intro
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
rw : a * (↑u : α) = 1 ↔ a * (↑u⁻¹⁻¹ : α) = 1
rw₁ rw₂ : a * (↑u : α) = 1 ↔ a * (↑u : α) = 1
⊢ a * (↑u : α) = 1 ↔ a = (↑u⁻¹ : α)

Tactic:
rw [← mul_inv_eq_one, inv_inv]

Premises used: Units.mul_inv_eq_one, inv_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
rw : (↑u : α) * a = 1 ↔ (↑u⁻¹⁻¹ : α) * a = 1
rw₁ rw₂ : (↑u : α) * a = 1 ↔ (↑u : α) * a = 1
⊢ (↑u : α) * a = 1 ↔ (↑u⁻¹ : α) = a

Tactic:
rw [← inv_mul_eq_one, inv_inv]

Premises used: Units.inv_mul_eq_one, inv_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
h : (↑u₁ : α) = (↑u₂ : α)
rw : (↑u₂ : α) * (↑u₂⁻¹ : α) = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ (↑u₁ : α) * (↑u₂⁻¹ : α) = 1

Tactic:
rw [h, u₂.mul_inv]

Premises used: Units.mul_inv
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
⊢ (↑u₁⁻¹ : α) = (↑u₂⁻¹ : α) ↔ (↑u₁ : α) = (↑u₂ : α)

Tactic:
Units.ext_iff.symm.trans <| inv_inj.trans Units.ext_iff

Premises used: Units.ext_iff, inv_inj, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a = (↑d⁻¹ : α) * c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
rw₂ : a = (↑d⁻¹ : α) * (c * (↑b : α)) ↔ a * (↑d : α) = c * (↑b : α)
rw₃ : (↑d : α) * a = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
rw₄ rw₅ : a * (↑d : α) = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)

Tactic:
rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]

Premises used: mul_assoc, Units.mul_inv_eq_iff_eq_mul, mul_comm, Units.eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
rw₂ rw₃ : a * (↑d : α) = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
⊢ (↑b⁻¹ : α) * a = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)

Tactic:
rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]

Premises used: Units.mul_inv_eq_mul_inv_iff, mul_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
a b : α
⊢ a /ₚ u = b /ₚ u ↔ a = b

Tactic:
Units.mul_left_inj _

Premises used: divp, Units.mul_left_inj
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
rw : x = y * (↑u : α) ↔ y * (↑u : α) = x
⊢ x /ₚ u * (↑u : α) = y * (↑u : α) ↔ y * (↑u : α) = x

Tactic:
rw [divp_mul_cancel]

Premises used: divp_mul_cancel
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
⊢ x = y * (↑u : α) ↔ y * (↑u : α) = x

Tactic:
⟨Eq.symm, Eq.symm⟩

Premises used: Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
⊢ x = y * (↑u : α) ↔ y * (↑u : α) = x

Tactic:
exact ⟨Eq.symm, Eq.symm⟩
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
rw : y /ₚ u = x ↔ x * (↑u : α) = y
rw₁ rw₂ : x * (↑u : α) = y ↔ x * (↑u : α) = y
⊢ x = y /ₚ u ↔ x * (↑u : α) = y

Tactic:
rw [eq_comm, divp_eq_iff_mul_eq]

Premises used: divp_eq_iff_mul_eq, eq_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a = 1 * (↑u : α) ↔ a = (↑u : α)
rw₁ rw₂ : a = (↑u : α) ↔ a = (↑u : α)
⊢ a /ₚ u * (↑u : α) = 1 * (↑u : α) ↔ a = (↑u : α)

Tactic:
rw [divp_mul_cancel, one_mul]

Premises used: divp_mul_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : Monoid α
u : αˣ
rw : (↑u⁻¹ : α) = 1 /ₚ u
rw₁ rw₂ : (↑u⁻¹ : α) = (↑u⁻¹ : α)
⊢ (↑(1 / u) : α) = 1 /ₚ u

Tactic:
rw [one_div, one_divp]

Premises used: one_divp, one_div
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : a * (b * a) = a * 1
rw₁ : a * b * a = a * 1
rw₂ : 1 * a = a * 1
rw₃ : a = a * 1
rw₄ rw₅ : a = a
⊢ b * a = 1

Tactic:
rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]

Premises used: mul_assoc, mul_one, mul_left_cancel_iff, one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rwa : ∀ (h : 1 * b = 1), b = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : b = 1), b = 1
⊢ b = 1

Tactic:
rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h

Premises used: LeftCancelMonoid.eq_one_of_mul_right, one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Premises used: not_iff_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : b * a * b = 1 * b
rw₁ : b * (a * b) = 1 * b
rw₂ : b * 1 = 1 * b
rw₃ : b * 1 = b
rw₄ rw₅ : b = b
⊢ b * a = 1

Tactic:
rw [← mul_right_cancel_iff (a := b), mul_assoc, h, one_mul, mul_one]

Premises used: mul_assoc, mul_right_cancel_iff, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rwa : ∀ (h : 1 * b = 1), b = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : b = 1), b = 1
⊢ b = 1

Tactic:
rwa [RightCancelMonoid.eq_one_of_mul_right h, one_mul] at h

Premises used: RightCancelMonoid.eq_one_of_mul_right, one_mul
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
rw : ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Premises used: not_iff_comm
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : RightCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Basic
Goal:
α : Type u
inst : CancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ a = 1

Tactic:
LeftCancelMonoid.eq_one_of_mul_right h

Premises used: LeftCancelMonoid.eq_one_of_mul_right