awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ (a : ↥M'),
    Eq.{u_2 + 1} (α := ↥(map f M')) ((f.subsemigroupMap M' : (a : ↥M') → ↥(map f M')) a : ↥(map f M'))
      (Subtype.mk (p := fun (x : N) ↦ x ∈ map f M') ((f : (a : M) → N) x) ⋯ : ↥(map f M'))

Tactic:
⟨⟨x, hx⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ (a : ↥M'),
    Eq.{u_2 + 1} (α := ↥(map f M')) ((f.subsemigroupMap M' : (a : ↥M') → ↥(map f M')) a : ↥(map f M'))
      (Subtype.mk (p := fun (x : N) ↦ x ∈ map f M') ((f : (a : M) → N) x) ⋯ : ↥(map f M'))

Tactic:
exact ⟨⟨x, hx⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
inst_2 : Nonempty N
⊢ Eq (α := Subsemigroup M) (srange (fst M N)) ⊤

Tactic:
(fst M N).srange_eq_top_of_surjective <| Prod.fst_surjective

Premises used: MulHom.fst, Prod.fst_surjective, MulHom.srange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
inst_2 : Nonempty M
⊢ Eq (α := Subsemigroup N) (srange (snd M N)) ⊤

Tactic:
(snd M N).srange_eq_top_of_surjective <| Prod.snd_surjective

Premises used: MulHom.snd, MulHom.srange_eq_top_of_surjective, Prod.snd_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
inst_2 : Nonempty M
inst_3 : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, ← srange_eq_map, srange_fst, srange_snd]

Premises used: Subsemigroup.srange_snd, eq_top_iff, Subsemigroup.srange_fst, MulHom.srange_eq_map, Subsemigroup.le_prod_iff
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
s : Subsemigroup M
⊢ srange (M := ↥s) (MulMemClass.subtype s) = s

Tactic:
SetLike.coe_injective <| (coe_srange _).trans <| Subtype.range_coe

Premises used: MulHom.coe_srange, SetLike.coe_injective, Subtype.range_coe, Eq.trans
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup M
⊢ S = ⊤ ↔ ∀ (x : M), x ∈ S

Tactic:
eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Premises used: eq_top_iff, Subsemigroup.mem_top, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g (⇑f : (a : M) → N)
x : ↥f.srange
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x' : N) ((f : (a : M) → N) x' : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup N
⊢ map f (comap f S) = S ⊓ f.srange

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup N
h : S ≤ f.srange
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Premises used: inf_of_le_left, Subsemigroup.map_comap_eq
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
M : Type u_2
inst : MulOneClass M
f g : α → M
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x * g x) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_binop_subset (· * ·) (one_mul _) f g

Premises used: HMul.hMul, Function.mulSupport_binop_subset, one_mul
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
f : α → M
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) ⊆ mulSupport f

Tactic:
simp [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ (n + 1)) ⊆ mulSupport f

Tactic:
simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Premises used: HasSubset.Subset.trans, Set.union_subset, Set.Subset.rfl, pow_succ', Function.mulSupport_mul
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
f : α → M
n : ℕ
zero : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) ⊆ mulSupport f
succ :
  ∀ (n : ℕ) (hfn : (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f),
    (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ (n + 1)) ⊆ mulSupport f
⊢ (mulSupport.{u_1, u_2} (M := M) fun (x : α) ↦ f x ^ n) ⊆ mulSupport f

Tactic:
induction n with
  | zero => simp [pow_zero]
  | succ n hfn =>
    simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Premises used: pow_zero, pow_succ'
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
G : Type u_3
inst : DivisionMonoid G
f : α → G
⊢ (mulSupport.{u_1, u_3} (M := G) fun (x : α) ↦ (f x)⁻¹) = mulSupport f

Tactic:
ext fun _ => inv_ne_one

Premises used: Set.ext, inv_ne_one
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
G : Type u_3
inst : DivisionMonoid G
f : α → G
⊢ mulSupport f⁻¹ = mulSupport f

Tactic:
mulSupport_fun_inv f

Premises used: Function.mulSupport_fun_inv
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
G : Type u_3
inst : DivisionMonoid G
f g : α → G
⊢ Eq.{u_3 + 1} (α := G) ((fun (a b : G) ↦ a * b⁻¹) 1 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Support
Goal:
α : Type u_1
G : Type u_3
inst : DivisionMonoid G
f g : α → G
⊢ (mulSupport.{u_1, u_3} (M := G) fun (x : α) ↦ f x / g x) ⊆ mulSupport f ∪ mulSupport g

Tactic:
mulSupport_binop_subset (· / ·) one_div_one f g

Premises used: Function.mulSupport_binop_subset, HDiv.hDiv, one_div_one
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ Injective (β := M) fun (a : M) ↦ a ^ n

Tactic:
IsMulTorsionFree.pow_left_injective hn

Premises used: IsMulTorsionFree.pow_left_injective
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a b : M
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
(pow_left_injective hn).eq_iff

Premises used: pow_left_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := M) 1 n
rw₁ rw₂ : a ^ n = 1 ↔ a ^ n = 1
⊢ a ^ n = 1 ↔ a = 1

Tactic:
rw [← pow_left_inj (a := a) hn, one_pow]

Premises used: one_pow, pow_left_inj
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
inl : HPow.hPow (β := ℕ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℕ) 0 0
inr : ∀ (hn : n ≠ 0), a ^ n = 1 ↔ a = 1 ∨ n = 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
a : M
⊢ HPow.hPow (β := ℕ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℕ) 0 0

Tactic:
simp [pow_eq_one_iff_left, *]

Premises used: pow_eq_one_iff_left
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
simp [pow_eq_one_iff_left, *]

Premises used: pow_eq_one_iff_left
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
n : ℕ
a : M
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
M : Type u_1
inst : Monoid M
inst_1 : IsMulTorsionFree M
a : M
⊢ Ne (α := ℕ) 2 0

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℕ
h : Ne (α := ℤ) (↑(n + 1) : ℤ) 0
⊢ Injective (β := G) fun (a : G) ↦ HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ)

Tactic:
simpa [← Int.natCast_one, ← Int.natCast_add] using pow_left_injective n.succ_ne_zero

Premises used: Int.natCast_add, pow_left_injective, Int.natCast_one, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℕ
h : Int.negSucc n ≠ 0
⊢ Injective (β := G) fun (a : G) ↦ a ^ Int.negSucc n

Tactic:
simpa using inv_injective.comp (pow_left_injective n.succ_ne_zero)

Premises used: pow_left_injective, Nat.succ_ne_zero, Function.Injective.comp, inv_injective
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a b : G
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
(zpow_left_injective hn).eq_iff

Premises used: Function.Injective.eq_iff, zpow_left_injective
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a b : G
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
zpow_left_inj hn

Premises used: zpow_left_inj
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
rw : a ^ n = 1 ↔ a ^ n = HPow.hPow (α := G) 1 n
rw₁ rw₂ : a ^ n = 1 ↔ a ^ n = 1
⊢ a ^ n = 1 ↔ a = 1

Tactic:
rw [← zpow_left_inj (a := a) hn, one_zpow]

Premises used: one_zpow, zpow_left_inj
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
inl : HPow.hPow (β := ℤ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℤ) 0 0
inr : ∀ (hn : n ≠ 0), a ^ n = 1 ↔ a = 1 ∨ n = 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
⊢ HPow.hPow (β := ℤ) a 0 = 1 ↔ a = 1 ∨ Eq (α := ℤ) 0 0

Tactic:
simp [zpow_eq_one_iff_left, *]

Premises used: IsMulTorsionFree.zpow_eq_one_iff_left
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
simp [zpow_eq_one_iff_left, *]

Premises used: IsMulTorsionFree.zpow_eq_one_iff_left
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
n : ℤ
a : G
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
rw : a = a⁻¹ ↔ HPow.hPow (β := ℕ) a 2 = 1
rw₁ : a = a⁻¹ ↔ a * a = 1
rw₂ rw₃ : a = a⁻¹ ↔ a = a⁻¹
⊢ a = a⁻¹ ↔ a = 1

Tactic:
rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]

Premises used: mul_eq_one_iff_eq_inv, sq, sq_eq_one
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
rw : a = a⁻¹ ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ a⁻¹ = a ↔ a = 1

Tactic:
rw [eq_comm, self_eq_inv]

Premises used: eq_comm, self_eq_inv
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
⊢ a ≠ a⁻¹ ↔ a ≠ 1

Tactic:
self_eq_inv.ne

Premises used: Iff.ne, self_eq_inv
-- Module: Mathlib.Algebra.Group.Torsion
Goal:
G : Type u_2
inst : Group G
inst_1 : IsMulTorsionFree G
a : G
⊢ a⁻¹ ≠ a ↔ a ≠ 1

Tactic:
inv_eq_self.ne

Premises used: inv_eq_self, Iff.ne
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : One β
⊢ Eq.{u_2 + 1} (α := α) (1 : α) ((e.symm : (a : β) → α) 1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
x y : α
⊢ x * y = (e.symm : (a : β) → α) (HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Div β
x y : α
⊢ x / y = (e.symm : (a : β) → α) (HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Inv β
x : α
⊢ x⁻¹ = (e.symm : (a : β) → α) (((e : (a : α) → β) x)⁻¹ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Pow β M
n : M
x : α
⊢ x ^ n = (e.symm : (a : β) → α) (HPow.hPow (α := β) ((e : (a : α) → β) x : β) n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e_1 e : α ≃ β
inst : Mul β
x_1 : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp [mul_def]

Premises used: Equiv.mul_def
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e_1 e : α ≃ β
inst : Mul β
x : Mul α := e.mul
⊢ α ≃* β

Tactic:
exact
    { e with
      map_mul' := fun x y => by
        simp [mul_def] }
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e.mulEquiv : (a : α) → β) a : β) ((e : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
b : β
⊢ Eq.{u_2 + 1} (α := α) ((MulEquiv.symm e.mulEquiv : (a : β) → α) b : α) ((e.symm : (a : β) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Semigroup β
mul : Mul α := e.mul
apply :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ Semigroup α

Tactic:
apply e.injective.semigroup _

Premises used: Function.Injective.semigroup, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Semigroup β
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Semigroup β
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommSemigroup β
mul : Mul α := e.mul
apply :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ CommSemigroup α

Tactic:
apply e.injective.commSemigroup _

Premises used: Function.Injective.commSemigroup, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommSemigroup β
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommSemigroup β
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α

Tactic:
e.injective.isLeftCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Equiv.injective, DFunLike.coe, Function.Injective.isLeftCancelMul
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsLeftCancelMul β
this : Mul α := e.mul
⊢ IsLeftCancelMul α

Tactic:
exact e.injective.isLeftCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Equiv.injective, DFunLike.coe, Function.Injective.isLeftCancelMul
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α

Tactic:
e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Function.Injective.isRightCancelMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α

Tactic:
exact e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Function.Injective.isRightCancelMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α

Tactic:
e.injective.isCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Function.Injective.isCancelMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Mul β
inst_1 : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α

Tactic:
exact e.injective.isCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply, HMul.hMul, Function.Injective.isCancelMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
⊢ MulOneClass α

Tactic:
apply e.injective.mulOneClass _

Premises used: Function.Injective.mulOneClass, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ Monoid α

Tactic:
apply e.injective.monoid _

Premises used: Function.Injective.monoid, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ CommMonoid α

Tactic:
apply e.injective.commMonoid _

Premises used: Equiv.injective, Function.Injective.commMonoid
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply