awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}
have classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
Tactic: classical rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}
have classical₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
Tactic: classical rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
classical₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}
have classical₂ : Eq (α := Finset α) {b⁻¹} {b⁻¹}
Tactic: classical rw [← image_mul_right', image_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
⊢ preimage 1 (fun (x : α) ↦ a⁻¹ * x) ⋯ = {a}
have rw : Eq (α := Finset α) {a⁻¹⁻¹} {a}
Tactic: rw [preimage_mul_left_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Finset α) {a⁻¹⁻¹} {a}
⊢ preimage 1 (fun (x : α) ↦ a⁻¹ * x) ⋯ = {a}
have rw₁ : Eq (α := Finset α) {a} {a}
Tactic: rw [preimage_mul_left_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
⊢ preimage 1 (fun (x : α) ↦ x * b⁻¹) ⋯ = {b}
have rw : Eq (α := Finset α) {b⁻¹⁻¹} {b}
Tactic: rw [preimage_mul_right_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Finset α) {b⁻¹⁻¹} {b}
⊢ preimage 1 (fun (x : α) ↦ x * b⁻¹) ⋯ = {b}
have rw₁ : Eq (α := Finset α) {b} {b}
Tactic: rw [preimage_mul_right_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)
have inl : s = ∅ → #s ≤ #(s * s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s * s)
⊢ #s ≤ #(s * s)
have inr : s.Nonempty → #s ≤ #(s * s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)
have inl : s = ∅ → #s ≤ #(s * s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s * s)
⊢ #s ≤ #(s * s)
have inr : s.Nonempty → #s ≤ #(s * s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ (n + 1))
have rw : #(s ^ n) ≤ #(s ^ n * s)
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(s ^ m) ≤ #(s ^ n)
have inl : #(HPow.hPow (α := Finset α) ∅ m) ≤ #(HPow.hPow (α := Finset α) ∅ n)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
inl : #(HPow.hPow (α := Finset α) ∅ m) ≤ #(HPow.hPow (α := Finset α) ∅ n)
⊢ #(s ^ m) ≤ #(s ^ n)
have inr : ∀ (hs : s.Nonempty), #(s ^ m) ≤ #(s ^ n)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s : Finset α
⊢ #s ≤ #(s / s)
have inl : s = ∅ → #s ≤ #(s / s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s / s)
⊢ #s ≤ #(s / s)
have inr : s.Nonempty → #s ≤ #(s / s)
Tactic: cases s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Scalar (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq β
inst_1 : DecidableEq γ
inst_2 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_3 : SMul β γ
inst_4 : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
have h₁ : ∀ (a_1 : γ), a_1 ∈ (op a • s) • t ↔ a_1 ∈ s • a • t
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
⊢ SProd.sprod (α := Set α) (β := Set β) 1 1 = 1
have h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) (β := Set β) 1 1 ↔ Membership.mem (γ := Set (α × β)) 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅
have rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' s) ∅ ↔ s = ∅
Tactic: rw [← image_inv_eq_inv, image_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' s) ∅ ↔ s = ∅
⊢ s⁻¹ = ∅ ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [← image_inv_eq_inv, image_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
have rw : s⁻¹⁻¹ ⊆ t⁻¹ ↔ s ⊆ t⁻¹
Tactic: rw [← inv_subset_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s t : Set α
rw : s⁻¹⁻¹ ⊆ t⁻¹ ↔ s ⊆ t⁻¹
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
have rw₁ : s ⊆ t⁻¹ ↔ s ⊆ t⁻¹
Tactic: rw [← inv_subset_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
⊢ Eq (α := Set α) {a}⁻¹ {a⁻¹}
have rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' {a}) {a⁻¹}
Tactic: rw [← image_inv_eq_inv, image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' {a}) {a⁻¹}
⊢ Eq (α := Set α) {a}⁻¹ {a⁻¹}
have rw₁ : Eq (α := Set α) {a⁻¹} {a⁻¹}
Tactic: rw [← image_inv_eq_inv, image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
have rw : ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
Tactic: rw [insert_eq, union_inv, inv_singleton, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
s : Set α
rw : ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
have rw₁ : {a}⁻¹ ∪ s⁻¹ = insert a⁻¹ s⁻¹
Tactic: rw [insert_eq, union_inv, inv_singleton, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
s : Set α
rw : ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
rw₁ : {a}⁻¹ ∪ s⁻¹ = insert a⁻¹ s⁻¹
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
have rw₂ : {a⁻¹} ∪ s⁻¹ = insert a⁻¹ s⁻¹
Tactic: rw [insert_eq, union_inv, inv_singleton, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
a : α
s : Set α
rw : ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
rw₁ : {a}⁻¹ ∪ s⁻¹ = insert a⁻¹ s⁻¹
rw₂ : {a⁻¹} ∪ s⁻¹ = insert a⁻¹ s⁻¹
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
have rw₃ : {a⁻¹} ∪ s⁻¹ = {a⁻¹} ∪ s⁻¹
Tactic: rw [insert_eq, union_inv, inv_singleton, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun (i : ι) ↦ (f i)⁻¹
have rw : Eq (α := Set α) ((fun (x : α) ↦ x⁻¹) '' range f) (range fun (i : ι) ↦ (f i)⁻¹)
Tactic: rw [← image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s
have rw : (fun (x : α) ↦ f x⁻¹) '' s = g '' s
Tactic: rw [← Set.image_inv_eq_inv, Set.image_image]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
inst_1 : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| (g '' s)⁻¹
have rw : f '' s⁻¹
Tactic: rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
inst_1 : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹
have conv_rhs : f '' s⁻¹ = (g '' s)⁻¹
Tactic: conv_rhs => rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : InvolutiveInv α
s : Set α
inst_1 : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
conv_rhs : f '' s⁻¹ = (g '' s)⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹
have conv_rhs₁ : f '' s⁻¹ = f '' s⁻¹
Tactic: conv_rhs => rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ (x : α), x ∈ s → p x⁻¹
have rw : (∀ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) → p ((Equiv.inv α : (a : α) → α) a)) ↔
  ∀ (x : α), x ∈ s → p x⁻¹
Tactic: rw [← (Equiv.inv _).forall_congr_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ (x : α), x⁻¹ ∈ s ∧ p x) ↔ ∃ (x : α), x ∈ s ∧ p x⁻¹
have rw : (∃ (a : α), Membership.mem (α := α) s (((Equiv.inv α : (a : α) → α) a)⁻¹ : α) ∧ p ((Equiv.inv α : (a : α) → α) a)) ↔
  ∃ (x : α), x ∈ s ∧ p x⁻¹
Tactic: rw [← (Equiv.inv _).exists_congr_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹
have simp_rw : Eq (α := Set αᵐᵒᵖ) (op '' (fun (x : α) ↦ x⁻¹) '' s) ((fun (x : αᵐᵒᵖ) ↦ x⁻¹) '' op '' s)
Tactic: simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)
have h : ∀ (x : α × β), x ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α × β
⊢ x ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)
have h : (∃ (a : α), ∃ (b : β), (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ (a_1 : α), ∃ (b_1 : β), (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x) ↔
  (∃ (x_1 : α), x_1 ∈ s₁ ∧ ∃ (y : α), y ∈ s₂ ∧ x_1 * y = x.1) ∧
    ∃ (x_1 : β), x_1 ∈ t₁ ∧ ∃ (y : β), y ∈ t₂ ∧ x_1 * y = x.2
Tactic: simp [mem_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty
have rw : (s ^ n * s).Nonempty
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
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 : Monoid α
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 : Monoid α
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 : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
have rs : (s ∩ t) ^ n ⊆ s ^ n
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
rs : (s ∩ t) ^ n ⊆ s ^ n
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
have rt : (s ∩ t) ^ n ⊆ t ^ n
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n
have rs : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
have rt : s ∩ t ⊆ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
⊢ HPow.hPow (α := Set α) univ (n + 2) = univ
have rw : HPow.hPow (α := Set α) univ (n + 1) * univ = univ
Tactic: rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Set α) univ (n + 1) * univ = univ
⊢ HPow.hPow (α := Set α) univ (n + 2) = univ
have rw₁ : HMul.hMul (α := Set α) univ univ = univ
Tactic: rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Set α) univ (n + 1) * univ = univ
rw₁ : HMul.hMul (α := Set α) univ univ = univ
⊢ HPow.hPow (α := Set α) univ (n + 2) = univ
have rw₂ : Eq.{u_2 + 1} (α := Set α) univ univ
Tactic: rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
⊢ s * t = 1 ↔ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_1 : ∀ (h : s * t = 1), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
refine_1 : ∀ (h : s * t = 1), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_2 : (∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (hypothesis)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have hst : (s * t).Nonempty
Tactic: have hst : (s * t).Nonempty := h.symm.subst one_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_1 : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
Tactic: obtain ⟨a, ha⟩ := hst.of_image2_left
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_1 : ∀ (b : α) (hb : b ∈ t), ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
Tactic: obtain ⟨b, hb⟩ := hst.of_image2_right
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (hypothesis)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
Tactic: have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_1 : s = {a}
Tactic: refine ⟨a, b, ?_, ?_, H ha hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
refine_1 : s = {a}
⊢ ∃ (a : α), ∃ (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have refine_1₁ : t = {b}
Tactic: refine ⟨a, b, ?_, ?_, H ha hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}
have refine_1 : ∀ (x : α) (hx : x ∈ s), x = a
Tactic: refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}
have refine_1 : ∀ (x : α) (hx : x ∈ t), x = b
Tactic: refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
b c : α
h : b * c = 1
⊢ HMul.hMul (α := Set α) {b} {c} = 1
have refine_2 : Eq (α := Set α) {b * c} 1
Tactic: rw [singleton_mul_singleton, h, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := Set α) {b * c} 1
⊢ HMul.hMul (α := Set α) {b} {c} = 1
have refine_2₁ : Eq (α := Set α) {1} 1
Tactic: rw [singleton_mul_singleton, h, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := Set α) {b * c} 1
refine_2₁ : Eq (α := Set α) {1} 1
⊢ HMul.hMul (α := Set α) {b} {c} = 1
have refine_2₂ : Eq.{u_2 + 1} (α := Set α) 1 1
Tactic: rw [singleton_mul_singleton, h, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun (x : α) ↦ a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
have rw : (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
Tactic: rw [← nonempty_inv, inter_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw : Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ a⁻¹ * x) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ x * a) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ a⁻¹ * x) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x * a) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw₁ : Set.Nonempty (α := α) ((fun (x : α) ↦ (a⁻¹ * x)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹ * a) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ a⁻¹ * x) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x * a) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₁ :
  Set.Nonempty (α := α) ((fun (x : α) ↦ (a⁻¹ * x)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹ * a) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw₂ : Set.Nonempty (α := α) ((fun (a_1 : α) ↦ a_1⁻¹ * a⁻¹⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹ * a) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun (x : α) ↦ x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
have rw : (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
Tactic: rw [← nonempty_inv, inter_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw : Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ x * a⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ x * a⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw₁ : Set.Nonempty (α := α) ((fun (x : α) ↦ (x * a⁻¹)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ a * x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
s t : Set α
a : α
simp_rw :
  Set.Nonempty (α := α) ((fun (x : α) ↦ x⁻¹) '' (fun (x : α) ↦ x * a⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
simp_rw₁ :
  Set.Nonempty (α := α) ((fun (x : α) ↦ (x * a⁻¹)⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
    Set.Nonempty (α := α) ((fun (x : α) ↦ a * x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
⊢ (((fun (x : α) ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun (x : α) ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
have simp_rw₂ : Set.Nonempty (α := α) ((fun (a_1 : α) ↦ a⁻¹⁻¹ * a_1⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t) ↔
  Set.Nonempty (α := α) ((fun (x : α) ↦ a * x⁻¹) '' s ∩ (fun (x : α) ↦ x⁻¹) '' t)
Tactic: simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]