awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddGroup A
inst_2 : DistribMulAction M A
m : A
a : M
S : AddSubgroup A
⊢ m ∈ a • S ↔ ∃ s ∈ S, a • s = m

Tactic:
(Set.mem_smul_set : m ∈ a • (S : Set A) ↔ _)

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
G : Type u_2
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddGroup A
inst_2 : DistribMulAction M A
a : M
inst_3 : DistribMulAction.{u_3, u_4} Mᵐᵒᵖ A
inst_4 : IsCentralScalar M A
⊢ IsCentralScalar.{u_3, u_4} M (AddSubgroup A)

Tactic:
⟨fun _ S => (congr_arg fun f => S.map f) <| AddMonoidHom.ext <| op_smul_eq_smul _⟩

Premises used: AddMonoidHom.ext, congr_arg, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul, AddSubgroup.map
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S : AddSubgroup A
a : G
x : A
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S : AddSubgroup A
a : G
x : A
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S : AddSubgroup A
a : G
x : A
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S T : AddSubgroup A
a : G
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S T : AddSubgroup A
a : G
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G : Type u_2
A : Type u_4
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
S T : AddSubgroup A
a : G
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubgroup A
x : A
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff₀ ha (S : Set A) x

Premises used: Set.Mem, Set.smul_mem_smul_set_iff₀, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubgroup A
x : A
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set A) x

Premises used: Set.Mem, SetLike.coe, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubgroup A
x : A
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff₀ ha (S : Set A) x

Premises used: Set.mem_inv_smul_set_iff₀, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
S T : AddSubgroup A
a : G₀
ha : a ≠ 0
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff₀ ha

Premises used: Set.smul_set_subset_smul_set_iff₀, Set.Mem, Set.Subset
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
S T : AddSubgroup A
a : G₀
ha : a ≠ 0
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
A : Type u_4
inst : GroupWithZero G₀
inst_1 : AddGroup A
inst_2 : DistribMulAction G₀ A
S T : AddSubgroup A
a : G₀
ha : a ≠ 0
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.subset_smul_set_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
S : Type u_2
inst_2 : SetLike S M₀
inst_3 : MulMemClass S M₀
inst_4 : ZeroMemClass S M₀
s : S
inst_5 : IsLeftCancelMulZero M₀
⊢ IsLeftCancelMulZero.{u_1} ↥s

Tactic:
Subtype.coe_injective.isLeftCancelMulZero Subtype.val rfl fun _ _ => rfl

Premises used: Subtype.coe_injective, Function.Injective.isLeftCancelMulZero, Subtype.val, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
S : Type u_2
inst_2 : SetLike S M₀
inst_3 : MulMemClass S M₀
inst_4 : ZeroMemClass S M₀
s : S
inst_5 : IsRightCancelMulZero M₀
⊢ IsRightCancelMulZero.{u_1} ↥s

Tactic:
Subtype.coe_injective.isRightCancelMulZero Subtype.val rfl fun _ _ => rfl

Premises used: Subtype.coe_injective, Subtype.val, Function.Injective.isRightCancelMulZero, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G →*₀ H
⊢ Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) 0 : H) (0 : H)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G →*₀ H
⊢ Eq.{u_2 + 1} (α := H) (↑0 : H) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
obtain :
  ∀ (y : G) (hy : (f : (a : G) → H) y = (↑x : H)), Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹
⊢ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹

Tactic:
obtain ⟨y, hy⟩ := x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
y : G
hy : (f : (a : G) → H) y = (↑x : H)
h : (f : (a : G) → H) y⁻¹ = (↑x : H)⁻¹
⊢ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) (↑x : H)⁻¹

Tactic:
use y⁻¹
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
y : G
hy : (f : (a : G) → H) y = (↑x : H)
⊢ (f : (a : G) → H) y⁻¹ = (↑x : H)⁻¹

Tactic:
simp [← hy]
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
⊢ Membership.mem (α := H) (γ := Submonoid H) (MonoidHom.mrange f) ((f : (a : G) → H) 1 : H)

Tactic:
simp [- map_one]

Premises used: map_one
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
⊢ Ne.{u_2 + 1} (α := ↥(MonoidHom.mrange f))
    (Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) ((f : (a : G) → H) 0) ⋯ :
      ↥(MonoidHom.mrange f))
    (Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) ((f : (a : G) → H) 1) ⋯ :
      ↥(MonoidHom.mrange f))

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
a : H
ha : Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) a
h : Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha ≠ 0
⊢ ¬a = (↑0 : H)

Tactic:
simp only [ne_eq, Subtype.ext_iff] at h

Premises used: ne_eq, Subtype.ext_iff
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
G : Type u_1
H : Type u_2
inst : GroupWithZero G
inst_1 : GroupWithZero H
f : G →*₀ H
a : H
ha : Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) a
h : ¬a = (↑0 : H)
⊢ Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha *
      Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x)
        (↑(Subtype.mk (p := fun (x : H) ↦ Membership.mem (γ := Submonoid H) (MonoidHom.mrange f) x) a ha) : H)⁻¹ ⋯ =
    1

Tactic:
simpa using mul_inv_cancel₀ h

Premises used: mul_inv_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
H : Type u_2
inst : CommGroupWithZero H
h :
  ∀ (x : H),
    Membership.mem (γ := Submonoid H) (MonoidHom.mker (F := H →*₀ H) MonoidWithZero.inverse) x ↔
      Membership.mem (γ := Submonoid H) ⊥ x
⊢ Eq (α := Submonoid H) (MonoidHom.mker (F := H →*₀ H) MonoidWithZero.inverse) ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances
Goal:
H : Type u_2
inst : CommGroupWithZero H
x : H
⊢ Membership.mem (γ := Submonoid H) (MonoidHom.mker (F := H →*₀ H) MonoidWithZero.inverse) x ↔
    Membership.mem (γ := Submonoid H) ⊥ x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S : Submonoid M
x : M
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff₀ ha (S : Set M) x

Premises used: Set.Mem, Set.smul_mem_smul_set_iff₀, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S : Submonoid M
x : M
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set M) x

Premises used: Set.Mem, SetLike.coe, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S : Submonoid M
x : M
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff₀ ha (S : Set M) x

Premises used: Set.mem_inv_smul_set_iff₀, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S T : Submonoid M
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff₀ ha

Premises used: Set.smul_set_subset_smul_set_iff₀, Set.Mem, Set.Subset
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S T : Submonoid M
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G₀ M
a : G₀
ha : a ≠ 0
S T : Submonoid M
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.subset_smul_set_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
m : M
S : AddSubmonoid A
⊢ (↑(m • S) : Set A) = m • (↑S : Set A)

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
a : A
m : M
S : AddSubmonoid A
⊢ a ∈ S → m • a ∈ m • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set A))

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
a : A
m : M
S : AddSubmonoid A
⊢ a ∈ m • S ↔ ∃ s ∈ S, m • s = a

Tactic:
(Set.mem_smul_set : a ∈ m • (S : Set A) ↔ _)

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
m : M
⊢ HSMul.hSMul (β := AddSubmonoid A) m ⊥ = ⊥

Tactic:
map_bot _

Premises used: AddSubmonoid.map_bot
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
m : M
S T : AddSubmonoid A
⊢ m • (S ⊔ T) = m • S ⊔ m • T

Tactic:
map_sup _ _ _

Premises used: Set.Mem, setOf, AddSubmonoid.map_sup
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
m : M
s : Set A
⊢ HSMul.hSMul (β := AddSubmonoid A) m (closure s) = closure (m • s)

Tactic:
AddMonoidHom.map_mclosure _ _

Premises used: AddMonoid.End.instFunLike._aux_1, AddMonoidHom.map_mclosure
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
inst_3 : DistribMulAction.{u_3, u_4} Mᵐᵒᵖ A
inst_4 : IsCentralScalar M A
⊢ IsCentralScalar.{u_3, u_4} M (AddSubmonoid A)

Tactic:
⟨fun _ S =>
    (congr_arg fun f : AddMonoid.End A => S.map f) <| AddMonoidHom.ext <| op_smul_eq_smul _⟩

Premises used: AddMonoidHom.ext, congr_arg, IsCentralScalar.mk, AddSubmonoid.map, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S : AddSubmonoid A
x : A
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S : AddSubmonoid A
x : A
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S : AddSubmonoid A
x : A
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S T : AddSubmonoid A
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S T : AddSubmonoid A
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G : Type u_2
A : Type u_4
inst : AddMonoid A
inst_1 : Group G
inst_2 : DistribMulAction G A
a : G
S T : AddSubmonoid A
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubmonoid A
x : A
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff₀ ha (S : Set A) x

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.smul_mem_smul_set_iff₀, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubmonoid A
x : A
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set A) x

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, SetLike.coe, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
a : G₀
ha : a ≠ 0
S : AddSubmonoid A
x : A
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff₀ ha (S : Set A) x

Premises used: Set.mem_inv_smul_set_iff₀, AddMonoid.End.instFunLike._aux_1, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
S T : AddSubmonoid A
a : G₀
ha : a ≠ 0
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff₀ ha

Premises used: Set.smul_set_subset_smul_set_iff₀, AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.Subset
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
S T : AddSubmonoid A
a : G₀
ha : a ≠ 0
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff₀ ha

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.Subset, Set.smul_set_subset_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Goal:
G₀ : Type u_1
A : Type u_4
inst : AddMonoid A
inst_1 : GroupWithZero G₀
inst_2 : DistribMulAction G₀ A
S T : AddSubmonoid A
a : G₀
ha : a ≠ 0
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff₀ ha

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, Set.Subset, Set.subset_smul_set_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
⊢ IsMulTorsionFree M

Tactic:
⟨fun n hn x y hxy ↦ ?_⟩

Premises used: IsMulTorsionFree.mk
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
refine :
  ∀ (n : ℕ) (hn : n ≠ 0) (x y : M) (hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)),
    x = y
⊢ IsMulTorsionFree M

Tactic:
refine ⟨fun n hn x y hxy ↦ ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
pos : ∀ (h : x ≠ 0 ∧ y ≠ 0), x = y
neg : ∀ (h : ¬(x ≠ 0 ∧ y ≠ 0)), x = y
⊢ x = y

Tactic:
by_cases h : x ≠ 0 ∧ y ≠ 0
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
h : x ≠ 0 ∧ y ≠ 0
⊢ x = y

Tactic:
ih x h.1 y h.2 n hn hxy

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
h : x ≠ 0 ∧ y ≠ 0
⊢ x = y

Tactic:
exact ih x h.1 y h.2 n hn hxy

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
h : ¬(x ≠ 0 ∧ y ≠ 0)
⊢ IsReduced M

Tactic:
have : IsReduced M := inferInstance
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NoZeroDivisors M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
h : ¬(x ≠ 0 ∧ y ≠ 0)
this : IsReduced M
⊢ x = y

Tactic:
grind [eq_zero_of_pow_eq_zero, zero_pow]

Premises used: eq_zero_of_pow_eq_zero, zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
⊢ IsMulTorsionFree M

Tactic:
.mk' fun x hx y hy n hn hxy ↦ ?_

Premises used: IsMulTorsionFree.mk'
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
refine : ∀ (x : M) (hx : x ≠ 0) (y : M) (hy : y ≠ 0) (n : ℕ) (hn : n ≠ 0) (hxy : x ^ n = y ^ n), x = y
⊢ IsMulTorsionFree M

Tactic:
refine .mk' fun x hx y hy n hn hxy ↦ ?_
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
⊢ normalizedFactors (x ^ n) = normalizedFactors (y ^ n)

Tactic:
have := (Associated.of_eq hxy).normalizedFactors_eq
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors (x ^ n) = normalizedFactors (y ^ n)
rwa : ∀ (this : n • normalizedFactors x = normalizedFactors (y ^ n)), Associated x y
rwa₁ : ∀ (this : n • normalizedFactors x = n • normalizedFactors y), Associated x y
rwa₂ : ∀ (this : normalizedFactors x = normalizedFactors y), Associated x y
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : Associated x y), Associated x y
⊢ Associated x y

Tactic:
rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this

Premises used: UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors, nsmul_right_inj, UniqueFactorizationMonoid.normalizedFactors_pow
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
obtain : ∀ (u : Mˣ) (hu : x * (↑u : M) = y), x = y
⊢ x = y

Tactic:
obtain ⟨u, hu⟩ : Associated x y := by
    have := (Associated.of_eq hxy).normalizedFactors_eq
    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this

Premises used: Associated
-- Module: Mathlib.Algebra.GroupWithZero.Torsion
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : NormalizationMonoid M
inst_3 : IsMulTorsionFree.{u_1} Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * (↑u : M) = y
⊢ IsLeftRegular (x ^ n)

Tactic:
replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n