awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : ∀ (x : M), IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
x : M
⊢ Eq.{u_4 + 1} (α := N) ((↑((liftRight f hf : (a : M) → Nˣ) x) : N) : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
x x_1 : M
⊢ (↑⋯.unit : N) = (f : (a : M) → N) x_1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
f : M →* N
hf : ∀ (x : M), IsUnit.{u_4} (M := N) ((f : (a : M) → N) x : N)
x : M
⊢ (liftRight f hf : (a : M) → Nˣ) x = ⋯.unit

Tactic:
rfl

Premises used: Units.copy, IsUnit.unit, rfl
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
R : Type u_2
S : Type u_3
F : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : FunLike F R S
f : F
inst_3 : IsLocalHom.{u_2, u_3, u_5} (R := R) (S := S) f
a : R
h : IsUnit.{u_3} (M := S) ((f : (a : R) → S) a : S)
⊢ IsUnit a

Tactic:
IsLocalHom.map_nonunit a h

Premises used: IsLocalHom.map_nonunit
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
R : Type u_2
S : Type u_3
F : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
inst_4 : IsLocalHom.{u_2, u_3, u_5} (R := R) (S := S) f
a : R
⊢ IsUnit.{u_3} (M := S) ((f : (a : R) → S) a : S) ↔ IsUnit a

Tactic:
⟨IsLocalHom.map_nonunit a, IsUnit.map f⟩

Premises used: IsLocalHom.map_nonunit, Iff.intro, IsUnit.map
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
G : Type u_1
R : Type u_2
S : Type u_3
F : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
inst_4 : FunLike G S R
inst_5 : MonoidHomClass G S R
f : F
g : G
hfg : LeftInverse.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_3} (M := S) ((f : (a : R) → S) a : S)
rwa rwa₁ rwa₂ rwa₃ : ∀ (ha : IsUnit a), IsUnit a
⊢ IsUnit a

Tactic:
rwa [isUnit_map_of_leftInverse g hfg] at ha

Premises used: isUnit_map_of_leftInverse
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
R : Type u_2
S : Type u_3
F : Type u_5
inst : Monoid R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
inst_4 : IsLocalHom.{u_2, u_3, u_5} (R := R) (S := S) f
⊢ IsLocalHom (R := R) (S := S) (F := R →* S) (↑f : R →* S)

Tactic:
⟨IsLocalHom.map_nonunit (f := f)⟩

Premises used: IsLocalHom.map_nonunit, IsLocalHom.mk
-- Module: Mathlib.Algebra.Group.Units.Hom
Goal:
R : Type u_2
S : Type u_3
T : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
f : R →* S
g : S →* T
inst_3 : IsLocalHom (R := R) (S := T) (g.comp f)
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (ha.map g)⟩

Premises used: IsLocalHom.mk, MonoidHom.comp, isUnit_map_iff, Iff.mp, IsUnit.map
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
u : Mᵐᵒᵖˣ
⊢ (↑(unop ((opEquiv : (a : Mᵐᵒᵖˣ) → Mˣᵐᵒᵖ) u)) : M) = unop (↑u : Mᵐᵒᵖ)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
u : Mˣᵐᵒᵖ
⊢ (↑((MulEquiv.symm opEquiv : (a : Mˣᵐᵒᵖ) → Mᵐᵒᵖˣ) u) : Mᵐᵒᵖ) = op (↑(unop u) : M)

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
m : M
h : IsUnit m
⊢ IsUnit (MulOpposite.op m)

Tactic:
let ⟨u, hu⟩ := h
  hu ▸ ⟨Units.opEquiv.symm (op u), rfl⟩

Premises used: IsUnit, _private.0.IsUnit.op.match_1, Eq.rec, Units.opEquiv, Exists.intro, MulEquiv.symm, DFunLike.coe, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
m : Mᵐᵒᵖ
h : IsUnit m
⊢ IsUnit (MulOpposite.unop m)

Tactic:
let ⟨u, hu⟩ := h
  hu ▸ ⟨unop (Units.opEquiv u), rfl⟩

Premises used: IsUnit, Eq.rec, Units.opEquiv, Exists.intro, MulOpposite.unop, DFunLike.coe, rfl, _private.0.IsUnit.unop.match_1
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
m : M
⊢ IsUnit (op m) ↔ IsUnit m

Tactic:
⟨IsUnit.unop, IsUnit.op⟩

Premises used: Iff.intro, IsUnit.op, IsUnit.unop
-- Module: Mathlib.Algebra.Group.Units.Opposite
Goal:
M : Type u_2
inst : Monoid M
m : Mᵐᵒᵖ
⊢ IsUnit (unop m) ↔ IsUnit m

Tactic:
⟨IsUnit.op, IsUnit.unop⟩

Premises used: Iff.intro, IsUnit.op, IsUnit.unop
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : InvolutiveInv α
a : WithOne α
simp_rw : Option.map id a = a
simp_rw₁ : id a = a
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a

Tactic:
simp_rw [inv_comp_inv, Option.map_id, id]

Premises used: id, inv_comp_inv, Option.map_id
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) (1 * y) =
    HMul.hMul (α := β) (β := β) (recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) 1 : β)
      (recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) y : β)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : MulOneClass β
f : α →ₙ* β
x_1 y : WithOne α
x : α
⊢ recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) ((↑x : WithOne α) * 1) =
    HMul.hMul (α := β) (β := β)
      (recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) (↑x : WithOne α) : β)
      (recOneCoe (motive := fun (x : WithOne α) ↦ β) 1 (⇑f : (a : α) → β) 1 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : MulOneClass β
f : α →ₙ* β
x : α
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α →ₙ* β) → WithOne α →* β) f : MonoidHom.{u, v} (WithOne α) β) : (a : WithOne α) → β)
        (↑x : WithOne α) :
      β)
    ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: WithOne.recOneCoe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : MulOneClass β
f : α →ₙ* β
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α →ₙ* β) → WithOne α →* β) f : MonoidHom.{u, v} (WithOne α) β) : (a : WithOne α) → β) 1 : β) (1 : β)

Tactic:
rfl

Premises used: WithOne.recOneCoe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : MulOneClass β
f : MonoidHom.{u, v} (WithOne α) β
⊢ f = (lift : (a : α →ₙ* β) → WithOne α →* β) ((↑f : WithOne α →ₙ* β).comp coeMulHom)

Tactic:
(lift.apply_symm_apply f).symm

Premises used: Equiv.apply_symm_apply, WithOne.lift, Eq.symm
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : MulOneClass β
f : MonoidHom.{u, v} (WithOne α) β
x : α
⊢ Eq.{v + 1} (α := β) ((((Equiv.symm lift : (a : WithOne α →* β) → α →ₙ* β) f : α →ₙ* β) : (a : α) → β) x : β)
    ((f : (a : WithOne α) → β) (↑x : WithOne α) : β)

Tactic:
rfl

Premises used: WithOne.coe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : Mul β
f : α →ₙ* β
a : α
⊢ Eq.{v + 1} (α := WithOne β) ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a : WithOne α) : WithOne β)
    ((↑((f : (a : α) → β) a) : WithOne β) : WithOne β)

Tactic:
rfl

Premises used: WithOne.coe, WithOne.recOneCoe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
inst : Mul α
h :
  ∀ (x : WithOne α),
    Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) x : WithOne α)
      ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) x : WithOne α)
⊢ Eq (α := WithOne α →* WithOne α) (mapMulHom (MulHom.id α)) (MonoidHom.id (WithOne α))

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
inst : Mul α
x : WithOne α
h :
  Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
h₁ :
  ∀ (a : α),
    Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)
      ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)
⊢ Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) x : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) x : WithOne α)

Tactic:
induction x
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
inst : Mul α
⊢ Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) 1 : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) 1 : WithOne α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
inst : Mul α
a : α
⊢ Eq (α := WithOne α) ((mapMulHom (MulHom.id α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)
    ((MonoidHom.id (WithOne α) : (a : WithOne α) → WithOne α) (↑a : WithOne α) : WithOne α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : Mul β
f : α →ₙ* β
hf : Function.Injective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : α
H :
  Eq.{v + 1} (α := WithOne β) ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a₁ : WithOne α) : WithOne β)
    ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a₂ : WithOne α) : WithOne β)
⊢ (↑a₁ : WithOne α) = (↑a₂ : WithOne α)

Tactic:
simpa [hf.eq_iff] using H

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : Mul β
f g : α →ₙ* β
h : mapMulHom f = mapMulHom g
x : α
⊢ Eq.{v + 1} (α := WithOne β) ((↑((f : (a : α) → β) x) : WithOne β) : WithOne β)
    ((↑((g : (a : α) → β) x) : WithOne β) : WithOne β)

Tactic:
simp only [← mapMulHom_coe, h]

Premises used: WithOne.mapMulHom_coe
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : Mul β
f g : α →ₙ* β
⊢ mapMulHom f = mapMulHom g ↔ f = g

Tactic:
mapMulHom_injective'.eq_iff

Premises used: Function.Injective.eq_iff, WithOne.mapMulHom_injective'
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
one :
  Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) 1) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) 1 : WithOne γ)
coe :
  ∀ (a : α),
    Eq.{w + 1} (α := WithOne γ)
      ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a : WithOne α)) :
        WithOne γ)
      ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) (↑a : WithOne α) : WithOne γ)
⊢ Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) x) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) x : WithOne γ)

Tactic:
induction x
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) 1) : WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) 1 : WithOne γ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a : α
⊢ Eq.{w + 1} (α := WithOne γ)
    ((mapMulHom g : (a : WithOne β) → WithOne γ) ((mapMulHom f : (a : WithOne α) → WithOne β) (↑a : WithOne α)) :
      WithOne γ)
    ((mapMulHom (g.comp f) : (a : WithOne α) → WithOne γ) (↑a : WithOne α) : WithOne γ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f)

Tactic:
MonoidHom.ext fun x => (mapMulHom_mapMulHom f g x).symm

Premises used: MonoidHom.ext, WithOne.mapMulHom_mapMulHom, Eq.symm
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
inst : Mul α
⊢ Eq (α := WithOne α ≃* WithOne α) (MulEquiv.withOneCongr (MulEquiv.refl α)) (MulEquiv.refl (WithOne α))

Tactic:
MulEquiv.toMonoidHom_injective mapMulHom_id

Premises used: WithOne.mapMulHom_id, MulEquiv.toMonoidHom_injective
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : Mul β
e : α ≃* β
⊢ e.withOneCongr.symm = e.symm.withOneCongr

Tactic:
rfl

Premises used: MulEquiv.withOneCongr, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Mul α
inst_1 : Mul β
inst_2 : Mul γ
e₁ : α ≃* β
e₂ : β ≃* γ
⊢ e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr

Tactic:
MulEquiv.toMonoidHom_injective (mapMulHom_comp _ _).symm

Premises used: WithOne.mapMulHom_comp, MulEquiv.toMonoidHom_injective, Eq.symm
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Nonempty α
⊢ Nontrivial.{u} (WithOne α)

Tactic:
Option.nontrivial

Premises used: WithOne, Option.nontrivial
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
p : WithOne α → Prop
⊢ (∀ (x : WithOne α), p x) ↔ p 1 ∧ ∀ (a : α), p (↑a : WithOne α)

Tactic:
Option.forall

Premises used: WithOne, Option.forall, WithOne.coe
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
p : WithOne α → Prop
⊢ (∃ (x : WithOne α), p x) ↔ p 1 ∨ ∃ (a : α), p (↑a : WithOne α)

Tactic:
Option.exists

Premises used: WithOne, WithOne.coe, Option.exists
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
motive : WithOne α → Sort u_1
h₁ : motive 1
h₂ : (a : α) → motive (↑a : WithOne α)
⊢ recOneCoe (motive := fun (x : WithOne α) ↦ motive x) h₁ h₂ 1 = h₁

Tactic:
rfl

Premises used: WithOne.recOneCoe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
motive : WithOne α → Sort u_1
h₁ : motive 1
h₂ : (a : α) → motive (↑a : WithOne α)
a : α
⊢ recOneCoe (motive := fun (x : WithOne α) ↦ motive x) h₁ h₂ (↑a : WithOne α) = h₂ a

Tactic:
rfl

Premises used: WithOne.recOneCoe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
x : α
hx : (↑x : WithOne α) ≠ 1
⊢ unone hx = x

Tactic:
rfl

Premises used: WithOne.unone, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
a : α
⊢ (↑a : WithOne α) ≠ 1

Tactic:
Option.some_ne_none a

Premises used: WithOne, WithOne.coe, Option.some_ne_none
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
a : α
⊢ 1 ≠ (↑a : WithOne α)

Tactic:
coe_ne_one.symm

Premises used: Ne.symm, WithOne.coe_ne_one
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
x : WithOne α
⊢ x ≠ 1 ↔ ∃ (a : α), (↑a : WithOne α) = x

Tactic:
Option.ne_none_iff_exists

Premises used: WithOne, Option.ne_none_iff_exists, WithOne.coe
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
a b : α
⊢ (↑a : WithOne α) = (↑b : WithOne α) ↔ a = b

Tactic:
Option.some_inj

Premises used: WithOne, WithOne.coe, Option.some_inj
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := α) coe

Tactic:
Option.some_injective _

Premises used: WithOne, WithOne.coe, Option.some_injective
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
P : WithOne α → Prop
⊢ ∀ (x : WithOne α), P 1 → (∀ (a : α), P (↑a : WithOne α)) → P x

Tactic:
Option.casesOn

Premises used: WithOne, Option.casesOn, WithOne.coe
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Mul α
a b : α
⊢ (↑(a * b) : WithOne α) = (↑a : WithOne α) * (↑b : WithOne α)

Tactic:
rfl

Premises used: Option.merge, WithOne.coe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Semigroup α
b c : WithOne α
⊢ 1 * b * c = 1 * (b * c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Semigroup α
a : α
c : WithOne α
⊢ (↑a : WithOne α) * 1 * c = (↑a : WithOne α) * (1 * c)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Semigroup α
a b : α
⊢ (↑a : WithOne α) * (↑b : WithOne α) * 1 = (↑a : WithOne α) * ((↑b : WithOne α) * 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Semigroup α
a b c : α
simp_rw : (↑(a * b * c) : WithOne α) = (↑(a * (b * c)) : WithOne α)
⊢ (↑a : WithOne α) * (↑b : WithOne α) * (↑c : WithOne α) = (↑a : WithOne α) * ((↑b : WithOne α) * (↑c : WithOne α))

Tactic:
simp_rw [← coe_mul, mul_assoc]

Premises used: mul_assoc, WithOne.coe_mul
-- Module: Mathlib.Algebra.Group.WithOne.Defs
Goal:
α : Type u
inst : Inv α
a : α
⊢ (↑a⁻¹ : WithOne α) = (↑a : WithOne α)⁻¹

Tactic:
rfl

Premises used: WithOne.coe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f 1 = 1

Tactic:
rfl

Premises used: WithOne.map, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f (↑a : WithOne α) = (↑(f a) : WithOne β)

Tactic:
rfl

Premises used: WithOne.map, WithOne.coe, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : β
⊢ map₂ f (↑a : WithOne α) (↑b : WithOne β) = (↑(f a b) : WithOne γ)

Tactic:
rfl

Premises used: WithOne.map₂, WithOne.coe, rfl, Option.map₂
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : WithOne β
⊢ map₂ f 1 b = 1

Tactic:
rfl

Premises used: WithOne.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
one : map₂ f 1 1 = 1
coe : ∀ (a : α), map₂ f (↑a : WithOne α) 1 = 1
⊢ map₂ f a 1 = 1

Tactic:
cases a
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f 1 1 = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
⊢ map₂ f (↑a : WithOne α) 1 = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : WithOne β
⊢ map₂ f (↑a : WithOne α) b = map (fun (b : β) ↦ f a b) b

Tactic:
rfl

Premises used: WithOne.map₂, WithOne.map, rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : β
one : map₂ f 1 (↑b : WithOne β) = map (fun (x : α) ↦ f x b) 1
coe : ∀ (a : α), map₂ f (↑a : WithOne α) (↑b : WithOne β) = map (fun (x : α) ↦ f x b) (↑a : WithOne α)
⊢ map₂ f a (↑b : WithOne β) = map (fun (x : α) ↦ f x b) a

Tactic:
cases a
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f 1 (↑b : WithOne β) = map (fun (x : α) ↦ f x b) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a : α
⊢ map₂ f (↑a : WithOne α) (↑b : WithOne β) = map (fun (x : α) ↦ f x b) (↑a : WithOne α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.WithOne.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : WithOne β
⊢ map₂ f a b = 1 ↔ a = 1 ∨ b = 1

Tactic:
Option.map₂_eq_none_iff

Premises used: WithOne, WithOne.map₂, Option.map₂_eq_none_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G₀ : Type u_2
α : Type u_8
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
a : G₀
ha : a ≠ 0
⊢ Bijective (β := α) fun (x : α) ↦ a • x

Tactic:
MulAction.bijective <| Units.mk0 a ha

Premises used: MulAction.bijective, Units.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G₀ : Type u_2
α : Type u_8
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
a : G₀
ha : a ≠ 0
⊢ Injective (β := α) fun (x : α) ↦ a • x

Tactic:
(MulAction.bijective₀ ha).injective

Premises used: Function.Bijective.injective, MulAction.bijective₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G₀ : Type u_2
α : Type u_8
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
a : G₀
ha : a ≠ 0
⊢ Surjective (β := α) fun (x : α) ↦ a • x

Tactic:
(MulAction.bijective₀ ha).surjective

Premises used: MulAction.bijective₀, Function.Bijective.surjective
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
R : Type u_7
inst : Group G
inst_1 : Monoid R
inst_2 : AddGroup R
inst_3 : DistribMulAction G R
inst_4 : IsScalarTower G R R
inst_5 : SMulCommClass G R R
r : G
a : R
rw : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (r • (1 - r⁻¹ • a))
rw₁ : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (HSMul.hSMul (β := R) r 1 - r • r⁻¹ • a)
rw₂ rw₃ : IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (HSMul.hSMul (β := R) r 1 - a)
⊢ IsUnit (HSMul.hSMul (β := R) r 1 - a) ↔ IsUnit (1 - r⁻¹ • a)

Tactic:
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

Premises used: HSub.hSub, smul_inv_smul, isUnit_smul_iff, smul_sub, Inv.inv, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
x : G
⊢ HSMul.hSMul (β := G₀) x 0 = 0

Tactic:
simpa using (smul_assoc x (0 : G₀) (0 : G₀)).symm

Premises used: smul_assoc, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
⊢ ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0

Tactic:
have (x : G) : x • (0 : G₀) = 0 := by simpa using (smul_assoc x (0 : G₀) (0 : G₀)).symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
pos : ∀ (hb : b = 0), (g / h) • (a / b) = g • a / h • b
neg : ∀ (hb : ¬b = 0), (g / h) • (a / b) = g • a / h • b
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : b = 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
simp [hb, this]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
⊢ h • b ≠ 0

Tactic:
(ne_of_apply_ne (h⁻¹ • ·) ?_)

Premises used: ne_of_apply_ne, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
refine : Ne.{u_2 + 1} (α := G₀) ((fun (x : G₀) ↦ h⁻¹ • x) (h • b)) ((fun (x : G₀) ↦ h⁻¹ • x) 0)
⊢ h • b ≠ 0

Tactic:
refine (ne_of_apply_ne (h⁻¹ • ·) ?_)

Premises used: ne_of_apply_ne, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
⊢ Ne.{u_2 + 1} (α := G₀) ((fun (x : G₀) ↦ h⁻¹ • x) (h • b)) ((fun (x : G₀) ↦ h⁻¹ • x) 0)

Tactic:
simpa [this]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
⊢ h • b ≠ 0

Tactic:
have : h • b ≠ 0 := by
    refine (ne_of_apply_ne (h⁻¹ • ·) ?_)
    simpa [this]