awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx_1 : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
hx :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x_1 : A),
        Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x_1 : B) (0 : B) ∧
          HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1
some :
  ∀ (r : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (s : A)
    (hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B))
    (hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s),
    Option.some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) = 0 ∨
      ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
        Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
        Option.some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) =
          (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
⊢ Option.some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      Option.some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx_1) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))

Tactic:
obtain ⟨r, hr, s, hs, hrs⟩ := hx
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
simp :
  x =
    HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r) hr)⁻¹ : Bˣ)
      (Units.mk0 ((f : (a : A) → B) s) hs : Bˣ)
⊢ Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx = valueGroup.mk f r s hr hs

Tactic:
simp only [valueGroup.mk, Subtype.mk.injEq]

Premises used: MonoidWithZeroHom.valueGroup.mk, Subtype.mk.injEq
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
rw : HMul.hMul (α := Bˣ) (Units.mk0 ((f : (a : A) → B) r) hr : Bˣ) x = Units.mk0 ((f : (a : A) → B) s) hs
⊢ x =
    HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r) hr)⁻¹ : Bˣ)
      (Units.mk0 ((f : (a : A) → B) s) hs : Bˣ)

Tactic:
rw [eq_inv_mul_iff_mul_eq]

Premises used: eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
⊢ HMul.hMul (α := Bˣ) (Units.mk0 ((f : (a : A) → B) r) hr : Bˣ) x = Units.mk0 ((f : (a : A) → B) s) hs

Tactic:
simp [← hrs, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : Bˣ
hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x
r : A
hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)
s : A
hs : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)
hrs : HMul.hMul (α := B) ((f : (a : A) → B) r : B) (↑x : B) = (f : (a : A) → B) s
⊢ some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) = 0 ∨
    ∃ (r : A) (s : A) (hr : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) r : B) (0 : B)) (hs :
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) s : B) (0 : B)),
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) x hx) =
        (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))

Tactic:
refine .inr ⟨r, s, hr, hs, Option.some_inj.mpr <| by
      simp only [valueGroup.mk, Subtype.mk.injEq]
      rw [eq_inv_mul_iff_mul_eq]
      simp [← hrs, mul_comm]⟩
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : CommGroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
⊢ x = 0 ∨
    ∃ (d :
      { xy : A × A //
        Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) xy.1 : B) (0 : B) ∧
          Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) xy.2 : B) (0 : B) }),
      x = (↑(valueGroup.mk f (↑d : A × A).1 (↑d : A × A).2 ⋯ ⋯) : WithZero ↥(valueGroup f))

Tactic:
x.zero_or_exists_mk.imp _root_.id fun ⟨r, s, hr, hs, hx⟩ ↦ ⟨⟨(r, s), ⟨hr, hs⟩⟩, hx⟩

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, id, Or.imp
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
h : IsLeftRegular.{u_1} (R := R) 0
⊢ Subsingleton R

Tactic:
⟨fun a b => h <| Eq.trans (zero_mul a) (zero_mul b).symm⟩

Premises used: MulZeroClass.zero_mul, Subsingleton.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
h : IsRightRegular.{u_1} (R := R) 0
⊢ Subsingleton R

Tactic:
⟨fun a b => h <| Eq.trans (mul_zero a) (mul_zero b).symm⟩

Premises used: MulZeroClass.mul_zero, Subsingleton.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
h : IsRegular.{u_1} (R := R) 0
⊢ Subsingleton R

Tactic:
h.left.subsingleton

Premises used: IsLeftRegular.subsingleton, IsRegular.left
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ IsLeftRegular.{u_1} (R := R) 0 ↔ Subsingleton R

Tactic:
⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩

Premises used: IsLeftRegular.subsingleton, Iff.intro, Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
rw : (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y
⊢ ¬IsLeftRegular.{u_1} (R := R) 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]

Premises used: isLeftRegular_zero_iff_subsingleton, subsingleton_iff, nontrivial_iff, not_iff_comm
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
push : (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
⊢ (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ IsRightRegular.{u_1} (R := R) 0 ↔ Subsingleton R

Tactic:
⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩

Premises used: Iff.intro, IsRightRegular.subsingleton, Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
rw : (¬∃ (x : R), ∃ (y : R), x ≠ y) ↔ ∀ (x y : R), x = y
⊢ ¬IsRightRegular.{u_1} (R := R) 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]

Premises used: subsingleton_iff, nontrivial_iff, isRightRegular_zero_iff_subsingleton, not_iff_comm
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
⊢ IsRegular.{u_1} (R := R) 0 ↔ Subsingleton R

Tactic:
⟨fun h => h.left.subsingleton, fun h =>
    ⟨isLeftRegular_zero_iff_subsingleton.mpr h, isRightRegular_zero_iff_subsingleton.mpr h⟩⟩

Premises used: Iff.mpr, isLeftRegular_zero_iff_subsingleton, IsLeftRegular.subsingleton, IsRegular.mk, Iff.intro, IsRegular.left, isRightRegular_zero_iff_subsingleton
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
rcases : ∀ (x y : R) (xy : x ≠ y), False
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
xy (la ?_)
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
refine : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ 0 * x) x) ((fun (x : R) ↦ 0 * x) y)
⊢ False

Tactic:
refine xy (la ?_)
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
la : IsLeftRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ 0 * x) x) ((fun (x : R) ↦ 0 * x) y)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
rcases : ∀ (x y : R) (xy : x ≠ y), False
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
xy (ra ?_)
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
refine : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * 0) x) ((fun (x : R) ↦ x * 0) y)
⊢ False

Tactic:
refine xy (ra ?_)
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
ra : IsRightRegular.{u_1} (R := R) 0
x y : R
xy : x ≠ y
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * 0) x) ((fun (x : R) ↦ x * 0) y)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a : R
inst_1 : Nontrivial R
la : IsRegular a
⊢ a ≠ 0

Tactic:
la.left.ne_zero

Premises used: IsLeftRegular.ne_zero, IsRegular.left
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
nR : Nontrivial R
⊢ ¬IsLeftRegular.{u_1} (R := R) 0

Tactic:
not_isLeftRegular_zero_iff.mpr nR

Premises used: Iff.mpr, not_isLeftRegular_zero_iff
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
nR : Nontrivial R
⊢ ¬IsRightRegular.{u_1} (R := R) 0

Tactic:
not_isRightRegular_zero_iff.mpr nR

Premises used: Iff.mpr, not_isRightRegular_zero_iff
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : Nontrivial R
⊢ ¬IsRegular.{u_1} (R := R) 0

Tactic:
fun h => IsRegular.ne_zero h rfl

Premises used: IsRegular.ne_zero, Not, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
rw : b * a = b * 0
| b * a = 0

Tactic:
rw [← mul_zero b]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
conv_lhs : b * a = b * 0 ↔ a = 0
⊢ b * a = 0 ↔ a = 0

Tactic:
conv_lhs => rw [← mul_zero b]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
rw rw₁ : b * 0 = b * 0
⊢ b * a = b * 0

Tactic:
rw [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
rw : a * b = 0 * b
| a * b = 0

Tactic:
rw [← zero_mul b]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
conv_lhs : a * b = 0 * b ↔ a = 0
⊢ a * b = 0 ↔ a = 0

Tactic:
conv_lhs => rw [← zero_mul b]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
rw rw₁ : 0 * b = 0 * b
⊢ a * b = 0 * b

Tactic:
rw [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : IsCancelMulZero R
a : R
a0 : a ≠ 0
⊢ IsRegular a

Tactic:
⟨fun _ _ => mul_left_cancel₀ a0, fun _ _ => mul_right_cancel₀ a0⟩

Premises used: mul_left_cancel₀, IsRegular.mk, mul_right_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Regular
Goal:
R : Type u_1
inst : MulZeroClass R
inst_1 : IsCancelMulZero R
a : R
inst_2 : Nontrivial R
⊢ IsRegular a ↔ a ≠ 0

Tactic:
⟨IsRegular.ne_zero, .of_ne_zero⟩

Premises used: IsRegular.of_ne_zero, IsRegular.ne_zero, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, SemiconjBy, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, SemiconjBy, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Tactic:
simp only [ha, inv_zero, SemiconjBy.zero_left]

Premises used: inv_zero, SemiconjBy.zero_left
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a⁻¹ y x

Tactic:
SemiconjBy.inv_symm_left_iff₀.2 h

Premises used: Iff.mpr, SemiconjBy.inv_symm_left_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
pos : ∀ (ha : a = 0), SemiconjBy a x⁻¹ y⁻¹
neg : ∀ (ha : ¬a = 0), SemiconjBy a x⁻¹ y⁻¹
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
simp only [ha, zero_left]

Premises used: SemiconjBy.zero_left
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
pos : ∀ (hx : x = 0), SemiconjBy a x⁻¹ y⁻¹
neg : ∀ (hx : ¬x = 0), SemiconjBy a x⁻¹ y⁻¹
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
pos : ∀ (h : SemiconjBy a 0 y), SemiconjBy a 0⁻¹ y⁻¹
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
subst x
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ y = 0 ∨ a = 0

Tactic:
simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h

Premises used: SemiconjBy, eq_comm, mul_eq_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹

Tactic:
simp [h.resolve_right ha]

Premises used: Or.resolve_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ a * x ≠ 0

Tactic:
have := mul_ne_zero ha hx
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ y ≠ 0 ∧ a ≠ 0

Tactic:
rw [h.eq, mul_ne_zero_iff] at this

Premises used: SemiconjBy.eq, mul_ne_zero_iff
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
@units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

Premises used: SemiconjBy.units_inv_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

Premises used: SemiconjBy.units_inv_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
⟨fun h => inv_inv x ▸ inv_inv y ▸ h.inv_right₀, inv_right₀⟩

Premises used: SemiconjBy.inv_right₀, Eq.rec, inv_inv, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
rw : SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
⊢ SemiconjBy a (x / x') (y / y')

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)

Tactic:
h.mul_right h'.inv_right₀

Premises used: SemiconjBy.inv_right₀, SemiconjBy.mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)

Tactic:
exact h.mul_right h'.inv_right₀

Premises used: SemiconjBy.inv_right₀, SemiconjBy.mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (HPow.hPow (β := ℤ) x (↑n : ℤ)) (HPow.hPow (β := ℤ) y (↑n : ℤ))

Tactic:
simp [h.pow_right n]

Premises used: SemiconjBy.pow_right
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

Premises used: SemiconjBy.inv_right₀, zpow_negSucc, SemiconjBy.pow_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a b : G₀
h : Commute a b
⊢ ∀ (m : ℤ), Commute a (b ^ m)

Tactic:
SemiconjBy.zpow_right₀ h

Premises used: Commute, SemiconjBy.zpow_right₀
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a b : G₀
h : Commute a b
m : ℤ
⊢ Commute (a ^ m) b

Tactic:
(h.symm.zpow_right₀ m).symm

Premises used: Commute.zpow_right₀, Commute.symm
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a b : G₀
h : Commute a b
m n : ℤ
⊢ Commute (a ^ m) (b ^ n)

Tactic:
(h.zpow_left₀ m).zpow_right₀ n

Premises used: Commute.zpow_right₀, Commute.zpow_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
n : ℤ
⊢ Commute (a ^ n) a

Tactic:
(Commute.refl a).zpow_left₀ n

Premises used: Commute.zpow_left₀, Commute.refl
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
n : ℤ
⊢ Commute a (a ^ n)

Tactic:
(Commute.refl a).zpow_right₀ n

Premises used: Commute.zpow_right₀, Commute.refl
-- Module: Mathlib.Algebra.GroupWithZero.Semiconj
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
a : G₀
m n : ℤ
⊢ Commute (a ^ m) (a ^ n)

Tactic:
(Commute.refl a).zpow_zpow₀ m n

Premises used: Commute.refl, Commute.zpow_zpow₀
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
G : Type u_2
inst : GroupWithZero G₀
inst_1 : Group G
inst_2 : MulDistribMulAction G₀ G
a : G₀
ha : a ≠ 0
S : Subgroup G
x : G
⊢ a • x ∈ a • S ↔ x ∈ S

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

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

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set G) 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
G : Type u_2
inst : GroupWithZero G₀
inst_1 : Group G
inst_2 : MulDistribMulAction G₀ G
a : G₀
ha : a ≠ 0
S : Subgroup G
x : G
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

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

Premises used: Set.mem_inv_smul_set_iff₀, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Subgroup
Goal:
G₀ : Type u_1
G : Type u_2
inst : GroupWithZero G₀
inst_1 : Group G
inst_2 : MulDistribMulAction G₀ G
S T : Subgroup G
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
G : Type u_2
inst : GroupWithZero G₀
inst_1 : Group G
inst_2 : MulDistribMulAction G₀ G
S T : Subgroup G
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
G : Type u_2
inst : GroupWithZero G₀
inst_1 : Group G
inst_2 : MulDistribMulAction G₀ G
S T : Subgroup G
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.Subgroup
Goal:
M : Type u_3
A : Type u_4
inst : Monoid M
inst_1 : AddGroup A
inst_2 : DistribMulAction M A
a : M
S : AddSubgroup A
⊢ a • S =
    map
      (((DistribMulAction.toAddMonoidEnd M A : MonoidHom.{u_3, u_4} M (AddMonoid.End A)) : (a : M) → AddMonoid.End A) a)
      S

Tactic:
rfl

Premises used: rfl
-- 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
a : M
S : AddSubgroup A
⊢ (↑(a • S) : Set A) = a • (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- 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
a : M
S : AddSubgroup A
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, AddSubmonoid.map, rfl
-- 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 ∈ S → a • m ∈ a • S

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

Premises used: Set.Mem, Set.smul_mem_smul_set