awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
w : G₀ˣ
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]

Premises used: WithZero.withZeroUnitsEquiv, commute_iff_eq, MonoidWithZeroHom.inl, MonoidWithZeroHom.inr, WithZero.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
w : G₀ˣ
w_1 : H₀ˣ
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w_1 : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]

Premises used: WithZero.withZeroUnitsEquiv, commute_iff_eq, MonoidWithZeroHom.inl, MonoidWithZeroHom.inr, WithZero.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
inst_2 : Nontrivial H
f : G →*₀ H
⊢ Ne.{u_2 + 1} (α := ↥(MonoidHom.mrange f)) 1 0

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.GroupWithZero.Range
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
inst_2 : Nontrivial H
f : G →*₀ H
⊢ Set.Nontrivial.{u_2} (α := H) (range.{u_2, u_1 + 1} (ι := G) (⇑f : (a : G) → H))

Tactic:
Set.nontrivial_coe_sort.mp f.mrange_nontrivial

Premises used: MonoidWithZeroHom.mrange_nontrivial, Iff.mp, Set.nontrivial_coe_sort
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
hb : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) a
hb' : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) b
obtain :
  ∀ (y : A) (hy : (f : (a : A) → B) y = (↑a : B)),
    Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)

Tactic:
obtain ⟨y, hy⟩ := hb
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
hb' : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) b
y : A
hy : (f : (a : A) → B) y = (↑a : B)
obtain :
  ∀ (y' : A) (hy' : (f : (a : A) → B) y' = (↑b : B)),
    Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)

Tactic:
obtain ⟨y', hy'⟩ := hb'
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
h : (f : (a : A) → B) (y * y') = (↑(a * b) : B)
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)

Tactic:
use y * y'
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
h : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
h₁ : HMul.hMul (β := B) (↑a : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
h₂ : (↑a : B) * (↑b : B) = (↑(a * b) : B)
h₃ h₄ : (↑a : B) * (↑b : B) = (↑a : B) * (↑b : B)
⊢ (f : (a : A) → B) (y * y') = (↑(a * b) : B)

Tactic:
rw [map_mul, hy, hy', Units.val_mul]

Premises used: 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) ((↑1 : 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) 1

Tactic:
⟨1, map_one ..⟩

Premises used: Set.Mem, setOf, Set.preimage, map_one, Exists.intro, Set.range, OfNat.ofNat
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq (α := ↥(valueMonoid f)) (Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) x) 1 ⋯)
    1

Tactic:
rfl

Premises used: 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
⊢ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b ↔
    Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.range
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq (α := Submonoid Bˣ) (valueMonoid f)
    (Submonoid.closure (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)))

Tactic:
(valueMonoid f).closure_eq.symm

Premises used: Set.Mem, setOf, Submonoid.closure_eq, Set.preimage, Set.range, Eq.symm, MonoidWithZeroHom.valueMonoid
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ valueGroup f = Subgroup.closure (↑(valueMonoid f) : Set Bˣ)

Tactic:
rfl

Premises used: MonoidWithZeroHom.valueGroup, 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
hb : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑b : B)
⊢ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b

Tactic:
tauto
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
hb : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑b : B)
suffices : Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) b

Tactic:
suffices b ∈ valueMonoid f from Subgroup.mem_closure.mpr fun _ a ↦ a this
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
hb : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑b : B)
⊢ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b

Tactic:
mem_valueMonoid _ hb

Premises used: MonoidWithZeroHom.mem_valueMonoid
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
hb : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑b : B)
⊢ Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b

Tactic:
exact mem_valueMonoid _ hb

Premises used: MonoidWithZeroHom.mem_valueMonoid
-- 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 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
b : Bˣ
hb : Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (↑b : B)
⊢ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) b⁻¹

Tactic:
Subgroup.inv_mem _ (mem_valueGroup f hb)

Premises used: MonoidWithZeroHom.mem_valueGroup, Set.Mem, Subgroup.inv_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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
    (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B) then 0
    else
      (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
            (Units.mk0 ((f : (a : A) → B) 0) h) ⋯) :
        WithZero ↥(valueGroup f)))
    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 : MonoidWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
    (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) (0 : B) then 0
    else
      (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
            (Units.mk0 ((f : (a : A) → B) 1) h) ⋯) :
        WithZero ↥(valueGroup f)))
    1

Tactic:
simp [← WithZero.coe_one]

Premises used: WithZero.coe_one
-- 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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ ∀ (x y : A),
    (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (x * y) : B) (0 : B) then 0
      else
        (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
              (Units.mk0 ((f : (a : A) → B) (x * y)) h) ⋯) :
          WithZero ↥(valueGroup f))) =
      HMul.hMul (α := ValueGroup₀ f)
        (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) (0 : B) then 0
        else
          (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
                (Units.mk0 ((f : (a : A) → B) x) h) ⋯) :
            WithZero ↥(valueGroup f)))
        (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) y : B) (0 : B) then 0
        else
          (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
                (Units.mk0 ((f : (a : A) → B) y) h) ⋯) :
            WithZero ↥(valueGroup f)))

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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
h : Ne.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
    (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a : ValueGroup₀ f)
    ((↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
            (Units.mk0 ((f : (a : A) → B) a) h) ⋯) :
        WithZero ↥(valueGroup f)) :
      WithZero ↥(valueGroup f))

Tactic:
simp [h, restrict₀_apply]

Premises used: 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 : MonoidWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
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) ↔
    Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)

Tactic:
simp [restrict₀_apply]

Premises used: 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 : MonoidWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
pos :
  ∀ (H : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)),
    Eq.{u_2 + 1} (α := ValueGroup₀ f) 0 1 ↔ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)
neg :
  ∀ (H : ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)),
    Eq.{u_2 + 1} (α := ValueGroup₀ f)
        ((↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
                (Units.mk0 ((f : (a : A) → B) a) H) ⋯) :
            WithZero ↥(valueGroup f)) :
          WithZero ↥(valueGroup f))
        (1 : ValueGroup₀ f) ↔
      Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
      (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) then 0
      else
        (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
              (Units.mk0 ((f : (a : A) → B) a) h) ⋯) :
          WithZero ↥(valueGroup f)))
      1 ↔
    Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)

Tactic:
split_ifs with 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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
H : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f) 0 1 ↔ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)

Tactic:
simp [H, ← WithZero.coe_one, ← Units.mk0_one]

Premises used: one_ne_zero, WithZero.coe_one, Units.mk0_one
-- 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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
H : ¬Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ f)
      ((↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
              (Units.mk0 ((f : (a : A) → B) a) H) ⋯) :
          WithZero ↥(valueGroup f)) :
        WithZero ↥(valueGroup f))
      (1 : ValueGroup₀ f) ↔
    Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)

Tactic:
simp [H, ← WithZero.coe_one, ← Units.mk0_one]

Premises used: one_ne_zero, WithZero.coe_one, Units.mk0_one
-- 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 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
simp :
  Eq.{u_2 + 1} (α := B)
    (WithZero.recZeroCoe (motive := fun (x : WithZero Bˣ) ↦ B) 0 Units.val
        ((WithZero.map' (Subgroup.subtype (valueGroup f)) : (a : ValueGroup₀ f) → WithZero Bˣ)
          (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) then 0
          else
            (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
                  (Units.mk0 ((f : (a : A) → B) a) h) ⋯) :
              WithZero ↥(valueGroup f)))) :
      B)
    ((f : (a : A) → B) a : B)
⊢ Eq (α := B)
    ((embedding : (a : ValueGroup₀ f) → B)
        (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) a : ValueGroup₀ f) :
      B)
    ((f : (a : A) → B) a : B)

Tactic:
simp only [restrict₀_apply, embedding_apply]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_apply, 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 : MonoidWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : A
⊢ Eq.{u_2 + 1} (α := B)
    (WithZero.recZeroCoe (motive := fun (x : WithZero Bˣ) ↦ B) 0 Units.val
        ((WithZero.map' (Subgroup.subtype (valueGroup f)) : (a : ValueGroup₀ f) → WithZero Bˣ)
          (if h : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B) then 0
          else
            (↑(Subtype.mk (p := fun (x : Bˣ) ↦ Membership.mem (γ := Subgroup Bˣ) (valueGroup f) x)
                  (Units.mk0 ((f : (a : A) → B) a) h) ⋯) :
              WithZero ↥(valueGroup f)))) :
      B)
    ((f : (a : A) → B) a : 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
rw : Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹) = valueMonoid f
⊢ Eq (α := Submonoid Bˣ) (valueMonoid f) (toSubmonoid (valueGroup f))

Tactic:
rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm]

Premises used: Subgroup.closure_toSubmonoid, MonoidWithZeroHom.valueGroup_def, Eq.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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
h₁ : (↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)
h₂ : valueMonoid f ≤ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹)
⊢ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹) = valueMonoid f

Tactic:
apply Submonoid.closure_eq_of_le

Premises used: Submonoid.closure_eq_of_le
-- 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
h₁ : (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)
⊢ (↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)

Tactic:
simp only [union_subset_iff, subset_refl, true_and]

Premises used: Set.union_subset_iff, subset_refl, true_and
-- 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
a : Bˣ
h₁ : ∀ (y : A) (hy : (f : (a : A) → B) y = (↑a⁻¹ : B)), a ∈ (↑(valueMonoid f) : Set Bˣ)
⊢ a ∈ (↑(valueMonoid f) : Set Bˣ)⁻¹ → a ∈ (↑(valueMonoid f) : Set Bˣ)

Tactic:
⟨y, 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a⁻¹ : B)
h : (f : (a : A) → B) y⁻¹ = (↑a : B)
⊢ a ∈ (↑(valueMonoid f) : Set Bˣ)

Tactic:
use y⁻¹
-- 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
a : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a⁻¹ : B)
⊢ (f : (a : A) → B) y⁻¹ = (↑a : B)

Tactic:
simp [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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
⊢ valueMonoid f ≤ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹)

Tactic:
simp [Submonoid.closure_union]

Premises used: Submonoid.closure_union
-- 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 : (↑(toSubmonoid (valueGroup f)) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
rw₁ rw₂ : (↑(valueGroup f) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
⊢ (↑(valueMonoid f) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)

Tactic:
rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]

Premises used: MonoidWithZeroHom.valueMonoid_eq_valueGroup, Subgroup.coe_toSubmonoid
-- 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
h :
  ∀ (x : B),
    x ∈ Units.val '' (↑(valueGroup f) : Set Bˣ) ↔
      Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B) \ {0}) x
⊢ Units.val '' (↑(valueGroup f) : Set Bˣ) = range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B) \ {0}

Tactic:
ext 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : B
h :
  (∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x) ↔
    (∃ (y : A), (f : (a : A) → B) y = x) ∧ ¬x = 0
⊢ x ∈ Units.val '' (↑(valueGroup f) : Set Bˣ) ↔
    Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B) \ {0}) x

Tactic:
simp only [mem_diff, mem_range, mem_singleton_iff, ← valueMonoid_eq_valueGroup' f, mem_image,
    SetLike.mem_coe, mem_valueMonoid_iff, mem_preimage, mem_range]

Premises used: Set.mem_range, Set.mem_image, Set.mem_singleton_iff, SetLike.mem_coe, Set.mem_diff, MonoidWithZeroHom.valueMonoid_eq_valueGroup', MonoidWithZeroHom.mem_valueMonoid_iff, Set.mem_preimage
-- 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 : B
h :
  (∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x) →
    (∃ (y : A), (f : (a : A) → B) y = x) ∧ ¬x = 0
h₁ :
  (∃ (y : A), (f : (a : A) → B) y = x) ∧ ¬x = 0 →
    ∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x
⊢ (∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x) ↔
    (∃ (y : A), (f : (a : A) → B) y = x) ∧ ¬x = 0

Tactic:
constructor
-- 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
y : Bˣ
hy : ∃ (y_1 : A), (f : (a : A) → B) y_1 = (↑y : B)
⊢ (∃ (y_1 : A), (f : (a : A) → B) y_1 = (↑y : B)) ∧ ¬(↑y : B) = 0

Tactic:
simp only [Units.ne_zero, not_false_eq_true, and_true, hy]

Premises used: and_true, Units.ne_zero, 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : B
hx₀ : ¬x = 0
y : A
hy : (f : (a : A) → B) y = x
⊢ ∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x

Tactic:
⟨Units.mk0 x hx₀, ?_, rfl⟩

Premises used: Units.mk0, And.intro, Exists.intro, 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : B
hx₀ : ¬x = 0
y : A
hy : (f : (a : A) → B) y = x
h : ∃ (y : A), (f : (a : A) → B) y = (↑(Units.mk0 x hx₀) : B)
⊢ ∃ (x_1 : Bˣ), (∃ (y : A), (f : (a : A) → B) y = (↑x_1 : B)) ∧ (↑x_1 : B) = x

Tactic:
refine ⟨Units.mk0 x hx₀, ?_, 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 : GroupWithZero A
inst_2 : GroupWithZero B
inst_3 : MonoidWithZeroHomClass F A B
x : B
hx₀ : ¬x = 0
y : A
hy : (f : (a : A) → B) y = x
⊢ ∃ (y : A), (f : (a : A) → B) y = (↑(Units.mk0 x hx₀) : B)

Tactic:
simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩

Premises used: Set.mem_range, Units.val_mk0