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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
rw : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := ValueGroup₀ f) (⇑(restrict₀ f) : (a : A) → ValueGroup₀ f)
⊢ Eq.{u_2 + 1} (α := Set (ValueGroup₀ f)) (range.{u_2, u_1 + 1} (ι := A) (⇑(restrict₀ f) : (a : A) → ValueGroup₀ f)) ⊤

Tactic:
rw [top_eq_univ, range_eq_univ]

Premises used: Set.range_eq_univ, Set.top_eq_univ
-- 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
h :
  Eq.{u_2 + 1} (α := ValueGroup₀ f)
    (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) 0
⊢ ∃ (a : A),
    Eq.{u_2 + 1} (α := ValueGroup₀ f)
      (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a : ValueGroup₀ f)
      (0 : ValueGroup₀ f)

Tactic:
use 0
-- 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
    (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) 0

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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
u : Bˣ
hu : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) u
⊢ u ∈ (↑(valueGroup f) : Set Bˣ)

Tactic:
change u ∈ (valueGroup f : Set Bˣ) at hu

Premises used: SetLike.coe, MonoidWithZeroHom.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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
u : Bˣ
hu : u ∈ (↑(valueGroup f) : Set Bˣ)
⊢ u ∈ (↑(valueMonoid f) : Set Bˣ)

Tactic:
rw [← valueMonoid_eq_valueGroup'] at hu

Premises used: MonoidWithZeroHom.valueMonoid_eq_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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
u : Bˣ
hu_1 : u ∈ (↑(valueGroup f) : Set Bˣ)
hu : u ∈ (↑(valueMonoid f) : Set Bˣ)
obtain :
  ∀ (v : A) (hv : (f : (a : A) → B) v = (↑u : B)),
    ∃ (a : A),
      ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a =
        some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) u hu_1)
⊢ ∃ (a : A),
    ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a =
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) u hu_1)

Tactic:
obtain ⟨v, hv⟩ := hu
-- 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
u : Bˣ
hu : u ∈ (↑(valueGroup f) : Set Bˣ)
v : A
hv : (f : (a : A) → B) v = (↑u : B)
h :
  ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) v =
    some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) u hu)
⊢ ∃ (a : A),
    ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a =
      some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) u hu)

Tactic:
use v
-- 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
u : Bˣ
hu : u ∈ (↑(valueGroup f) : Set Bˣ)
v : A
hv : (f : (a : A) → B) v = (↑u : B)
⊢ ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) v =
    some (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x) u hu)

Tactic:
simp [restrict₀_apply, hv, Units.ne_zero, WithZero.coe]

Premises used: Units.ne_zero, WithZero.coe, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
⊢ ∃ (a : A), ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a = x

Tactic:
match x with
  | 0 => use 0; simp
  | some ⟨u, hu⟩ =>
    change u ∈ (valueGroup f : Set Bˣ) at hu
    rw [← valueMonoid_eq_valueGroup'] at hu
    obtain ⟨v, hv⟩ := hu
    use v
    simp [restrict₀_apply, hv, Units.ne_zero, WithZero.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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : ValueGroup₀ f
⊢ Membership.mem (γ := Set (ValueGroup₀ f)) (range.{u_2, u_1 + 1} (ι := A) (⇑(restrict₀ f) : (a : A) → ValueGroup₀ f)) x

Tactic:
simp [ValueGroup₀.restrict₀_range_eq_top]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top
-- 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ˣ
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y ↔
    ∃ (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

Tactic:
⟨fun hy ↦ ?_, fun ⟨a, ha, x, hy⟩ ↦ ?_⟩

Premises used: Membership.mem, _private.0.MonoidWithZeroHom.mem_valueGroup_iff_of_comm.match_1, Iff.intro, MonoidWithZeroHom.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ˣ
refine_1 :
  ∀ (hy : Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y),
    ∃ (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
refine_2 :
  (∃ (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),
      Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) y ↔
    ∃ (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

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨a, ha, x, 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 x : Bˣ
h : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) x
refine_1 :
  ∀ (a : A) (ha : (f : (a : A) → B) a = (↑x : B)),
    ∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x_1 : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1
⊢ ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x_1 : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1

Tactic:
obtain ⟨a, ha⟩ := h
-- 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 x : Bˣ
a : A
ha : (f : (a : A) → B) a = (↑x : B)
⊢ HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) (a * a)

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

Tactic:
exact ⟨a, ha.symm ▸ Units.ne_zero _, ⟨a * a, by simp [← 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ˣ
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) (0 : 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
y : Bˣ
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) 1 : B) ((↑1 : B) : B) = (f : (a : A) → B) 1

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

Tactic:
exact ⟨1, by simp, 1, by 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
y c d : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hd :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    d
hcy :
  ∃ (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) (↑c : B) = (f : (a : A) → B) x
hdy :
  ∃ (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) (↑d : B) = (f : (a : A) → B) x
refine_1 :
  ∀ (u : A) (hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)) (a : A)
    (ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a),
    ∃ (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) (↑(c * d) : B) = (f : (a : A) → B) x
⊢ ∃ (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) (↑(c * d) : B) = (f : (a : A) → B) x

Tactic:
obtain ⟨u, hu, a, ha⟩ := hcy
-- 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 c d : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hd :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    d
hdy :
  ∃ (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) (↑d : B) = (f : (a : A) → B) x
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
refine_1 :
  ∀ (v : A) (hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) v : B) (0 : B)) (b : A)
    (hb : HMul.hMul (α := B) ((f : (a : A) → B) v : B) (↑d : B) = (f : (a : A) → B) 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) (↑(c * d) : B) = (f : (a : A) → B) x
⊢ ∃ (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) (↑(c * d) : B) = (f : (a : A) → B) x

Tactic:
obtain ⟨v, hv, b, hb⟩ := hdy
-- 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 c d : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hd :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    d
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
v : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) v : B) (0 : B)
b : A
hb : HMul.hMul (α := B) ((f : (a : A) → B) v : B) (↑d : B) = (f : (a : A) → B) b
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) (u * v) : B) (0 : B)

Tactic:
simp [hu, hv]
-- 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 c d : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hd :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    d
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
v : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) v : B) (0 : B)
b : A
hb : HMul.hMul (α := B) ((f : (a : A) → B) v : B) (↑d : B) = (f : (a : A) → B) b
refine_1 : HMul.hMul (α := B) ((f : (a : A) → B) (u * v) : B) (↑(c * d) : B) = (f : (a : A) → B) (a * 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) (↑(c * d) : B) = (f : (a : A) → B) x

Tactic:
refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩
-- 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 c d : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hd :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    d
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
v : A
hv : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) v : B) (0 : B)
b : A
hb : HMul.hMul (α := B) ((f : (a : A) → B) v : B) (↑d : B) = (f : (a : A) → B) b
⊢ HMul.hMul (α := B) ((f : (a : A) → B) (u * v) : B) (↑(c * d) : B) = (f : (a : A) → B) (a * b)

Tactic:
simpa [map_mul, Units.val_mul, ← hb, ← ha] using mul_mul_mul_comm ..

Premises used: mul_mul_mul_comm, map_mul, Units.val_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 c : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
hcy :
  ∃ (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) (↑c : B) = (f : (a : A) → B) x
refine_1 :
  ∀ (u : A) (hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)) (a : A)
    (ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a),
    ∃ (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) (↑c⁻¹ : B) = (f : (a : A) → B) x
⊢ ∃ (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) (↑c⁻¹ : B) = (f : (a : A) → B) x

Tactic:
obtain ⟨u, hu, a, ha⟩ := hcy
-- 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 c : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)

Tactic:
simp [← ha, hu]
-- 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 c : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
⊢ HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑c⁻¹ : B) = (f : (a : A) → B) u

Tactic:
simp [← 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 c : Bˣ
hc :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    c
u : A
hu : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) u : B) (0 : B)
a : A
ha : HMul.hMul (α := B) ((f : (a : A) → B) u : B) (↑c : B) = (f : (a : A) → B) a
⊢ ∃ (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) (↑c⁻¹ : B) = (f : (a : A) → B) x

Tactic:
exact ⟨a, by simp [← ha, hu], u, by simp [← 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ˣ
hy :
  Membership.mem (γ := Subgroup Bˣ) (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))
    y
refine_1 :
  ∀ (x : Bˣ) (h : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) x),
    ∃ (a : A),
      Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
        ∃ (x_1 : A), HMul.hMul (α := B) ((f : (a : A) → B) a : B) (↑x : B) = (f : (a : A) → B) x_1
refine_1₁ :
  ∃ (a : A),
    Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) ∧
      ∃ (x : A), HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((↑1 : B) : B) = (f : (a : A) → B) x
refine_1₂ :
  ∀ (c d : Bˣ)
    (hc :
      Membership.mem (γ := Subgroup Bˣ)
        (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B))) c)
    (hd :
      Membership.mem (γ := Subgroup Bˣ)
        (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B))) d)
    (hcy :
      ∃ (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) (↑c : B) = (f : (a : A) → B) x)
    (hdy :
      ∃ (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) (↑d : B) = (f : (a : A) → B) x),
    ∃ (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) (↑(c * d) : B) = (f : (a : A) → B) x
refine_1₃ :
  ∀ (c : Bˣ)
    (hc :
      Membership.mem (γ := Subgroup Bˣ)
        (Subgroup.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B))) c)
    (hcy :
      ∃ (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) (↑c : B) = (f : (a : A) → B) x),
    ∃ (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) (↑c⁻¹ : B) = (f : (a : A) → B) x
⊢ ∃ (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

Tactic:
induction hy using Subgroup.closure_induction with
    | mem _ h =>
      obtain ⟨a, ha⟩ := h
      exact ⟨a, ha.symm ▸ Units.ne_zero _, ⟨a * a, by simp [← ha]⟩⟩
    | one => exact ⟨1, by simp, 1, by simp⟩
    | mul c d hc hd hcy hdy =>
      obtain ⟨u, hu, a, ha⟩ := hcy
      obtain ⟨v, hv, b, hb⟩ := hdy
      refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩
      simpa [map_mul, Units.val_mul, ← hb, ← ha] using mul_mul_mul_comm ..
    | inv c hc hcy =>
      obtain ⟨u, hu, a, ha⟩ := hcy
      exact ⟨a, by simp [← ha, hu], u, by simp [← ha]⟩

Premises used: mul_mul_mul_comm, map_mul, Subgroup.inv, Units.val_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
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)

Tactic:
simp only [← hy, ne_eq, mul_eq_zero, ha, Units.ne_zero, or_self, not_false_eq_true]

Premises used: Units.ne_zero, mul_eq_zero, ne_eq, or_self, not_false_eq_true
-- 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
⊢ Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B)

Tactic:
have hv : f x ≠ 0 := by
      simp only [← hy, ne_eq, mul_eq_zero, ha, Units.ne_zero, or_self, not_false_eq_true]
-- 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
⊢ (f : (a : A) → B) x = (↑v : B)

Tactic:
have hv₀ : f x = ↑v := IsUnit.unit_spec (Ne.isUnit hv)