awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
a : M
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x y : M
⊢ SemiconjBy.{u_3} (M := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
    SemiconjBy a x y

Tactic:
⟨.of_map hf, (.map · f)⟩

Premises used: SemiconjBy.of_map, SemiconjBy.map, Iff.intro
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x y : M
⊢ Commute.{u_3} (S := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔ Commute x y

Tactic:
⟨.of_map hf, (.map · f)⟩

Premises used: Commute.of_map, Iff.intro, Commute.map
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
⊢ Commute a (↑u : M) → Commute a (↑u⁻¹ : M)

Tactic:
SemiconjBy.units_inv_right

Premises used: Commute, SemiconjBy.units_inv_right
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
⊢ Commute a (↑u⁻¹ : M) ↔ Commute a (↑u : M)

Tactic:
SemiconjBy.units_inv_right_iff

Premises used: Commute, SemiconjBy.units_inv_right_iff
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
⊢ Commute (↑u : M) a → Commute (↑u⁻¹ : M) a

Tactic:
SemiconjBy.units_inv_symm_left

Premises used: Commute, SemiconjBy.units_inv_symm_left
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
⊢ Commute (↑u⁻¹ : M) a ↔ Commute (↑u : M) a

Tactic:
SemiconjBy.units_inv_symm_left_iff

Premises used: Commute, SemiconjBy.units_inv_symm_left_iff
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u₁ u₂ : Mˣ
⊢ Commute u₁ u₂ → Commute (↑u₁ : M) (↑u₂ : M)

Tactic:
SemiconjBy.units_val

Premises used: Commute, SemiconjBy.units_val
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u₁ u₂ : Mˣ
⊢ Commute (↑u₁ : M) (↑u₂ : M) → Commute u₁ u₂

Tactic:
SemiconjBy.units_of_val

Premises used: Commute, SemiconjBy.units_of_val
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u₁ u₂ : Mˣ
⊢ Commute (↑u₁ : M) (↑u₂ : M) ↔ Commute u₁ u₂

Tactic:
SemiconjBy.units_val_iff

Premises used: Commute, SemiconjBy.units_val_iff
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
rw : a * b * (↑u⁻¹ : M) = 1
rw₁ : (↑u : M) * (↑u⁻¹ : M) = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := M) 1 1
⊢ a * (b * (↑u⁻¹ : M)) = 1

Tactic:
rw [← mul_assoc, hu, u.mul_inv]

Premises used: mul_assoc, Units.mul_inv
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
⊢ Commute a (↑u : M)

Tactic:
have : Commute a u := hu ▸ (Commute.refl _).mul_right hc
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a_1 b_1 : M
u_1 u₁ u₂ u : Mˣ
a b : M
hu : a * b = (↑u : M)
hc : Commute a b
this : Commute a (↑u : M)
rw : b * a * (↑u⁻¹ : M) = 1
rw₁ : a * b * (↑u⁻¹ : M) = 1
rw₂ : (↑u : M) * (↑u⁻¹ : M) = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := M) 1 1
⊢ b * (↑u⁻¹ : M) * a = 1

Tactic:
rw [← this.units_inv_right.right_comm, ← hc.eq, hu, u.mul_inv]

Premises used: Units.mul_inv, Commute.units_inv_right, Commute.right_comm, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : Commute a b
⊢ IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b

Tactic:
⟨fun ⟨u, hu⟩ => ⟨(u.leftOfMul a b hu.symm h).isUnit, (u.rightOfMul a b hu.symm h).isUnit⟩,
  fun H => H.1.mul H.2⟩

Premises used: IsUnit, IsUnit.mul, And, And.right, _private.0.Commute.isUnit_mul_iff.match_1, And.left, And.intro, Units.leftOfMul, Iff.intro, Units.isUnit, Units.rightOfMul, Eq.symm
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ IsUnit (a * a) ↔ IsUnit a

Tactic:
(Commute.refl a).isUnit_mul_iff.trans and_self_iff

Premises used: Commute.refl, Commute.isUnit_mul_iff, Iff.trans, and_self_iff
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : Commute a (↑u : M)
m : ℤ
⊢ Commute a (↑(u ^ m) : M)

Tactic:
SemiconjBy.units_zpow_right h m

Premises used: Commute, SemiconjBy.units_zpow_right
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
u : Mˣ
h : Commute (↑u : M) a
m : ℤ
⊢ Commute (↑(u ^ m) : M) a

Tactic:
(h.symm.units_zpow_right m).symm

Premises used: Commute.units_zpow_right, Commute.symm
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n_1 : ℕ
a b : M
u_1 u₁ u₂ u : Mˣ
x : M
n : ℕ
hn : n ≠ 0
hu : x ^ n = (↑u : M)
rwa : x ^ (n - 1 + 1) = (↑u : M)
rwa₁ rwa₂ rwa₃ rwa₄ : x ^ n = (↑u : M)
⊢ x * x ^ (n - 1) = (↑u : M)

Tactic:
rwa [← _root_.pow_succ', Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)]

Premises used: Nat.succ_le_of_lt, Nat.pos_of_ne_zero, Nat.sub_add_cancel, pow_succ'
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a : M
hn : n ≠ 0
⊢ IsUnit (a ^ n) ↔ IsUnit a

Tactic:
⟨fun ⟨u, hu⟩ ↦ (u.ofPow a hn hu.symm).isUnit, IsUnit.pow n⟩

Premises used: IsUnit, Units.ofPow, _private.0.isUnit_pow_iff.match_1, IsUnit.pow, Iff.intro, Units.isUnit, Eq.symm
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a : M
⊢ IsUnit (a ^ (n + 1)) ↔ IsUnit a

Tactic:
isUnit_pow_iff n.succ_ne_zero

Premises used: isUnit_pow_iff, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
zero : IsUnit (HPow.hPow (β := ℕ) a 0) ↔ Eq (α := ℕ) 0 0
succ : ∀ (n : ℕ), IsUnit (a ^ (n + 1)) ↔ n + 1 = 0
⊢ IsUnit (a ^ n) ↔ n = 0

Tactic:
rcases n with (_ | n)
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
hx : ¬IsUnit a
⊢ IsUnit (HPow.hPow (β := ℕ) a 0) ↔ Eq (α := ℕ) 0 0

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ (n + 1)) ↔ n + 1 = 0

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a : M
ha : a ^ n = 1
hn : n ≠ 0
⊢ (↑(ofPowEqOne a n ha hn ^ n) : M) = (↑1 : M)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
n : ℕ
a : M
ha : a ^ n = 1
hn : n ≠ 0
⊢ IsUnit a

Tactic:
(Units.ofPowEqOne _ n ha hn).isUnit

Premises used: Units.ofPowEqOne, Units.isUnit
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
rw₁ : Commute (↑u : M) a ↔ a * (↑u : M) = (↑u : M) * a
rw₂ : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
rw₃ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
rw₄ rw₅ : (↑u : M) * a = a * (↑u : M) ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * a * (↑u : M) = a

Tactic:
rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]

Premises used: mul_assoc, SemiconjBy, Commute, eq_comm, Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : (↑u⁻¹ : M) * a * (↑u : M) = a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
rw₁ rw₂ : (↑u⁻¹ : M) * (a * (↑u : M)) = a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a
⊢ Commute (↑u : M) a ↔ (↑u⁻¹ : M) * (a * (↑u : M)) = a

Tactic:
rw [u.commute_iff_inv_mul_cancel, mul_assoc]

Premises used: Units.commute_iff_inv_mul_cancel, mul_assoc
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : Commute (↑u : M) a ↔ (↑u : M) * a = a * (↑u : M)
rw₁ : SemiconjBy (↑u : M) a a ↔ (↑u : M) * a = a * (↑u : M)
rw₂ rw₃ : (↑u : M) * a = a * (↑u : M) ↔ (↑u : M) * a = a * (↑u : M)
⊢ Commute (↑u : M) a ↔ (↑u : M) * a * (↑u⁻¹ : M) = a

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul, Commute, SemiconjBy]

Premises used: Units.mul_inv_eq_iff_eq_mul, SemiconjBy, Commute
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
a : M
rw : (↑u : M) * a * (↑u⁻¹ : M) = a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
rw₁ rw₂ : (↑u : M) * (a * (↑u⁻¹ : M)) = a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a
⊢ Commute (↑u : M) a ↔ (↑u : M) * (a * (↑u⁻¹ : M)) = a

Tactic:
rw [u.commute_iff_mul_inv_cancel, mul_assoc]

Premises used: mul_assoc, Units.commute_iff_mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : a / b * (b * d) = c / d * (b * d) ↔ a * d = c * b
rw₁ : a / b * b * d = c / d * (b * d) ↔ a * d = c * b
rw₂ : a * d = c / d * (b * d) ↔ a * d = c * b
rw₃ : a * d = c / d * b * d ↔ a * d = c * b
rw₄ : a * d = c / d * d * 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 [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, hbd.right_comm,
    hd.div_mul_cancel]

Premises used: mul_assoc, IsUnit.mul, Commute.right_comm, IsUnit.mul_left_inj, IsUnit.div_mul_cancel
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : a / b = c * d⁻¹ ↔ a * d = c * b
rw₁ : a / b = c / d ↔ a * d = c * b
rw₂ rw₃ : a * d = c * b ↔ a * d = c * b
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, hbd.div_eq_div_iff_of_isUnit hb hd]

Premises used: div_eq_mul_inv, Commute.div_eq_div_iff_of_isUnit
-- Module: Mathlib.Algebra.Group.Commute.Units
Goal:
M : Type u_1
inst : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
rw : d * b * (b⁻¹ * a) = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₁ : d * b * b⁻¹ * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₂ : d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₃ : d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₄ : d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
rw₅ : d * a = d * b * d⁻¹ * c ↔ d * a = b * c
rw₆ : d * a = d * (b * d⁻¹) * c ↔ d * a = b * c
rw₇ : d * a = b * (d * d⁻¹) * c ↔ d * a = b * c
rw₈ : d * a = b * 1 * c ↔ d * a = b * c
rw₉ rw₁₀ : d * a = b * c ↔ d * a = b * c
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c

Tactic:
rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]

Premises used: Commute.left_comm, IsUnit.mul_inv_cancel, mul_assoc, IsUnit.mul, IsUnit.mul_right_inj, Commute.symm, mul_one
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsConj a a

Tactic:
⟨1, SemiconjBy.one_left a⟩

Premises used: Exists.intro, IsConj, SemiconjBy.one_left, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
g h : α
⊢ IsConj g h ↔ IsConj h g

Tactic:
⟨IsConj.symm, IsConj.symm⟩

Premises used: IsConj.symm, Iff.intro
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : IsConj a b
c : αˣ
hc : SemiconjBy (↑c : α) a b
⊢ a = b

Tactic:
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc

Premises used: mul_assoc, Units.mul_inv_eq_iff_eq_mul, SemiconjBy, Units.mul_inv, mul_comm, mul_one
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : IsConj a b
c : αˣ
hc : a = b
⊢ a = b

Tactic:
hc
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : IsConj a b
c : αˣ
hc : a = b
⊢ a = b

Tactic:
exact hc
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
h : a = b
rw rw₁ : IsConj b b
⊢ IsConj a b

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
rw₁ :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₂ :
  (f : (a : α) → β) ((↑c : α) * a) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₃ :
  (f : (a : α) → β) (b * (↑c : α)) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₄ rw₅ :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)

Tactic:
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]

Premises used: Units.coe_map, SemiconjBy, SemiconjBy.eq, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
h : a = 1
rw rw₁ : IsConj.{u} (α := α) 1 1
⊢ IsConj 1 a

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
refine : IsConj 1 a → ∀ (c : αˣ) (h : SemiconjBy (↑c : α) 1 a), a = 1
⊢ IsConj 1 a ↔ a = 1

Tactic:
refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
h_1 : IsConj 1 a
c : αˣ
h : SemiconjBy (↑c : α) 1 a
⊢ (↑c : α) = a * (↑c : α)

Tactic:
rw [SemiconjBy, mul_one] at h

Premises used: SemiconjBy, mul_one
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
h_1 : IsConj 1 a
c : αˣ
h : (↑c : α) = a * (↑c : α)
⊢ a = 1

Tactic:
c.isUnit.mul_eq_right.mp h.symm

Premises used: IsUnit.mul_eq_right, Iff.mp, Units.isUnit, Eq.symm
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
h_1 : IsConj 1 a
c : αˣ
h : (↑c : α) = a * (↑c : α)
⊢ a = 1

Tactic:
exact c.isUnit.mul_eq_right.mp h.symm

Premises used: IsUnit.mul_eq_right, Iff.mp, Units.isUnit, Eq.symm
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsConj a 1 ↔ a = 1

Tactic:
calc
    IsConj a 1 ↔ IsConj 1 a := ⟨IsConj.symm, IsConj.symm⟩
    _ ↔ a = 1 := isConj_one_right

Premises used: IsConj.symm, Trans.trans, isConj_one_right, Iff.intro
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
⊢ IsConj a b ↔ ∃ (c : α), c * a * c⁻¹ = b

Tactic:
⟨fun ⟨c, hc⟩ => ⟨c, mul_inv_eq_iff_eq_mul.2 hc⟩, fun ⟨c, hc⟩ =>
    ⟨⟨c, c⁻¹, mul_inv_cancel c, inv_mul_cancel c⟩, mul_inv_eq_iff_eq_mul.1 hc⟩⟩

Premises used: Iff.mpr, Units.val, _private.0.isConj_iff.match_2, inv_mul_cancel, HMul.hMul, Exists, Inv.inv, Iff.intro, Units.mk, Exists.intro, Iff.mp, mul_inv_cancel, IsConj, _private.0.isConj_iff.match_1, Eq, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
⊢ (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b c : α
⊢ b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
⊢ HPow.hPow (β := ℕ) (a * b * a⁻¹) 0 = a * HPow.hPow (β := ℕ) b 0 * a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹

Tactic:
simp [pow_succ, hi]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
i : ℕ
a b : α
zero : HPow.hPow (β := ℕ) (a * b * a⁻¹) 0 = a * HPow.hPow (β := ℕ) b 0 * a⁻¹
succ : ∀ (i : ℕ) (hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹), (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
induction i with
  | zero => simp
  | succ i hi => simp [pow_succ, hi]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
i : ℤ
a b : α
ofNat : ∀ (a_1 : ℕ), (a * b * a⁻¹) ^ Int.ofNat a_1 = a * b ^ Int.ofNat a_1 * a⁻¹
negSucc : ∀ (a_1 : ℕ), (a * b * a⁻¹) ^ Int.negSucc a_1 = a * b ^ Int.negSucc a_1 * a⁻¹
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
cases i
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
a_1 : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a_1 = a * b ^ Int.ofNat a_1 * a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
a_1 : ℕ
negSucc : a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * (b ^ (a_1 + 1))⁻¹ * a⁻¹
⊢ (a * b * a⁻¹) ^ Int.negSucc a_1 = a * b ^ Int.negSucc a_1 * a⁻¹

Tactic:
simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]

Premises used: zpow_negSucc, conj_pow, inv_inv, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
a b : α
a_1 : ℕ
negSucc negSucc₁ : a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹)
⊢ a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * (b ^ (a_1 + 1))⁻¹ * a⁻¹

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Group α
x a b : α
⊢ Eq.{u + 1} (α := α) ((fun (g : α) ↦ x * g * x⁻¹) a) ((fun (g : α) ↦ x * g * x⁻¹) b) → a = b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
⊢ Eq (α := ConjClasses α) (ConjClasses.mk a) (ConjClasses.mk b) ↔ IsConj a b

Tactic:
Iff.intro Quotient.exact Quot.sound

Premises used: Quot.sound, Iff.intro, Quotient.exact
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ ⟦a⟧ = ConjClasses.mk a

Tactic:
rfl

Premises used: ConjClasses.mk, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ Eq (α := Quot (α := α) (⇑(IsConj.setoid α) : α → α → Prop)) (Quot.mk (⇑(IsConj.setoid α) : α → α → Prop) a)
    (ConjClasses.mk a)

Tactic:
rfl

Premises used: ConjClasses.mk, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
p : ConjClasses α → Prop
⊢ (∀ (a : ConjClasses α), p a) ↔ ∀ (a : α), p (ConjClasses.mk a)

Tactic:
Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h

Premises used: ConjClasses.mk, Quotient.inductionOn, Iff.intro
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
⊢ Function.Surjective.{u + 1, u + 1} (α := α) (β := ConjClasses α) ConjClasses.mk

Tactic:
forall_isConj.2 fun a => ⟨a, rfl⟩

Premises used: Iff.mpr, ConjClasses.forall_isConj, Exists.intro, Function.Surjective, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
⊢ Eq.{u + 1} (α := ConjClasses α) 1 (ConjClasses.mk 1)

Tactic:
rfl

Premises used: ConjClasses.mk, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : ConjClasses α
⊢ ∃ (a0 : α), ConjClasses.mk a0 = a

Tactic:
Quot.exists_rep a

Premises used: ConjClasses.mk, ConjClasses, Quot.exists_rep, Quotient
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : ConjClasses β
obtain : ∀ (b : β), ∃ (a : ConjClasses α), map f a = ConjClasses.mk b
⊢ ∃ (a : ConjClasses α), map f a = b

Tactic:
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b

Premises used: ConjClasses.mk_surjective, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
obtain : ∀ (a : α), ∃ (a_1 : ConjClasses α), map f a_1 = ConjClasses.mk ((f : (a : α) → β) a)
⊢ ∃ (a : ConjClasses α), map f a = ConjClasses.mk b

Tactic:
obtain ⟨a, rfl⟩ := hf b

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ ∃ (a_1 : ConjClasses α), map f a_1 = ConjClasses.mk ((f : (a : α) → β) a)

Tactic:
⟨ConjClasses.mk a, rfl⟩

Premises used: ConjClasses.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ ∃ (a_1 : ConjClasses α), map f a_1 = ConjClasses.mk ((f : (a : α) → β) a)

Tactic:
exact ⟨ConjClasses.mk a, rfl⟩
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : CommMonoid α
⊢ Function.Injective.{u + 1, u + 1} (α := α) (β := ConjClasses α) ConjClasses.mk

Tactic:
fun _ _ =>
  (mk_eq_mk_iff_isConj.trans isConj_iff_eq).1

Premises used: ConjClasses.mk_eq_mk_iff_isConj, isConj_iff_eq, Iff.mp, Iff.trans, Function.Injective
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : CommMonoid α
⊢ Function.Bijective.{u + 1, u + 1} (α := α) (β := ConjClasses α) ConjClasses.mk

Tactic:
⟨mk_injective, mk_surjective⟩

Premises used: ConjClasses.mk_injective, ConjClasses.mk_surjective, And.intro, Function.Bijective
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : CommMonoid α
rw :
  ∀ (a : α),
    Eq (α := ConjClasses α) (ConjClasses.mk (Quotient.lift (s := IsConj.setoid α) id ⋯ (ConjClasses.mk a)))
      (ConjClasses.mk a)
⊢ Function.RightInverse.{u + 1, u + 1} (α := α) (β := ConjClasses α) (Quotient.lift id ⋯) ConjClasses.mk

Tactic:
rw [Function.RightInverse, Function.LeftInverse, forall_isConj]

Premises used: Function.LeftInverse, ConjClasses.forall_isConj, Function.RightInverse
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
β : Type v
inst : CommMonoid α
⊢ ∀ (a : α),
    Eq (α := ConjClasses α) (ConjClasses.mk (Quotient.lift (s := IsConj.setoid α) id ⋯ (ConjClasses.mk a)))
      (ConjClasses.mk a)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ a ∈ conjugatesOf a

Tactic:
IsConj.refl _

Premises used: Set.Mem, setOf, conjugatesOf, IsConj.refl, IsConj
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
ab : IsConj a b
⊢ conjugatesOf a = conjugatesOf b

Tactic:
Set.ext fun _ => ⟨fun ag => ab.symm.trans ag, fun bg => ab.trans bg⟩

Premises used: Set.ext, IsConj.symm, IsConj.trans, Iff.intro
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ b ∈ conjugatesOf b

Tactic:
have ha := mem_conjugatesOf_self (a := b)
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
rwa rwa₁ rwa₂ rwa₃ : ∀ (ha : b ∈ conjugatesOf a), IsConj a b
⊢ IsConj a b

Tactic:
rwa [← h] at ha
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
⊢ a ∈ carrier (ConjClasses.mk a)

Tactic:
IsConj.refl _

Premises used: Set.Mem, setOf, ConjClasses.carrier, conjugatesOf, IsConj.refl, IsConj
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
b : ConjClasses α
revert : ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
revert b
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : α
rw : ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ Eq (α := ConjClasses α) (ConjClasses.mk a) (ConjClasses.mk a_1)
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
rw [forall_isConj]

Premises used: ConjClasses.forall_isConj
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
rw : a ∈ conjugatesOf b ↔ IsConj b a
⊢ a ∈ carrier (ConjClasses.mk b) ↔ Eq (α := ConjClasses α) (ConjClasses.mk a) (ConjClasses.mk b)

Tactic:
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]

Premises used: Quotient.lift_mk, ConjClasses.carrier, ConjClasses.quotient_mk_eq_mk, eq_comm, ConjClasses.mk_eq_mk_iff_isConj
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a

Tactic:
rfl