awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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)
⊢ (f : (a : A) → B) (y * y') = (↑(a * b) : B)
have h₃ : (↑a : B) * (↑b : B) = (↑a : B) * (↑b : B)
Tactic: rw [map_mul, hy, hy', Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
have suffices : Membership.mem (γ := Submonoid Bˣ) (valueMonoid f) b
Tactic: suffices b ∈ valueMonoid f from Subgroup.mem_closure.mpr fun _ a ↦ a this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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)
      (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)
have 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)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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)
⊢ 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)
have 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) sorry) :
          WithZero ↥(valueGroup f)) :
        WithZero ↥(valueGroup f))
      (1 : ValueGroup₀ f) ↔
    Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) (1 : B)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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 (α := 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)
have 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) sorry) :
            WithZero ↥(valueGroup f)))) :
    B)
  ((f : (a : A) → B) a : B)
Tactic: simp only [restrict₀_apply, embedding_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ Eq (α := Submonoid Bˣ) (valueMonoid f) (toSubmonoid (valueGroup f))
have rw : Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹) = valueMonoid f
Tactic: rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹) = valueMonoid f
have h₁ : (↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)
Tactic: apply Submonoid.closure_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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ˣ)
⊢ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹) = valueMonoid f
have h₂ : valueMonoid f ≤ Submonoid.closure ((↑(valueMonoid f) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹)
Tactic: apply Submonoid.closure_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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) : Set Bˣ) ∪ (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)
have h₁ : (↑(valueMonoid f) : Set Bˣ)⁻¹ ⊆ (↑(valueMonoid f) : Set Bˣ)
Tactic: simp only [union_subset_iff, subset_refl, true_and]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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ˣ
⊢ a ∈ (↑(valueMonoid f) : Set Bˣ)⁻¹ → a ∈ (↑(valueMonoid f) : Set Bˣ)
have h₁ : ∀ (y : A) (hy : (f : (a : A) → B) y = (↑a⁻¹ : B)), a ∈ (↑(valueMonoid f) : Set Bˣ)
Tactic: ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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)
⊢ a ∈ (↑(valueMonoid f) : Set Bˣ)
have h : (f : (a : A) → B) y⁻¹ = (↑a : B)
Tactic: use y⁻¹
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
have rw : (↑(toSubmonoid (valueGroup f)) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
Tactic: rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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ˣ)
⊢ (↑(valueMonoid f) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
have rw₁ : (↑(valueGroup f) : Set Bˣ) = (↑(valueGroup f) : Set Bˣ)
Tactic: rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ Units.val '' (↑(valueGroup f) : Set Bˣ) = range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B) \ {0}
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ x ∈ Units.val '' (↑(valueGroup f) : Set Bˣ) ↔
    Membership.mem (γ := Set B) (range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B) \ {0}) x
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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_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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
have h : ∃ (y : A), (f : (a : A) → B) y = (↑(Units.mk0 x hx₀) : B)
Tactic: refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ Eq.{u_2 + 1} (α := Set (ValueGroup₀ f)) (range.{u_2, u_1 + 1} (ι := A) (⇑(restrict₀ f) : (a : A) → ValueGroup₀ f)) ⊤
have rw : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := ValueGroup₀ f) (⇑(restrict₀ f) : (a : A) → ValueGroup₀ f)
Tactic: rw [top_eq_univ, range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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),
    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)
have h : Eq.{u_2 + 1} (α := ValueGroup₀ f)
  (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (hypothesis)
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
⊢ ∃ (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)
have hu₁ : u ∈ (↑(valueGroup f) : Set Bˣ)
Tactic: change u ∈ (valueGroup f : Set Bˣ) at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (hypothesis)
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ˣ)
⊢ ∃ (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)
have hu₁ : u ∈ (↑(valueMonoid f) : Set Bˣ)
Tactic: rw [← valueMonoid_eq_valueGroup'] at hu
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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ˣ)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨v, hv⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use v
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
have 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
Tactic: refine ⟨fun hy ↦ ?_, fun ⟨a, ha, x, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun hy ↦ ?_, fun ⟨a, ha, x, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨u, hu, a, ha⟩ := hcy
Cleared hypotheses: hcy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨v, hv, b, hb⟩ := hdy
Cleared hypotheses: hdy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have refine_1 : HMul.hMul (α := B) ((f : (a : A) → B) (u * v) : B) (↑(c * d) : B) = (f : (a : A) → B) (a * b)
Tactic: refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨u, hu, a, ha⟩ := hcy
Cleared hypotheses: hcy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
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
⊢ ∃ (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
have 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
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]⟩
Cleared hypotheses: hy