awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ f.toMulHom = (↑f : M →ₙ* N)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ f.toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ Eq (α := (a : M) → N) (⇑(↑f : M ≃ N) : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ Eq (α := (a : M) → N) (⇑f.toMulHom : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ ∀ (x y : M),
    (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
map_mul f

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ Bijective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.bijective e

Premises used: EquivLike.bijective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.injective e

Premises used: EquivLike.injective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.surjective e

Premises used: EquivLike.surjective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
x y : M
⊢ Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) x : N) ((e : (a : M) → N) y : N) ↔ x = y

Tactic:
e.injective.eq_iff

Premises used: Function.Injective.eq_iff, MulEquiv.injective
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
inst : Mul M
⊢ Eq (α := (a : M) → M) (⇑(refl M) : (a : M) → M) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
inst : Mul M
m : M
⊢ (refl M : (a : M) → M) m = m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_9
N : Type u_10
inst : Mul M
inst_1 : Mul N
h : M ≃* N
x y : N
⊢ (h.symm : (a : N) → M) (x * y) =
    HMul.hMul (α := M) (β := M) ((h.symm : (a : N) → M) x : M) ((h.symm : (a : N) → M) y : M)

Tactic:
map_mul (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv) x y

Premises used: MulEquiv.toMulHom, Equiv.right_inv, MulEquiv.toEquiv, map_mul, Equiv.symm, DFunLike.coe, Equiv.left_inv, MulHom.inverse
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ f.invFun = (⇑f.symm : (a : N) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ Eq (α := (a : N) → M) (⇑(↑f : M ≃ N).symm : (a : N) → M) (⇑f.symm : (a : N) → M)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ EquivLike.inv f = (⇑f.symm : (a : N) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ (↑f.symm : N ≃ M) = (↑f : M ≃ N).symm

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃* N
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
⊢ Bijective (α := M ≃* N) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, MulEquiv.symm_symm
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
f : N → M
h₁ : LeftInverse (⇑e : (a : M) → N) f
h₂ : RightInverse (⇑e : (a : M) → N) f
h₃ :
  ∀ (x y : N),
    { toFun := f, invFun := (⇑e : (a : M) → N), left_inv := h₁, right_inv := h₂ : N ≃ M }.toFun (x * y) =
      { toFun := f, invFun := (⇑e : (a : M) → N), left_inv := h₁, right_inv := h₂ : N ≃ M }.toFun x *
        { toFun := f, invFun := (⇑e : (a : M) → N), left_inv := h₁, right_inv := h₂ : N ≃ M }.toFun y
⊢ { toFun := f, invFun := (⇑e : (a : M) → N), left_inv := h₁, right_inv := h₂, map_mul' := h₃ : N ≃* M } = e.symm

Tactic:
symm_bijective.injective <| ext fun _ => rfl

Premises used: Function.Bijective.injective, MulEquiv.ext, MulEquiv.symm_bijective, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M ≃ N
h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ { toEquiv := f, map_mul' := h : M ≃* N }.symm = { toEquiv := f.symm, map_mul' := ⋯ }

Tactic:
rfl

Premises used: MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
inst : Mul M
⊢ Eq (α := M ≃* M) (symm (refl M)) (refl M)

Tactic:
rfl

Premises used: MulEquiv.refl, Equiv.symm, MulEquiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
y : N
⊢ (e : (a : M) → N) ((e.symm : (a : N) → M) y : M) = y

Tactic:
e.toEquiv.apply_symm_apply y

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
x : M
⊢ (e.symm : (a : N) → M) ((e : (a : M) → N) x : N) = x

Tactic:
e.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ Eq.{u_4 + 1} (α := M → M) (comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := N) (⇑e.symm : (a : N) → M) (⇑e : (a : M) → N)) id

Tactic:
funext e.symm_apply_apply

Premises used: funext, MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ Eq.{u_5 + 1} (α := N → N) (comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M) (⇑e : (a : M) → N) (⇑e.symm : (a : N) → M)) id

Tactic:
funext e.apply_symm_apply

Premises used: funext, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
x : M
y : N
⊢ (e : (a : M) → N) x = y ↔ x = (e.symm : (a : N) → M) y

Tactic:
e.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: MulEquiv.toEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
x : N
y : M
⊢ (e.symm : (a : N) → M) x = y ↔ x = (e : (a : M) → N) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
x : N
y : M
⊢ y = (e.symm : (a : N) → M) x ↔ (e : (a : M) → N) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: MulEquiv.toEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
α : Type u_9
e : M ≃* N
f : N → α
g : M → α
⊢ f = g ∘ (⇑e.symm : (a : N) → M) ↔ f ∘ (⇑e : (a : M) → N) = g

Tactic:
e.toEquiv.eq_comp_symm f g

Premises used: MulEquiv.toEquiv, Equiv.eq_comp_symm
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
α : Type u_9
e : M ≃* N
f : N → α
g : M → α
⊢ g ∘ (⇑e.symm : (a : N) → M) = f ↔ g = f ∘ (⇑e : (a : M) → N)

Tactic:
e.toEquiv.comp_symm_eq f g

Premises used: MulEquiv.toEquiv, Equiv.comp_symm_eq
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
α : Type u_9
e : M ≃* N
f : α → M
g : α → N
⊢ f = (⇑e.symm : (a : N) → M) ∘ g ↔ (⇑e : (a : M) → N) ∘ f = g

Tactic:
e.toEquiv.eq_symm_comp f g

Premises used: Equiv.eq_symm_comp, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
α : Type u_9
e : M ≃* N
f : α → M
g : α → N
⊢ (⇑e.symm : (a : N) → M) ∘ g = f ↔ g = (⇑e : (a : M) → N) ∘ f

Tactic:
e.toEquiv.symm_comp_eq f g

Premises used: Equiv.symm_comp_eq, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
α : Type u_9
β : Type u_10
inst : Mul α
inst_1 : Mul β
F : Type u_11
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
e : F
x : β
⊢ (e : (a : α) → β) ((symm (↑e : α ≃* β) : (a : β) → α) x : α) = x

Tactic:
(e : α ≃* β).right_inv x

Premises used: Equiv.right_inv, MulEquiv.toEquiv, MulEquivClass.toMulEquiv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
α : Type u_9
β : Type u_10
inst : Mul α
inst_1 : Mul β
F : Type u_11
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
e : F
x : α
⊢ (symm (↑e : α ≃* β) : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
(e : α ≃* β).left_inv x

Premises used: MulEquiv.toEquiv, MulEquivClass.toMulEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
rw :
  (h2 : (a : N) → P) (HMul.hMul (α := N) (β := N) ((h1 : (a : M) → N) x : N) ((h1 : (a : M) → N) y : N)) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
rw₁ rw₂ :
  HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)
⊢ (h2 : (a : N) → P) ((h1 : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := P) (β := P) ((h2 : (a : N) → P) ((h1 : (a : M) → N) x : N) : P)
      ((h2 : (a : N) → P) ((h1 : (a : M) → N) y : N) : P)

Tactic:
rw [map_mul, map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
e₁ : M ≃* N
e₂ : N ≃* P
⊢ Eq (α := M → P) (⇑(e₁.trans e₂) : (a : M) → P)
    (comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := N) (⇑e₂ : (a : N) → P) (⇑e₁ : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
e₁ : M ≃* N
e₂ : N ≃* P
m : M
⊢ Eq.{u_6 + 1} (α := P) ((e₁.trans e₂ : (a : M) → P) m : P) ((e₂ : (a : N) → P) ((e₁ : (a : M) → N) m : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
e₁ : M ≃* N
e₂ : N ≃* P
p : P
⊢ Eq.{u_4 + 1} (α := M) (((e₁.trans e₂).symm : (a : P) → M) p : M)
    ((e₁.symm : (a : N) → M) ((e₂.symm : (a : P) → N) p : N) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ e.symm.trans e = refl N

Tactic:
DFunLike.ext _ _ e.apply_symm_apply

Premises used: DFunLike.ext, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
e : M ≃* N
⊢ e.trans e.symm = refl M

Tactic:
DFunLike.ext _ _ e.symm_apply_apply

Premises used: DFunLike.ext, MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst_1 : (i : ι) → Mul (M i)
i j : ι
h : i = j
x x_1 : M i
refl : (Equiv.cast ⋯).toFun (x * x_1) = (Equiv.cast ⋯).toFun x * (Equiv.cast ⋯).toFun x_1
⊢ (Equiv.cast ⋯).toFun (x * x_1) = (Equiv.cast ⋯).toFun x * (Equiv.cast ⋯).toFun x_1

Tactic:
cases h
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst_1 : (i : ι) → Mul (M i)
i : ι
x x_1 : M i
__Equiv : M i ≃ M i := Equiv.cast ⋯
⊢ (Equiv.cast ⋯).toFun (x * x_1) = (Equiv.cast ⋯).toFun x * (Equiv.cast ⋯).toFun x_1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
inst : MulOneClass M
⊢ Eq (α := M →* M) (↑(refl M) : M →* M) (MonoidHom.id M)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
e₁ : M ≃* N
e₂ : N ≃* P
⊢ Eq (α := M →* P) (↑(e₁.trans e₂) : M →* P) (MonoidHom.comp (↑e₂ : N →* P) (↑e₁ : M →* N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
h :
  ∀ (x : N),
    Eq (α := N) ((MonoidHom.comp (↑e : M →* N) (↑e.symm : N →* M) : (a : N) → N) x : N)
      ((MonoidHom.id N : (a : N) → N) x : N)
⊢ Eq (α := N →* N) (MonoidHom.comp (↑e : M →* N) (↑e.symm : N →* M)) (MonoidHom.id N)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
x : N
⊢ Eq (α := N) ((MonoidHom.comp (↑e : M →* N) (↑e.symm : N →* M) : (a : N) → N) x : N)
    ((MonoidHom.id N : (a : N) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
h :
  ∀ (x : M),
    Eq (α := M) ((MonoidHom.comp (↑e.symm : N →* M) (↑e : M →* N) : (a : M) → M) x : M)
      ((MonoidHom.id M : (a : M) → M) x : M)
⊢ Eq (α := M →* M) (MonoidHom.comp (↑e.symm : N →* M) (↑e : M →* N)) (MonoidHom.id M)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
x : M
⊢ Eq (α := M) ((MonoidHom.comp (↑e.symm : N →* M) (↑e : M →* N) : (a : M) → M) x : M)
    ((MonoidHom.id M : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
e : M ≃* N
f : N →* P
⊢ (fun (f : M →* P) ↦ (f.comp (↑e.symm : N →* M) : N →* P)) (f.comp (↑e : M →* N)) = f

Tactic:
simp [MonoidHom.comp_assoc]

Premises used: MonoidHom.comp_assoc
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
e : M ≃* N
f : P →* M
⊢ MonoidHom.comp (↑e.symm : N →* M) (MonoidHom.comp (↑e : M →* N) f) = f

Tactic:
simp [← MonoidHom.comp_assoc]

Premises used: MonoidHom.comp_assoc
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
h : M ≃* N
⊢ Eq.{u_5 + 1} (α := N) ((h : (a : M) → N) 1 : N) (1 : N)

Tactic:
map_one h

Premises used: map_one
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
h : M ≃* N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((h : (a : M) → N) x : N) (1 : N) ↔ x = 1

Tactic:
EmbeddingLike.map_eq_one_iff

Premises used: EmbeddingLike.map_eq_one_iff
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
h : M ≃* N
x : M
⊢ Ne.{u_5 + 1} (α := N) ((h : (a : M) → N) x : N) (1 : N) ↔ x ≠ 1

Tactic:
EmbeddingLike.map_ne_one_iff

Premises used: EmbeddingLike.map_ne_one_iff
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
n : N
f : M →* N
hf : Bijective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (f : (a : M) → N) ((symm (ofBijective f hf) : (a : N) → M) n : M) = n

Tactic:
(ofBijective f hf).apply_symm_apply n

Premises used: MulEquiv.ofBijective, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
e : M ≃* N
⊢ Eq (α := (a : M) → N) (⇑e.toMonoidHom : (a : M) → N) (⇑e : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
f : M ≃* N
⊢ f.toMonoidHom = (↑f : M →* N)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Injective (α := M ≃* N) toMonoidHom

Tactic:
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
G : Type u_7
H : Type u_8
inst : Group G
inst_1 : DivisionMonoid H
h : G ≃* H
x : G
⊢ Eq.{u_8 + 1} (α := H) ((h : (a : G) → H) x⁻¹ : H) (((h : (a : G) → H) x)⁻¹ : H)

Tactic:
map_inv h x

Premises used: map_inv
-- Module: Mathlib.Algebra.Group.Equiv.Defs
Goal:
G : Type u_7
H : Type u_8
inst : Group G
inst_1 : DivisionMonoid H
h : G ≃* H
x y : G
⊢ (h : (a : G) → H) (x / y) = HDiv.hDiv (α := H) (β := H) ((h : (a : G) → H) x : H) ((h : (a : G) → H) y : H)

Tactic:
map_div h x y

Premises used: map_div
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq.{u_1 + 1} (α := (a : M) → Mᵐᵒᵖ) (⇑opMulEquiv : (a : M) → Mᵐᵒᵖ) op

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq.{u_1 + 1} (α := (a : Mᵐᵒᵖ) → M) (⇑(MulEquiv.symm opMulEquiv) : (a : Mᵐᵒᵖ) → M) unop

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
α : Type u_2
inst : Add α
⊢ (↑opAddEquiv : α ≃ αᵐᵒᵖ) = opEquiv

Tactic:
rfl

Premises used: MulOpposite.opEquiv, MulOpposite, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
α : Type u_2
inst : Mul α
⊢ (↑opMulEquiv : α ≃ αᵃᵒᵖ) = opEquiv

Tactic:
rfl

Premises used: AddOpposite, AddOpposite.opEquiv, AddOpposite.unop, AddOpposite.op, rfl
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M_1 : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute.{u_4} (S := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
x y : M
⊢ (op ∘ (⇑f : (a : M) → N)) (x * y) = HMul.hMul (α := Nᵐᵒᵖ) ((op ∘ (⇑f : (a : M) → N)) x) ((op ∘ (⇑f : (a : M) → N)) y)

Tactic:
simp [(hf x y).eq]

Premises used: Commute.eq
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M_1 : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute.{u_4} (S := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
x y : M
⊢ (op ∘ (⇑f : (a : M) → N)) (x * y) = HMul.hMul (α := Nᵐᵒᵖ) ((op ∘ (⇑f : (a : M) → N)) x) ((op ∘ (⇑f : (a : M) → N)) y)

Tactic:
simp [(hf x y).eq]

Premises used: Commute.eq
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M : Type u_1
α_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : Mul β
f : MulEquiv.{u_3, u_4} αᵐᵒᵖ βᵐᵒᵖ
x : α
⊢ Function.comp.{u_4 + 1, u_3 + 1, u_3 + 1} (α := β) unop ((⇑f.symm : (a : βᵐᵒᵖ) → αᵐᵒᵖ) ∘ MulOpposite.op)
      ((unop ∘ (⇑f : (a : αᵐᵒᵖ) → βᵐᵒᵖ) ∘ MulOpposite.op) x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
M : Type u_1
α_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : Mul β
f : MulEquiv.{u_3, u_4} αᵐᵒᵖ βᵐᵒᵖ
x : β
⊢ Function.comp.{u_3 + 1, u_4 + 1, u_4 + 1} (α := α) unop ((⇑f : (a : αᵐᵒᵖ) → βᵐᵒᵖ) ∘ MulOpposite.op)
      ((unop ∘ (⇑f.symm : (a : βᵐᵒᵖ) → αᵐᵒᵖ) ∘ MulOpposite.op) x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Opposite
Goal:
α : Type u_3
β : Type u_4
inst : AddZeroClass α
inst_1 : AddZeroClass β
f g : AddMonoidHom.{u_3, u_4} αᵐᵒᵖ β
h : Eq (α := α →+ β) (f.comp (AddEquiv.toAddMonoidHom opAddEquiv)) (g.comp (AddEquiv.toAddMonoidHom opAddEquiv))
⊢ f = g

Tactic:
AddMonoidHom.ext <| MulOpposite.rec' fun x => (DFunLike.congr_fun h :) x

Premises used: MulOpposite.rec', AddMonoidHom.ext
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
a : α
⊢ IsSquare a ↔ ∃ (r : α), a = r * r

Tactic:
.rfl

Premises used: Iff.rfl, IsSquare
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
r : α
⊢ IsSquare (r * r)

Tactic:
⟨r, rfl⟩

Premises used: IsSquare, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
a : α
⊢ IsSquare (op a) ↔ IsSquare a

Tactic:
⟨fun ⟨r, hr⟩ ↦ ⟨unop r, congr_arg unop hr⟩, fun ⟨r, hr⟩ ↦ ⟨op r, congr_arg op hr⟩⟩

Premises used: _private.0.isSquare_op_iff.match_1, congr_arg, _private.0.isSquare_op_iff.match_2, Iff.intro, IsSquare, Exists.intro, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
a : αᵐᵒᵖ
⊢ IsSquare (unop a) ↔ IsSquare a

Tactic:
isSquare_op_iff.symm

Premises used: MulOpposite, isSquare_op_iff, MulOpposite.unop, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
a : α
⊢ Even (α := Additive α) ((Additive.ofMul : (a : α) → Additive α) a : Additive α) ↔ IsSquare a

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl, IsSquare
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Mul α
a : Additive α
⊢ IsSquare (α := α) ((Additive.toMul : (a : Additive α) → α) a : α) ↔ Even a

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl, Even
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Add α
a : α
⊢ IsSquare (α := Multiplicative α) ((Multiplicative.ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) ↔ Even a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative, Even
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : Add α
a : Multiplicative α
⊢ Even (α := α) ((Multiplicative.toAdd : (a : Multiplicative α) → α) a : α) ↔ IsSquare a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative, IsSquare
-- Module: Mathlib.Algebra.Group.Even
Goal:
α : Type u_2
inst : MulOneClass α
⊢ IsSquare.{u_2} (α := α) 1

Tactic:
⟨1, (mul_one _).symm⟩

Premises used: IsSquare, Exists.intro, mul_one, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Group.Even
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
a : α
f : F
h : IsSquare a
r : α
h_1 : a = r * r
⊢ (f : (a : α) → β) a = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) r : β) ((f : (a : α) → β) r : β)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Even
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
h : Membership.mem (γ := Set β) {b : β | IsSquare b} b
s : β
h_1 : b = s * s
rcases :
  ∀ (r : α),
    b = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) r : β) ((f : (a : α) → β) r : β) →
      Membership.mem (γ := Set β) (Set.image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {a : α | IsSquare a}) b
⊢ Membership.mem (γ := Set β) (Set.image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {a : α | IsSquare a}) b

Tactic:
rcases hf s with ⟨r, rfl⟩

Premises used: rfl