awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
u : Prod.{u_3, u_4} Mˣ Nˣ
⊢ ((↑u.1 : M), (↑u.2 : N)) * ((↑u.1⁻¹ : M), (↑u.2⁻¹ : N)) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
u : Prod.{u_3, u_4} Mˣ Nˣ
⊢ ((↑u.1⁻¹ : M), (↑u.2⁻¹ : N)) * ((↑u.1 : M), (↑u.2 : N)) = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
u : (M × N)ˣ
⊢ (fun (u : Prod.{u_3, u_4} Mˣ Nˣ) ↦
        { val := ((↑u.1 : M), (↑u.2 : N)), inv := ((↑u.1⁻¹ : M), (↑u.2⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ : (M × N)ˣ })
      ((MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N)) : (a : (M × N)ˣ) → Mˣ × Nˣ) u) =
    u

Tactic:
simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd,
      Prod.mk.eta, Units.coe_map_inv, Units.mk_val]

Premises used: MonoidHom.coe_snd, Units.coe_map, Units.coe_map_inv, MonoidHom.prod_apply, Units.mk_val, Prod.mk.eta, MonoidHom.coe_fst
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
x : Prod.{u_3, u_4} Mˣ Nˣ
u₁ : Mˣ
u₂ : Nˣ
simp :
  (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).1, inv := (↑u⁻¹ : M × N).1, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Mˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₁ ∧
    (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).2, inv := (↑u⁻¹ : M × N).2, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Nˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₂
⊢ (MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N)) : (a : (M × N)ˣ) → Mˣ × Nˣ)
      ((fun (u : Prod.{u_3, u_4} Mˣ Nˣ) ↦
          { val := ((↑u.1 : M), (↑u.2 : N)), inv := ((↑u.1⁻¹ : M), (↑u.2⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ :
            (M × N)ˣ })
        (u₁, u₂)) =
    (u₁, u₂)

Tactic:
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv,
      MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]

Premises used: MonoidHom.coe_snd, Units.inv_eq_val_inv, MonoidHom.prod_apply, Prod.mk.injEq, MonoidHom.coe_fst, Units.map
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
x : Prod.{u_3, u_4} Mˣ Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).1, inv := (↑u⁻¹ : M × N).1, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Mˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₁ ∧
    (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).2, inv := (↑u⁻¹ : M × N).2, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Nˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₂

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
x : Prod.{u_3, u_4} Mˣ Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).1, inv := (↑u⁻¹ : M × N).1, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Mˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₁ ∧
    (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).2, inv := (↑u⁻¹ : M × N).2, val_inv := ⋯, inv_val := ⋯ })
            ⋯ :
          (a : (M × N)ˣ) → Nˣ)
        { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ } =
      u₂

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : Subsingleton.{u_3 + 1} Mˣ
inst_3 : Subsingleton.{u_4 + 1} Nˣ
⊢ ∀ (a : M × N), IsUnit a → a = 1

Tactic:
simp [Prod.isUnit_iff, Prod.ext_iff]

Premises used: Prod.isUnit_iff, Prod.ext_iff
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
α : Type u_6
inst : Monoid α
⊢ Eq.{u_6 + 1} (α := α × αᵐᵒᵖ) ((↑1 : α), op (↑1⁻¹ : α)) 1

Tactic:
simp only [inv_one, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]

Premises used: inv_one, Prod.mk_eq_one, MulOpposite.op_one, Units.val_one, and_self_iff
-- Module: Mathlib.Algebra.Group.Prod
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
α : Type u_6
inst : Monoid α
x y : αˣ
⊢ ((↑(x * y) : α), op (↑(x * y)⁻¹ : α)) = ((↑x : α), op (↑x⁻¹ : α)) * ((↑y : α), op (↑y⁻¹ : α))

Tactic:
simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]

Premises used: MulOpposite.op_mul, Prod.mk_mul_mk, mul_inv_rev, Units.val_mul
-- Module: Mathlib.Algebra.Group.Prod
Goal:
α : Type u_6
inst : Monoid α
⊢ Function.Injective (α := αˣ) (β := α × αᵐᵒᵖ) (⇑(embedProduct α) : (a : αˣ) → α × αᵐᵒᵖ)

Tactic:
fun _ _ h => Units.ext <| (congr_arg Prod.fst h :)

Premises used: Units.ext, Prod.fst, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : DivisionMonoid G
a x y : G
simp_rw : a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a
simp_rw₁ : (x * a)⁻¹ = (a * y)⁻¹ ↔ a * y = x * a
simp_rw₂ : x * a = a * y ↔ a * y = x * a
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]

Premises used: SemiconjBy, eq_comm, inv_inj, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
simp_rw : a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
simp_rw₁ : a⁻¹ * y * a = x ↔ a * x = y * a
simp_rw₂ : a⁻¹ * (y * a) = x ↔ a * x = y * a
simp_rw₃ : y * a = a * x ↔ a * x = y * a
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]

Premises used: mul_assoc, SemiconjBy, eq_comm, eq_mul_inv_iff_mul_eq, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
rw : SemiconjBy a⁻¹ y⁻¹ x⁻¹ ↔ SemiconjBy a x y
rw₁ rw₂ : SemiconjBy a x y ↔ SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
rw [← inv_symm_left_iff, inv_inv_symm_iff]

Premises used: SemiconjBy.inv_inv_symm_iff, SemiconjBy.inv_symm_left_iff
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (HPow.hPow (β := ℤ) x (↑n : ℤ)) (HPow.hPow (β := ℤ) y (↑n : ℤ))

Tactic:
simp [zpow_natCast, h.pow_right n]

Premises used: zpow_natCast, SemiconjBy.pow_right
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
simp : SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, inv_right_iff]

Premises used: zpow_negSucc, SemiconjBy.inv_right_iff
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))

Tactic:
apply pow_right h

Premises used: SemiconjBy.pow_right
-- Module: Mathlib.Algebra.Group.Semiconj.Basic
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
rw : a * x * a⁻¹ = 1 ↔ y = 1
rw₁ : y * a * a⁻¹ = 1 ↔ y = 1
rw₂ rw₃ : y = 1 ↔ y = 1
⊢ x = 1 ↔ y = 1

Tactic:
rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, SemiconjBy.eq, conj_eq_one_iff
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
S : Type u_1
inst : Mul S
a x y : S
h : SemiconjBy a x y
⊢ a * x = y * a

Tactic:
h

Premises used: SemiconjBy
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
S : Type u_1
inst : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : a * x * x' = y * y' * a
rw₁ : y * a * x' = y * y' * a
rw₂ : y * (a * x') = y * y' * a
rw₃ : y * (y' * a) = y * y' * a
rw₄ rw₅ : y * y' * a = y * y' * a
⊢ a * (x * x') = y * y' * a

Tactic:
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

Premises used: mul_assoc, SemiconjBy.eq
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
S : Type u_1
inst : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
rw : a * (b * x) = z * (a * b)
rw₁ : a * (y * b) = z * (a * b)
rw₂ : a * y * b = z * (a * b)
rw₃ : z * a * b = z * (a * b)
rw₄ rw₅ : z * (a * b) = z * (a * b)
⊢ a * b * x = z * (a * b)

Tactic:
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

Premises used: mul_assoc, SemiconjBy.eq
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
S : Type u_1
inst : Semigroup S
⊢ IsTrans S fun (a b : S) ↦ ∃ (c : S), SemiconjBy c a b

Tactic:
⟨fun _ _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨y * x, hy.mul_left hx⟩⟩

Premises used: HMul.hMul, IsTrans.mk, SemiconjBy, _private.0.SemiconjBy.isTrans.match_1, Exists, Exists.intro, SemiconjBy.mul_left
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : MulOneClass M
a : M
rw : a * 1 = 1 * a
rw₁ : a = 1 * a
rw₂ rw₃ : a = a
⊢ SemiconjBy a 1 1

Tactic:
rw [SemiconjBy, mul_one, one_mul]

Premises used: SemiconjBy, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : MulOneClass M
x : M
⊢ SemiconjBy 1 x x

Tactic:
Eq.symm <| one_right x

Premises used: SemiconjBy, SemiconjBy.one_right, Eq.symm
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
zero : SemiconjBy a 1 1
⊢ SemiconjBy a (HPow.hPow (β := ℕ) x 0) (HPow.hPow (β := ℕ) y 0)

Tactic:
rw [pow_zero, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Tactic:
SemiconjBy.one_right _

Premises used: SemiconjBy.one_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Tactic:
exact SemiconjBy.one_right _

Premises used: SemiconjBy.one_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
succ : SemiconjBy a (x ^ n * x) (y ^ n * y)
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)

Tactic:
ih.mul_right h

Premises used: SemiconjBy.mul_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)

Tactic:
exact ih.mul_right h

Premises used: SemiconjBy.mul_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
zero : SemiconjBy a (HPow.hPow (β := ℕ) x 0) (HPow.hPow (β := ℕ) y 0)
succ : ∀ (n : ℕ) (ih : SemiconjBy a (x ^ n) (y ^ n)), SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h

Premises used: pow_succ, pow_zero, SemiconjBy.one_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x : G
rw : a * x = a * x * (a⁻¹ * a)
rw₁ : a * x = a * x * 1
rw₂ rw₃ : a * x = a * x
⊢ a * x = a * x * a⁻¹ * a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

Premises used: inv_mul_cancel, mul_assoc, mul_one
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
simp : b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
⊢ b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a

Tactic:
simp only [← mul_assoc, inv_mul_cancel_right]

Premises used: mul_assoc, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a
⊢ b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
repeat : b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
repeat rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
G : Type u_3
inst : Group G
a x y b : G
rw : a * (x * b⁻¹) = y * (a * b⁻¹) ↔ a * x = y * a
rw₁ : a * x * b⁻¹ = y * (a * b⁻¹) ↔ a * x = y * a
rw₂ : a * x * b⁻¹ = y * a * b⁻¹ ↔ a * x = y * a
rw₃ rw₄ : a * x = y * a ↔ a * x = y * a
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Tactic:
rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

Premises used: mul_assoc, mul_right_cancel_iff, mul_left_cancel_iff
-- Module: Mathlib.Algebra.Group.Semiconj.Defs
Goal:
M : Type u_2
inst : CancelCommMonoid M
a x y : M
h : x = y
rw : SemiconjBy a y y
rw₁ : a * y = y * a
rw₂ rw₃ : y * a = y * a
⊢ SemiconjBy a x y

Tactic:
rw [h, SemiconjBy, mul_comm]

Premises used: SemiconjBy, mul_comm
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
rw rw₁ : a * (↑x⁻¹ : M) = a * (↑x⁻¹ : M)
⊢ a * (↑x⁻¹ : M) = (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M)

Tactic:
rw [Units.inv_mul_cancel_left]

Premises used: Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
rw : (↑y⁻¹ : M) * (a * (↑x : M)) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a
rw₁ : (↑y⁻¹ : M) * (a * (↑x : M) * (↑x⁻¹ : M)) = (↑y⁻¹ : M) * a
rw₂ rw₃ : (↑y⁻¹ : M) * a = (↑y⁻¹ : M) * a
⊢ (↑y⁻¹ : M) * ((↑y : M) * a) * (↑x⁻¹ : M) = (↑y⁻¹ : M) * a

Tactic:
rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]

Premises used: mul_assoc, Units.mul_inv_cancel_right, SemiconjBy.eq
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
⊢ SemiconjBy a (↑x⁻¹ : M) (↑y⁻¹ : M) ↔ SemiconjBy a (↑x : M) (↑y : M)

Tactic:
⟨units_inv_right, units_inv_right⟩

Premises used: Iff.intro, SemiconjBy.units_inv_right
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
rw rw₁ : (↑a⁻¹ : M) * y = (↑a⁻¹ : M) * y
⊢ (↑a⁻¹ : M) * y = (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M))

Tactic:
rw [Units.mul_inv_cancel_right]

Premises used: Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a : M) x y
rw : (↑a⁻¹ : M) * ((↑a : M) * x * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)
rw₁ : (↑a⁻¹ : M) * ((↑a : M) * x) * (↑a⁻¹ : M) = x * (↑a⁻¹ : M)
rw₂ rw₃ : x * (↑a⁻¹ : M) = x * (↑a⁻¹ : M)
⊢ (↑a⁻¹ : M) * (y * (↑a : M) * (↑a⁻¹ : M)) = x * (↑a⁻¹ : M)

Tactic:
rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]

Premises used: mul_assoc, SemiconjBy.eq, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
x y : M
⊢ SemiconjBy (↑a⁻¹ : M) y x ↔ SemiconjBy (↑a : M) x y

Tactic:
⟨units_inv_symm_left, units_inv_symm_left⟩

Premises used: Iff.intro, SemiconjBy.units_inv_symm_left
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a x y : Mˣ
h : SemiconjBy a x y
⊢ SemiconjBy (↑a : M) (↑x : M) (↑y : M)

Tactic:
congr_arg Units.val h

Premises used: Units.val, SemiconjBy, congr_arg
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a x y : Mˣ
h : SemiconjBy (↑a : M) (↑x : M) (↑y : M)
⊢ SemiconjBy a x y

Tactic:
Units.ext h

Premises used: SemiconjBy, Units.ext
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a x y : Mˣ
⊢ SemiconjBy (↑a : M) (↑x : M) (↑y : M) ↔ SemiconjBy a x y

Tactic:
⟨units_of_val, units_val⟩

Premises used: Iff.intro, SemiconjBy.units_of_val, SemiconjBy.units_val
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
n : ℕ
⊢ SemiconjBy a (↑(HPow.hPow (β := ℤ) x (↑n : ℤ)) : M) (↑(HPow.hPow (β := ℤ) y (↑n : ℤ)) : M)

Tactic:
simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]

Premises used: zpow_natCast, SemiconjBy.pow_right, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a (↑x : M) (↑y : M)
n : ℕ
⊢ SemiconjBy a (↑(x ^ -[n+1]) : M) (↑(y ^ -[n+1]) : M)

Tactic:
simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

Premises used: zpow_negSucc, SemiconjBy.pow_right, Units.val_pow_eq_pow_val, SemiconjBy.units_inv_right
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
x : M
rw rw₁ : (↑u : M) * x = (↑u : M) * x
⊢ (↑u : M) * x = (↑u : M) * x * (↑u⁻¹ : M) * (↑u : M)

Tactic:
rw [Units.inv_mul_cancel_right]

Premises used: Units.inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
x : M
n : ℕ
⊢ ((↑u : M) * x * (↑u⁻¹ : M)) ^ n = (↑u : M) * x ^ n * (↑u⁻¹ : M)

Tactic:
eq_divp_iff_mul_eq.2 ((u.mk_semiconjBy x).pow_right n).eq.symm

Premises used: Iff.mpr, SemiconjBy.eq, divp, SemiconjBy.pow_right, Eq.symm, Units.mk_semiconjBy, eq_divp_iff_mul_eq
-- Module: Mathlib.Algebra.Group.Semiconj.Units
Goal:
M : Type u_1
inst : Monoid M
u : Mˣ
x : M
n : ℕ
⊢ ((↑u⁻¹ : M) * x * (↑u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (↑u : M)

Tactic:
u⁻¹.conj_pow x n

Premises used: Inv.inv, Units.conj_pow
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : One α
⊢ Eq.{u_2 + 1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) 1 : α) (1 : α)

Tactic:
(equivShrink α).symm_apply_apply 1

Premises used: Equiv.symm_apply_apply, OfNat.ofNat, equivShrink
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Mul α
x y : Shrink.{v, u_2} α
⊢ (Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) (x * y) =
    HMul.hMul (α := α) (β := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) x : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) y : α)

Tactic:
simp [Equiv.mul_def]

Premises used: Equiv.mul_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Mul α
x y : α
⊢ (equivShrink α : (a : α) → Shrink.{v, u_2} α) (x * y) =
    HMul.hMul (α := Shrink.{v, u_2} α) (β := Shrink.{v, u_2} α)
      ((equivShrink α : (a : α) → Shrink.{v, u_2} α) x : Shrink.{v, u_2} α)
      ((equivShrink α : (a : α) → Shrink.{v, u_2} α) y : Shrink.{v, u_2} α)

Tactic:
simp [Equiv.mul_def]

Premises used: Equiv.mul_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
M : Type u_3
inst_1 : SMul M α
m : M
x : Shrink.{v, u_2} α
⊢ (Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) (m • x) =
    HSMul.hSMul (β := α) m ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) x : α)

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
M : Type u_3
inst_1 : SMul M α
m : M
x : α
⊢ (equivShrink α : (a : α) → Shrink.{v, u_2} α) (m • x) =
    HSMul.hSMul (β := Shrink.{v, u_2} α) m ((equivShrink α : (a : α) → Shrink.{v, u_2} α) x : Shrink.{v, u_2} α)

Tactic:
simp [Equiv.smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Div α
x y : Shrink.{v, u_2} α
⊢ (Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) (x / y) =
    HDiv.hDiv (α := α) (β := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) x : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) y : α)

Tactic:
simp [Equiv.div_def]

Premises used: Equiv.div_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Div α
x y : α
⊢ (equivShrink α : (a : α) → Shrink.{v, u_2} α) (x / y) =
    HDiv.hDiv (α := Shrink.{v, u_2} α) (β := Shrink.{v, u_2} α)
      ((equivShrink α : (a : α) → Shrink.{v, u_2} α) x : Shrink.{v, u_2} α)
      ((equivShrink α : (a : α) → Shrink.{v, u_2} α) y : Shrink.{v, u_2} α)

Tactic:
simp [Equiv.div_def]

Premises used: Equiv.div_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Inv α
x : Shrink.{v, u_2} α
⊢ Eq.{u_2 + 1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) x⁻¹ : α)
    (((Equiv.symm (equivShrink α) : (a : Shrink.{v, u_2} α) → α) x)⁻¹ : α)

Tactic:
simp [Equiv.inv_def]

Premises used: Equiv.inv_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Inv α
x : α
⊢ Eq.{v + 1} (α := Shrink.{v, u_2} α) ((equivShrink α : (a : α) → Shrink.{v, u_2} α) x⁻¹ : Shrink.{v, u_2} α)
    (((equivShrink α : (a : α) → Shrink.{v, u_2} α) x)⁻¹ : Shrink.{v, u_2} α)

Tactic:
simp [Equiv.inv_def]

Premises used: Equiv.inv_def
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
M : Type u_1
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Mul α
inst_2 : IsLeftCancelMul α
⊢ IsLeftCancelMul.{v} (Shrink.{v, u_2} α)

Tactic:
(equivShrink α).symm.isLeftCancelMul

Premises used: Equiv.symm, equivShrink, Equiv.isLeftCancelMul
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
M : Type u_1
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Mul α
inst_2 : IsRightCancelMul α
⊢ IsRightCancelMul.{v} (Shrink.{v, u_2} α)

Tactic:
(equivShrink α).symm.isRightCancelMul

Premises used: Equiv.isRightCancelMul, Equiv.symm, equivShrink
-- Module: Mathlib.Algebra.Group.Shrink
Goal:
M : Type u_1
α : Type u_2
inst : Small.{v, u_2} α
inst_1 : Mul α
inst_2 : IsCancelMul α
⊢ IsCancelMul.{v} (Shrink.{v, u_2} α)

Tactic:
(equivShrink α).symm.isCancelMul

Premises used: Equiv.isCancelMul, Equiv.symm, equivShrink
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Subgroup G
g : ↥S
m : α
⊢ g • m = (↑g : G) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Subgroup G
g : G
hg : g ∈ S
a : α
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg • a = g • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G β
inst_2 : SMul α β
inst_3 : SMulCommClass G α β
S : Subgroup G
⊢ SMulCommClass.{u_1, u_2, u_3} (↥S) α β

Tactic:
S.toSubmonoid.smulCommClass_left

Premises used: Set.Mem, Submonoid.smulCommClass_left, Subgroup.toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : SMul α β
inst_2 : MulAction G β
inst_3 : SMulCommClass α G β
S : Subgroup G
⊢ SMulCommClass.{u_2, u_1, u_3} α (↥S) β

Tactic:
S.toSubmonoid.smulCommClass_right

Premises used: Set.Mem, Submonoid.smulCommClass_right, Subgroup.toSubmonoid