awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s_1 t_1 : Set α
n : ℤ
s t : Set α
⊢ s / t = s * t⁻¹
have rw : id '' (s / t) = s * (fun (x : α) ↦ x⁻¹) '' t
Tactic: rw [← image_id (s / t), ← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s_1 t_1 : Set α
n : ℤ
s t : Set α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹
have simp_rw : (fun (x : α) ↦ x⁻¹) '' (s * t) = HMul.hMul (α := Set α) ((fun (x : α) ↦ x⁻¹) '' t) ((fun (x : α) ↦ x⁻¹) '' s)
Tactic: simp_rw [← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s_1 t_1 : Set α
n : ℤ
s t : Set α
h : s * t = 1
⊢ s⁻¹ = t
have obtain : ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := Set α) {a} {b} = 1), Eq (α := Set α) {a}⁻¹ {b}
Tactic: obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : HMul.hMul (α := Set α) {a} {b} = 1
⊢ Eq (α := Set α) {a}⁻¹ {b}
have rw : Eq (α := Set α) {a⁻¹} {b}
Tactic: rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : HMul.hMul (α := Set α) {a} {b} = 1
rw : Eq (α := Set α) {a⁻¹} {b}
⊢ Eq (α := Set α) {a}⁻¹ {b}
have rw₁ : Eq (α := Set α) {b} {b}
Tactic: rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
⊢ IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a
have mp : IsUnit s → ∃ (a : α), s = {a} ∧ IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
mp : IsUnit s → ∃ (a : α), s = {a} ∧ IsUnit a
⊢ IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a
have mpr : (∃ (a : α), s = {a} ∧ IsUnit a) → IsUnit s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
⊢ ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a
have mp : ∀ (a b : α) (ha : (↑u : Set α) = {a}) (hb : (↑u⁻¹ : Set α) = {b}) (h : a * b = 1),
  ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a
Tactic: obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
⊢ ∃ (a : α), (↑u : Set α) = {a} ∧ IsUnit a
have mp : Eq (α := Set α) {b * a} {1}
Tactic: refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : (↑u : Set α) = {a}
hb : (↑u⁻¹ : Set α) = {b}
h : a * b = 1
⊢ Eq (α := Set α) {b * a} {1}
have mp : (↑u⁻¹ : Set α) * (↑u : Set α) = {1}
Tactic: rw [← singleton_mul_singleton, ← ha, ← hb]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s / t
have rw : s ⊆ s * t⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t
have rw : t⁻¹ ⊆ s * t⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Set α) ∅ n = ∅
have ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Set α) ∅ (Int.ofNat a) = ∅
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
n : ℤ
hn : n ≠ 0
ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Set α) ∅ (Int.ofNat a) = ∅
⊢ HPow.hPow (α := Set α) ∅ n = ∅
have negSucc : ∀ (a : ℕ) (hn : Int.negSucc a ≠ 0), HPow.hPow (α := Set α) ∅ (Int.negSucc a) = ∅
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
have mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
have mpr : s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0
have mp : s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
n : ℤ
⊢ HPow.hPow (α := Set α) {a} n = {a ^ n}
have ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Set α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
n : ℤ
ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Set α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}
⊢ HPow.hPow (α := Set α) {a} n = {a ^ n}
have negSucc : ∀ (a_1 : ℕ), HPow.hPow (α := Set α) {a} (Int.negSucc a_1) = {a ^ Int.negSucc a_1}
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
t : Set α
a : α
⊢ Eq (α := Set α) ((fun (x : α) ↦ a * x) '' t) ((fun (x : α) ↦ a⁻¹ * x) ⁻¹' t)
have h₁ : LeftInverse (fun (x : α) ↦ a⁻¹ * x) fun (x : α) ↦ a * x
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
t : Set α
a : α
h₁ : LeftInverse (fun (x : α) ↦ a⁻¹ * x) fun (x : α) ↦ a * x
⊢ Eq (α := Set α) ((fun (x : α) ↦ a * x) '' t) ((fun (x : α) ↦ a⁻¹ * x) ⁻¹' t)
have h₂ : RightInverse (fun (x : α) ↦ a⁻¹ * x) fun (x : α) ↦ a * x
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
t : Set α
b : α
⊢ Eq (α := Set α) ((fun (x : α) ↦ x * b) '' t) ((fun (x : α) ↦ x * b⁻¹) ⁻¹' t)
have h₁ : LeftInverse (fun (x : α) ↦ x * b⁻¹) fun (x : α) ↦ x * b
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
t : Set α
b : α
h₁ : LeftInverse (fun (x : α) ↦ x * b⁻¹) fun (x : α) ↦ x * b
⊢ Eq (α := Set α) ((fun (x : α) ↦ x * b) '' t) ((fun (x : α) ↦ x * b⁻¹) ⁻¹' t)
have h₂ : RightInverse (fun (x : α) ↦ x * b⁻¹) fun (x : α) ↦ x * b
Tactic: rw [image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) {b}) {a⁻¹ * b}
have rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' {b}) {a⁻¹ * b}
Tactic: rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' {b}) {a⁻¹ * b}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) {b}) {a⁻¹ * b}
have rw₁ : Eq (α := Set α) {a⁻¹ * b} {a⁻¹ * b}
Tactic: rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * a) {b}) {b * a⁻¹}
have rw : Eq (α := Set α) ((fun (x : α) ↦ x * a⁻¹) '' {b}) {b * a⁻¹}
Tactic: rw [← image_mul_right', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x * a⁻¹) '' {b}) {b * a⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * a) {b}) {b * a⁻¹}
have rw₁ : Eq (α := Set α) {b * a⁻¹} {b * a⁻¹}
Tactic: rw [← image_mul_right', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) 1) {a⁻¹}
have rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' 1) {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' 1) {a⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) 1) {a⁻¹}
have rw₁ : Eq (α := Set α) {a⁻¹ * 1} {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Set α) ((fun (x : α) ↦ a⁻¹ * x) '' 1) {a⁻¹}
rw₁ : Eq (α := Set α) {a⁻¹ * 1} {a⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ a * x) 1) {a⁻¹}
have rw₂ : Eq (α := Set α) {a⁻¹} {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * b) 1) {b⁻¹}
have rw : Eq (α := Set α) ((fun (x : α) ↦ x * b⁻¹) '' 1) {b⁻¹}
Tactic: rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x * b⁻¹) '' 1) {b⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * b) 1) {b⁻¹}
have rw₁ : Eq (α := Set α) {1 * b⁻¹} {b⁻¹}
Tactic: rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x * b⁻¹) '' 1) {b⁻¹}
rw₁ : Eq (α := Set α) {1 * b⁻¹} {b⁻¹}
⊢ Eq (α := Set α) (preimage (β := α) (fun (x : α) ↦ x * b) 1) {b⁻¹}
have rw₂ : Eq (α := Set α) {b⁻¹} {b⁻¹}
Tactic: rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
s : Set α
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s⁻¹) ((⇑f : (a : α) → β) '' s)⁻¹
have rw : Eq.{u_3 + 1} (α := Set β) (image (α := α) (⇑f : (a : α) → β) ((fun (x : α) ↦ x⁻¹) '' s))
  ((fun (x : β) ↦ x⁻¹) '' (⇑f : (a : α) → β) '' s)
Tactic: rw [← image_inv_eq_inv, ← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)) ((fun (x1 x2 : β) ↦ x1 * x2) a b)
have obtain : ∀ (a : α) (ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)),
  Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) b)
Tactic: obtain ⟨a, rfl⟩ := hs ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
b : β
hb : b ∈ t
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) b)
have obtain : ∀ (b : α) (hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)),
  Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 * x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))
Tactic: obtain ⟨b, rfl⟩ := ht hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)))
    ((⇑m : (a : α) → β) '' HMul.hMul (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
  HMul.hMul (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
    (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
Tactic: rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    HMul.hMul (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)))
    ((⇑m : (a : α) → β) '' HMul.hMul (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₁ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
  s * image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
Tactic: rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    HMul.hMul (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    s * image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)))
    ((⇑m : (a : α) → β) '' HMul.hMul (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) = s * t
Tactic: rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    HMul.hMul (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) =
    s * image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)) = s * t
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s * t)))
    ((⇑m : (a : α) → β) '' HMul.hMul (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₃ : s * t = s * t
Tactic: rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)) ((fun (x1 x2 : β) ↦ x1 / x2) a b)
have obtain : ∀ (a : α) (ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)),
  Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) b)
Tactic: obtain ⟨a, rfl⟩ := hs ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
b : β
hb : b ∈ t
a : α
ha : Membership.mem (α := β) s ((m : (a : α) → β) a : β)
⊢ Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) b)
have obtain : ∀ (b : α) (hb : Membership.mem (α := β) t ((m : (a : α) → β) b : β)),
  Membership.mem (γ := Set β) (range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β))
    ((fun (x1 x2 : β) ↦ x1 / x2) ((m : (a : α) → β) a) ((m : (a : α) → β) b))
Tactic: obtain ⟨b, rfl⟩ := ht hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)))
    ((⇑m : (a : α) → β) '' HDiv.hDiv (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
  HDiv.hDiv (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
    (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
Tactic: rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    HDiv.hDiv (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)))
    ((⇑m : (a : α) → β) '' HDiv.hDiv (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₁ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
  s / image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
Tactic: rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    HDiv.hDiv (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    s / image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)))
    ((⇑m : (a : α) → β) '' HDiv.hDiv (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) = s / t
Tactic: rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
hm : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑m : (a : α) → β)
s t : Set β
hs : s ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑m : (a : α) → β)
rw :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    HDiv.hDiv (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' s))
      (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t))
rw₁ :
  image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) =
    s / image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' t)
rw₂ : image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)) = s / t
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑m : (a : α) → β) ((⇑m : (a : α) → β) ⁻¹' (s / t)))
    ((⇑m : (a : α) → β) '' HDiv.hDiv (α := Set α) ((⇑m : (a : α) → β) ⁻¹' s) ((⇑m : (a : α) → β) ⁻¹' t))
have rw₃ : s / t = s / t
Tactic: rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]