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
y : Bˣ
h :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hy : HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
⊢ (f : (a : A) → B) a = (↑u : B)

Tactic:
have ha₀ : f a = ↑u := IsUnit.unit_spec (Ne.isUnit ha)
-- 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
y : Bˣ
h :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hy : HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
⊢ (f : (a : A) → B) x = (↑v : B)

Tactic:
rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy

Premises used: Eq.comm, inv_mul_eq_iff_eq_mul
-- 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
y : Bˣ
h :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hy : HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hv₁ : (f : (a : A) → B) x = (↑v : B)
⊢ let u := ⋯.unit;
  (f : (a : A) → B) a = (↑u : B)

Tactic:
rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy

Premises used: Eq.comm, inv_mul_eq_iff_eq_mul
-- 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
y : Bˣ
h :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hy : HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hv₁ : (f : (a : A) → B) x = (↑v : B)
ha₁ :
  let u := ⋯.unit;
  (f : (a : A) → B) a = (↑u : B)
⊢ let u := ⋯.unit;
  u⁻¹ * v = y

Tactic:
rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy

Premises used: Eq.comm, inv_mul_eq_iff_eq_mul
-- 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
y : Bˣ
h :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
refine_2 : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) (u⁻¹ * v)
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y

Tactic:
rw [← hy]
-- 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
y : Bˣ
h :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
refine_2 : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) u⁻¹
refine_2₁ : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) v
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) (u⁻¹ * v)

Tactic:
apply Subgroup.mul_mem

Premises used: Subgroup.mul_mem
-- 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
y : Bˣ
h :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
refine_2 : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑u : B)
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) u⁻¹

Tactic:
apply inv_mem_valueGroup

Premises used: MonoidWithZeroHom.inv_mem_valueGroup
-- 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
y : Bˣ
h_1 :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
w : A
h : (f : (a : A) → B) a = (↑u : B)
⊢ Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑u : B)

Tactic:
use a
-- 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
y : Bˣ
h :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
refine_2 : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑v : B)
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) v

Tactic:
apply mem_valueGroup

Premises used: MonoidWithZeroHom.mem_valueGroup
-- 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
y : Bˣ
h_1 :
  ∃ (a : A),
    ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)
v : Bˣ := ⋯.unit
hv₀ : (f : (a : A) → B) x = (↑v : B)
u : Bˣ := ⋯.unit
ha₀ : (f : (a : A) → B) a = (↑u : B)
hy : u⁻¹ * v = y
w : A
h : (f : (a : A) → B) x = (↑v : B)
⊢ Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑v : B)

Tactic:
use x
-- 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
y : Bˣ
rw :
  (∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x) ↔
    ∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x : A),
          Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B) ∧
            HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y ↔
    ∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x : A),
          Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B) ∧
            HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x

Tactic:
rw [mem_valueGroup_iff_of_comm]

Premises used: MonoidWithZeroHom.mem_valueGroup_iff_of_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
y : Bˣ
h :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
a : A
ha : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A
hax : HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)

Tactic:
aesop
-- 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
y : Bˣ
⊢ (∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x) ↔
    ∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x : A),
          Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B) ∧
            HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑y : B) = (f : (a : A) → B) x

Tactic:
exact ⟨fun ⟨a, ha, x, hax⟩ ↦ ⟨a, ha, x, by aesop, hax⟩, fun ⟨a, ha, x, hx, hax⟩ ↦ ⟨a, ha, x, hax⟩⟩
-- 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
r₁ s₁ r₂ s₂ r 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)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B))
    ((↑(Units.mk0 ((f : (a : A) → B) r) hr) : B) : B)

Tactic:
simp
-- 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
r₁ s₁ r₂ s₂ r 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)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B))
    ((↑(Units.mk0 ((f : (a : A) → B) s) hs) : B) : B)

Tactic:
simp
-- 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
r₁ s₁ r₂ 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)
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)
simp :
  HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ) =
      HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) ↔
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₁ : B) ((f : (a : A) → B) s₂ : B) =
      HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₂ : B) ((f : (a : A) → B) s₁ : B)
⊢ Eq (α := ↥(valueGroup f)) (mk f r₁ s₁ hr₁ hs₁) (mk f r₂ s₂ hr₂ hs₂) ↔
    Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (r₁ * s₂) : B) ((f : (a : A) → B) (r₂ * s₁) : B)

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

Premises used: map_mul, 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
r₁ s₁ r₂ 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)
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)
rw :
  HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) r₁) hr₁ : Bˣ) =
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) r₂) hr₂ : Bˣ) ↔
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₁ : B) ((f : (a : A) → B) s₂ : B) =
      HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₂ : B) ((f : (a : A) → B) s₁ : B)
⊢ HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ) =
      HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) ↔
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₁ : B) ((f : (a : A) → B) s₂ : B) =
      HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₂ : B) ((f : (a : A) → B) s₁ : B)

Tactic:
rw [inv_mul_eq_inv_mul_iff_mul_eq_mul, eq_comm]

Premises used: eq_comm, inv_mul_eq_inv_mul_iff_mul_eq_mul
-- 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
r₁ s₁ r₂ 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)
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)
⊢ HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) r₁) hr₁ : Bˣ) =
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) r₂) hr₂ : Bˣ) ↔
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₁ : B) ((f : (a : A) → B) s₂ : B) =
      HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r₂ : B) ((f : (a : A) → B) s₁ : B)

Tactic:
simp [Units.ext_iff, mul_comm (f r₂), mul_comm (f s₂)]

Premises used: Units.ext_iff, mul_comm, DFunLike.coe
-- 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
r₁ s₁ r₂ 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)
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)
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) (r₁ * r₂) : B) (0 : B)

Tactic:
simp_all
-- 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
r₁ s₁ r₂ 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)
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)
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) (s₁ * s₂) : B) (0 : B)

Tactic:
simp_all
-- 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
r₁ s₁ r₂ 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)
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)
simp :
  HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ) *
      HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) =
    (HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) r₁) ⋯ : Bˣ)
          (Units.mk0 ((f : (a : A) → B) r₂) ⋯ : Bˣ))⁻¹ *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) ⋯ : Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) ⋯ : Bˣ)
⊢ HMul.hMul (α := ↥(valueGroup f)) (mk f r₁ s₁ hr₁ hs₁) (mk f r₂ s₂ hr₂ hs₂) = mk f (r₁ * r₂) (s₁ * s₂) ⋯ ⋯

Tactic:
simp only [mk, map_mul, MulMemClass.mk_mul_mk, Units.mk0_mul, Subtype.mk.injEq]

Premises used: Units.mk0_mul, map_mul, MonoidWithZeroHom.valueGroup.mk, Subtype.mk.injEq, MulMemClass.mk_mul_mk
-- 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
r₁ s₁ r₂ 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)
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)
rw :
  HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ) *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) =
    (HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) r₁) ⋯ : Bˣ)
          (Units.mk0 ((f : (a : A) → B) r₂) ⋯ : Bˣ))⁻¹ *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) ⋯ : Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) ⋯ : Bˣ)
rw₁ rw₂ :
  HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ) *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) =
    HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) ⋯)⁻¹ : Bˣ)
        ((Units.mk0 ((f : (a : A) → B) r₂) ⋯)⁻¹ : Bˣ) *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) ⋯ : Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) ⋯ : Bˣ)
⊢ HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₁) hr₁)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₁) hs₁ : Bˣ) *
      HMul.hMul (α := Bˣ) (β := Bˣ) ((Units.mk0 ((f : (a : A) → B) r₂) hr₂)⁻¹ : Bˣ)
        (Units.mk0 ((f : (a : A) → B) s₂) hs₂ : Bˣ) =
    (HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) r₁) ⋯ : Bˣ)
          (Units.mk0 ((f : (a : A) → B) r₂) ⋯ : Bˣ))⁻¹ *
      HMul.hMul (α := Bˣ) (β := Bˣ) (Units.mk0 ((f : (a : A) → B) s₁) ⋯ : Bˣ) (Units.mk0 ((f : (a : A) → B) s₂) ⋯ : Bˣ)

Tactic:
rw [mul_mul_mul_comm, mul_inv]

Premises used: mul_mul_mul_comm, mul_inv
-- 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
inst_4 : DecidablePred fun (b : B) ↦ b = 0
r 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)
⊢ Eq (α := ValueGroup₀ f) (mk f r s) (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))

Tactic:
simp [ValueGroup₀.mk, hr, hs]

Premises used: MonoidWithZeroHom.ValueGroup₀.mk
-- 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
none :
  Eq.{u_2 + 1} (α := ValueGroup₀ f) Option.none 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)),
      Eq (α := ValueGroup₀ f) Option.none (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))
some :
  ∀ (x : Bˣ) (hx : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x),
    Option.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)),
        Option.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))
⊢ x = 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)),
      x = (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))

Tactic:
obtain _ | ⟨x, hx⟩ := x
-- 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
none : Eq.{u_2 + 1} (α := ValueGroup₀ f) Option.none 0
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f) Option.none 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)),
      Eq (α := ValueGroup₀ f) Option.none (↑(valueGroup.mk f r s hr hs) : WithZero ↥(valueGroup f))

Tactic:
left
-- 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
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f) none 0

Tactic:
rfl
-- 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
⊢ ∃ (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

Tactic:
rw [mem_valueGroup_iff_of_comm'] at hx

Premises used: MonoidWithZeroHom.mem_valueGroup_iff_of_comm'