awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
change : (↑⋯.unit⁻¹ : M) * a = 1
⊢ a⁻¹ * a = 1

Tactic:
change ↑(h a).unit⁻¹ * a = 1

Premises used: IsUnit.unit
-- Module: Mathlib.Algebra.Group.Units.Defs
Goal:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
rw : a = (↑⋯.unit : M) * 1
rw₁ : a = a * 1
rw₂ rw₃ : a = a
⊢ (↑⋯.unit⁻¹ : M) * a = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]

Premises used: mul_one, Units.inv_mul_eq_iff_eq_mul, IsUnit.unit_spec
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_6
inst : Group G
x : Gˣ
simp_rw : (↑x : G) = (MulEquiv.symm toUnits : (a : Gˣ) → G) x
⊢ (toUnits : (a : G) → Gˣ) (↑x : G) = x

Tactic:
simp_rw [MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply]

Premises used: MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
h : M ≃* N
⊢ (mapEquiv h).symm = mapEquiv h.symm

Tactic:
rfl

Premises used: Units.mapEquiv, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
h : M ≃* N
x : Mˣ
⊢ Eq.{u_4 + 1} (α := N) ((↑((mapEquiv h : (a : Mˣ) → Nˣ) x) : N) : N) ((h : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
⊢ Equiv.symm u.mulLeft = u⁻¹.mulLeft

Tactic:
Equiv.ext fun _ => rfl

Premises used: Equiv.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
inst : Monoid M
a : Mˣ
⊢ Function.Bijective (β := M) fun (x : M) ↦ (↑a : M) * x

Tactic:
(mulLeft a).bijective

Premises used: Equiv.bijective, Units.mulLeft
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
inst : Monoid M
u : Mˣ
⊢ Equiv.symm u.mulRight = u⁻¹.mulRight

Tactic:
Equiv.ext fun _ => rfl

Premises used: Equiv.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
M : Type u_3
inst : Monoid M
a : Mˣ
⊢ Function.Bijective (β := M) fun (x : M) ↦ x * (↑a : M)

Tactic:
(mulRight a).bijective

Premises used: Units.mulRight, Equiv.bijective
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Equiv.mulLeft a) : (a : G) → G) fun (x : G) ↦ a * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Equiv.symm (Equiv.mulLeft a)) : (a : G) → G) fun (x : G) ↦ a⁻¹ * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Equiv.symm (Equiv.mulLeft a) = Equiv.mulLeft a⁻¹

Tactic:
ext fun _ => rfl

Premises used: Equiv.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Function.Bijective (β := G) fun (x : G) ↦ a * x

Tactic:
(Equiv.mulLeft a).bijective

Premises used: Equiv.bijective, Equiv.mulLeft
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Equiv.mulRight a) : (a : G) → G) fun (x : G) ↦ x * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Equiv.symm (Equiv.mulRight a) = Equiv.mulRight a⁻¹

Tactic:
ext fun _ => rfl

Premises used: Equiv.ext, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Equiv.symm (Equiv.mulRight a)) : (a : G) → G) fun (x : G) ↦ x * a⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Function.Bijective (β := G) fun (x : G) ↦ x * a

Tactic:
(Equiv.mulRight a).bijective

Premises used: Equiv.bijective, Equiv.mulRight
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst : Group G
a b : G
⊢ (fun (b : G) ↦ b⁻¹ * a) ((fun (b : G) ↦ a / b) b) = b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst : Group G
a b : G
⊢ (fun (b : G) ↦ a / b) ((fun (b : G) ↦ b⁻¹ * a) b) = b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Equiv.divLeft a = Equiv.trans (Equiv.inv G) (Equiv.mulLeft a)

Tactic:
ext fun _ => div_eq_mul_inv _ _

Premises used: Equiv.ext, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst : Group G
a b : G
⊢ (fun (b : G) ↦ b * a) ((fun (b : G) ↦ b / a) b) = b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst : Group G
a b : G
⊢ (fun (b : G) ↦ b / a) ((fun (b : G) ↦ b * a) b) = b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : Group G
a : G
⊢ Equiv.divRight a = Equiv.mulRight a⁻¹

Tactic:
ext fun _ => div_eq_mul_inv _ _

Premises used: Equiv.ext, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : CommGroup G
a : G
⊢ (Equiv.divLeft a).symm = Equiv.divLeft a

Tactic:
ext fun _ ↦ inv_mul_eq_div _ _

Premises used: inv_mul_eq_div, Equiv.ext
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_5
inst : CommGroup G
a : G
⊢ Function.Involutive (α := G) (⇑(Equiv.divLeft a) : (a : G) → G)

Tactic:
fun _ ↦ div_div_cancel ..

Premises used: Function.Involutive, div_div_cancel
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
G : Type u_6
inst : DivisionCommMonoid G
⊢ Eq (α := G ≃* G) (symm (inv G)) (inv G)

Tactic:
rfl

Premises used: MulEquiv.inv, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
x : M
hx : IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) (EquivLike.inv f 1) : N) ((f : (a : M) → N) 1 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
x_1 : M
hx : IsUnit.{u_4} (M := N) ((f : (a : M) → N) x_1 : N)
x y : N
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : M) → N) (OneHom.toFun { toFun := EquivLike.inv f, map_one' := ⋯ : OneHom N M } (x * y)) : N)
    ((f : (a : M) → N)
        (OneHom.toFun { toFun := EquivLike.inv f, map_one' := ⋯ : OneHom N M } x *
          OneHom.toFun { toFun := EquivLike.inv f, map_one' := ⋯ : OneHom N M } y) :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
x : M
hx : IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
⊢ IsUnit x

Tactic:
simpa using hx.map <| MonoidHom.mk ⟨EquivLike.inv f, EquivLike.injective f <| by simp⟩
      fun x y ↦ EquivLike.injective f <| by simp

Premises used: OneHom.mk, MonoidHom.mk, IsUnit.map, EquivLike.injective, EquivLike.inv
-- Module: Mathlib.Algebra.Group.Units.Equiv
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
⊢ ∀ (a : M), IsUnit.{u_4} (M := N) ((f : (a : M) → N) a : N) → IsUnit a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
G : Type u_2
N : Type u_3
inst : DivisionMonoid G
inst_1 : Monoid N
inst_2 : FunLike F G N
inst_3 : MonoidHomClass F G N
x : G
hx : IsUnit x
f g : F
h : Eq.{u_3 + 1} (α := N) ((f : (a : G) → N) x : N) ((g : (a : G) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : G) → N) x⁻¹ : N) ((g : (a : G) → N) x⁻¹ : N)

Tactic:
left_inv_eq_right_inv (map_mul_eq_one f hx.inv_mul_cancel)
    (h.symm ▸ map_mul_eq_one g (hx.mul_inv_cancel))

Premises used: IsUnit.mul_inv_cancel, IsUnit.inv_mul_cancel, Eq.rec, left_inv_eq_right_inv, map_mul_eq_one, Eq.symm
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
G : Type u_2
M : Type u_3
inst : Group G
inst_1 : Monoid M
inst_2 : FunLike F G M
inst_3 : MonoidHomClass F G M
f g : F
x : G
h : Eq.{u_3 + 1} (α := M) ((f : (a : G) → M) x : M) ((g : (a : G) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : G) → M) x⁻¹ : M) ((g : (a : G) → M) x⁻¹ : M)

Tactic:
(Group.isUnit x).eq_on_inv f g h

Premises used: Group.isUnit, IsUnit.eq_on_inv
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
u : Mˣ
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑u : M) : N) ((f : (a : M) → N) u.inv : N) = 1

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
u : Mˣ
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u.inv : N) ((f : (a : M) → N) (↑u : M) : N) = 1

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
x x_1 : Mˣ
⊢ (↑((fun (u : Mˣ) ↦
            ({ val := (f : (a : M) → N) (↑u : M), inv := (f : (a : M) → N) u.inv, val_inv := ⋯, inv_val := ⋯ } : Nˣ))
          (x * x_1)) :
      N) =
    (↑(HMul.hMul (α := Nˣ)
          ((fun (u : Mˣ) ↦
              ({ val := (f : (a : M) → N) (↑u : M), inv := (f : (a : M) → N) u.inv, val_inv := ⋯, inv_val := ⋯ } : Nˣ))
            x)
          ((fun (u : Mˣ) ↦
              ({ val := (f : (a : M) → N) (↑u : M), inv := (f : (a : M) → N) u.inv, val_inv := ⋯, inv_val := ⋯ } : Nˣ))
            x_1)) :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
x : Mˣ
⊢ Eq.{v + 1} (α := N) ((↑((map f : (a : Mˣ) → Nˣ) x) : N) : N) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
u : Mˣ
⊢ Eq.{v + 1} (α := N) ((↑((map f : (a : Mˣ) → Nˣ) u)⁻¹ : N) : N) ((f : (a : M) → N) (↑u⁻¹ : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) val : N) ((f : (a : M) → N) inv : N) = 1

Tactic:
simp [← map_mul, val_inv]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) inv : N) ((f : (a : M) → N) val : N) = 1

Tactic:
simp [← map_mul, inv_val]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ Eq.{v + 1} (α := Nˣ) ((map f : (a : Mˣ) → Nˣ) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } : Nˣ)
    ({ val := (f : (a : M) → N) val, inv := (f : (a : M) → N) inv, val_inv := ⋯, inv_val := ⋯ } : Nˣ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : N →* P
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: rfl, Units.map
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Injective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
fun _ _ e => ext (hf (congr_arg val e))

Premises used: Units.val, Units.ext, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Bijective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
⟨map_injective hf.injective, ?_⟩

Premises used: Units.map_injective, Function.Bijective.injective, And.intro, Function.Bijective
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
refine : Surjective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)
⊢ Bijective.{u + 1, v + 1} (α := Mˣ) (β := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
refine ⟨map_injective hf.injective, ?_⟩
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
u v : N
uv : u * v = 1
vu : v * u = 1
rcases :
  ∀ (u v : M) (uv : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u : N) ((f : (a : M) → N) v : N) = 1)
    (vu : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) v : N) ((f : (a : M) → N) u : N) = 1),
    ∃ (a : Mˣ),
      Eq.{v + 1} (α := Nˣ) ((map f : (a : Mˣ) → Nˣ) a : Nˣ)
        ({ val := (f : (a : M) → N) u, inv := (f : (a : M) → N) v, val_inv := uv, inv_val := vu } : Nˣ)
⊢ ∃ (a : Mˣ), (map f : (a : Mˣ) → Nˣ) a = { val := u, inv := v, val_inv := uv, inv_val := vu : Nˣ }

Tactic:
rcases hf.surjective u, hf.surjective v with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩

Premises used: Function.Bijective.surjective, rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
u v : M
uv : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u : N) ((f : (a : M) → N) v : N) = 1
vu : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) v : N) ((f : (a : M) → N) u : N) = 1
⊢ Eq.{v + 1} (α := N) ((f : (a : M) → N) (u * v) : N) ((f : (a : M) → N) 1 : N)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
u v : M
uv : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u : N) ((f : (a : M) → N) v : N) = 1
vu : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) v : N) ((f : (a : M) → N) u : N) = 1
⊢ Eq.{v + 1} (α := N) ((f : (a : M) → N) (v * u) : N) ((f : (a : M) → N) 1 : N)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : Bijective.{u + 1, v + 1} (α := M) (β := N) (⇑f : (a : M) → N)
u v : M
uv : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) u : N) ((f : (a : M) → N) v : N) = 1
vu : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) v : N) ((f : (a : M) → N) u : N) = 1
⊢ ∃ (a : Mˣ),
    Eq.{v + 1} (α := Nˣ) ((map f : (a : Mˣ) → Nˣ) a : Nˣ)
      ({ val := (f : (a : M) → N) u, inv := (f : (a : M) → N) v, val_inv := uv, inv_val := vu } : Nˣ)

Tactic:
exact ⟨⟨u, v, hf.injective <| by simpa, hf.injective <| by simpa⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
inst : Monoid M
h :
  ∀ (x : Mˣ),
    Eq.{u + 1} (α := M) (↑((map (MonoidHom.id M) : (a : Mˣ) → Mˣ) x) : M) (↑((MonoidHom.id Mˣ : (a : Mˣ) → Mˣ) x) : M)
⊢ Eq (α := Mˣ →* Mˣ) (map (MonoidHom.id M)) (MonoidHom.id Mˣ)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
inst : Monoid M
x : Mˣ
⊢ Eq.{u + 1} (α := M) (↑((map (MonoidHom.id M) : (a : Mˣ) → Mˣ) x) : M) (↑((MonoidHom.id Mˣ : (a : Mˣ) → Mˣ) x) : M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
inst : Monoid M
x : Mˣ
⊢ (coeHom M : (a : Mˣ) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
inst : Monoid M
⊢ Injective (α := Mˣ) (β := M) (⇑(coeHom M) : (a : Mˣ) → M)

Tactic:
Units.val_injective

Premises used: Units.val_injective
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
α : Type u_1
inst : DivisionMonoid α
⊢ ∀ (u : αˣ) (n : ℤ), (↑(u ^ n) : α) = (↑u : α) ^ n

Tactic:
(Units.coeHom α).map_zpow

Premises used: Units.coeHom, MonoidHom.map_zpow
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
inst : Monoid M
α : Type u_1
inst_1 : DivisionMonoid α
F : Type u_2
inst_2 : FunLike F M α
inst_3 : MonoidHomClass F M α
f : F
u : Mˣ
⊢ Eq.{u_1 + 1} (α := α) ((f : (a : M) → α) (↑u⁻¹ : M) : α) (((f : (a : M) → α) (↑u : M))⁻¹ : α)

Tactic:
((f : M →* α).comp (Units.coeHom M)).map_inv u

Premises used: Units.coeHom, MonoidHomClass.toMonoidHom, MonoidHom.comp, MonoidHom.map_inv
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
huv : (↑(g 1) : N) = (↑1 : N)
⊢ g 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
huv : Eq.{v + 1} (α := N) ((f : (a : M) → N) 1 : N) ((↑1 : N) : N)
⊢ (↑(g 1) : N) = (↑1 : N)

Tactic:
rw [h 1]

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
⊢ Eq.{v + 1} (α := N) ((f : (a : M) → N) 1 : N) ((↑1 : N) : N)

Tactic:
f.map_one

Premises used: MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
⊢ Eq.{v + 1} (α := N) ((f : (a : M) → N) 1 : N) ((↑1 : N) : N)

Tactic:
exact f.map_one

Premises used: MonoidHom.map_one
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
P : Type w
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x y : M
⊢ (↑(g (x * y)) : N) = (↑(g x * g y) : N)

Tactic:
simp only [h, val_mul, f.map_mul]

Premises used: MonoidHom.map_mul, Units.val_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
⊢ Eq.{v + 1} (α := N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N) ((f : (a : M) → N) x : N)

Tactic:
h x
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) 1 (↑((liftRight f g h : (a : M) → Nˣ) x) : N)
rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
rw₂ rw₃ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) = 1

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]

Premises used: Units.coe_liftRight, Units.mul_inv_eq_iff_eq_mul, one_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), (↑(g x) : N) = (f : (a : M) → N) x
x : M
rw : (f : (a : M) → N) x = HMul.hMul (α := N) (↑((liftRight f g h : (a : M) → Nˣ) x) : N) 1
rw₁ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((↑((liftRight f g h : (a : M) → Nˣ) x) : N) : N)
rw₂ rw₃ : Eq.{v + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
⊢ HMul.hMul (α := N) (β := N) ((↑((liftRight f g h : (a : M) → Nˣ) x)⁻¹ : N) : N) ((f : (a : M) → N) x : N) = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

Premises used: Units.coe_liftRight, mul_one, Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Monoid M
f : G →* M
g : G
⊢ Eq.{u_2 + 1} (α := M) ((↑((f.toHomUnits : (a : G) → Mˣ) g) : M) : M) ((f : (a : G) → M) g : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommMonoid M
f g : G →* M
h :
  ∀ (x : G),
    Eq.{u_2 + 1} (α := M) (↑(((f * g).toHomUnits : (a : G) → Mˣ) x) : M)
      (↑((f.toHomUnits * g.toHomUnits : (a : G) → Mˣ) x) : M)
⊢ (f * g).toHomUnits = f.toHomUnits * g.toHomUnits

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommMonoid M
f g : G →* M
x : G
⊢ Eq.{u_2 + 1} (α := M) (↑(((f * g).toHomUnits : (a : G) → Mˣ) x) : M)
    (↑((f.toHomUnits * g.toHomUnits : (a : G) → Mˣ) x) : M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommMonoid M
⊢ ∀ (x y : G →* M), (x * y).toHomUnits = x.toHomUnits * y.toHomUnits

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
rcases : ∀ (y : Mˣ), IsUnit.{u_4} (M := N) ((f : (a : M) → N) (↑y : M) : N)
⊢ IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)

Tactic:
rcases h with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit.{u_4} (M := N) ((f : (a : M) → N) (↑y : M) : N)

Tactic:
(Units.map (f : M →* N) y).isUnit

Premises used: MonoidHomClass.toMonoidHom, Units.isUnit, DFunLike.coe, Units.map
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit.{u_4} (M := N) ((f : (a : M) → N) (↑y : M) : N)

Tactic:
exact (Units.map (f : M →* N) y).isUnit

Premises used: MonoidHomClass.toMonoidHom, Units.isUnit, DFunLike.coe, Units.map
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ (↑(IsUnit.unit (a := (f : (a : M) → N) x) ⋯) : N) = (f : (a : M) → N) (↑h.unit : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ HMul.hMul (α := N) ((f : (a : M) → N) (↑h.unit⁻¹ : M) : N) (↑(IsUnit.unit (a := (f : (a : M) → N) x) ⋯) : N) = 1

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : FunLike G N M
inst_2 : Monoid M
inst_3 : Monoid N
inst_4 : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑g : (a : N) → M) (⇑f : (a : M) → N)
h : IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
⊢ IsUnit x

Tactic:
simpa only [hfg x] using h.map g

Premises used: IsUnit.map
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst : FunLike F M N
inst_1 : FunLike G N M
inst_2 : Monoid M
inst_3 : Monoid N
inst_4 : MonoidHomClass F M N
inst_5 : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑g : (a : N) → M) (⇑f : (a : M) → N)
⊢ IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N) ↔ IsUnit x

Tactic:
⟨of_leftInverse g hfg, map _⟩

Premises used: IsUnit.of_leftInverse, Iff.intro, IsUnit.map