awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
zero : (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
⊢ (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
have succ : ∀ (n : ℕ) (ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n), (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
Tactic: induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
have mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
have a : (s ∩ t) ^ n ⊆ s ^ n
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
a : (s ∩ t) ^ n ⊆ s ^ n
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
have a₁ : (s ∩ t) ^ n ⊆ t ^ n
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n
have a : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
have a : s ∩ t ⊆ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin n) → ↥(s i)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have rw : (∃ (f : (i : Fin n) → (↑((SetLike.coe ∘ s) i) : Type u_2)),
    List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a) ↔
  ∃ (f : (i : Fin n) → ↥(s i)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
Tactic: rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)
have rw : #(s ^ n * s) ≤ #s ^ n * #s
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) * #s ≤ #s ^ n * #s
have bc : #(s ^ n) ≤ #s ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
inst_2 : Fintype α
hn : n ≠ 0
⊢ (↑(HPow.hPow (α := Finset α) univ n) : Set α) = (↑univ : Set α)
have rw : (↑univ : Set α) ^ n = (↑univ : Set α)
Tactic: rw [coe_pow, coe_univ, Set.univ_pow hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
inst_2 : Fintype α
hn : n ≠ 0
rw : (↑univ : Set α) ^ n = (↑univ : Set α)
⊢ (↑(HPow.hPow (α := Finset α) univ n) : Set α) = (↑univ : Set α)
have rw₁ : HPow.hPow (α := Set α) Set.univ n = Set.univ
Tactic: rw [coe_pow, coe_univ, Set.univ_pow hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
inst_2 : Fintype α
hn : n ≠ 0
rw : (↑univ : Set α) ^ n = (↑univ : Set α)
rw₁ : HPow.hPow (α := Set α) Set.univ n = Set.univ
⊢ (↑(HPow.hPow (α := Finset α) univ n) : Set α) = (↑univ : Set α)
have rw₂ : Eq.{u_2 + 1} (α := Set α) Set.univ Set.univ
Tactic: rw [coe_pow, coe_univ, Set.univ_pow hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)
have rw : image op (s ^ n * s) = image op s ^ (n + 1)
Tactic: rw [pow_succ, pow_succ', image_op_mul, image_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : image op (s ^ n * s) = image op s ^ (n + 1)
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)
have rw₁ : image op (s ^ n * s) = image op s * image op s ^ n
Tactic: rw [pow_succ, pow_succ', image_op_mul, image_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : image op (s ^ n * s) = image op s ^ (n + 1)
rw₁ : image op (s ^ n * s) = image op s * image op s ^ n
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)
have rw₂ : image op s * image op (s ^ n) = image op s * image op s ^ n
Tactic: rw [pow_succ, pow_succ', image_op_mul, image_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : image op (s ^ n * s) = image op s ^ (n + 1)
rw₁ : image op (s ^ n * s) = image op s * image op s ^ n
rw₂ : image op s * image op (s ^ n) = image op s * image op s ^ n
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)
have rw₃ : image op s * image op s ^ n = image op s * image op s ^ n
Tactic: rw [pow_succ, pow_succ', image_op_mul, image_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ map (Equiv.toEmbedding opEquiv) (s ^ (n + 1)) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
have rw : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
Tactic: rw [pow_succ, pow_succ', map_op_mul, map_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
⊢ map (Equiv.toEmbedding opEquiv) (s ^ (n + 1)) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
have rw₁ : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
Tactic: rw [pow_succ, pow_succ', map_op_mul, map_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
rw₁ :
  map (Equiv.toEmbedding opEquiv) (s ^ n * s) =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
⊢ map (Equiv.toEmbedding opEquiv) (s ^ (n + 1)) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
have rw₂ : map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) (s ^ n) =
  map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
Tactic: rw [pow_succ, pow_succ', map_op_mul, map_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
rw₁ :
  map (Equiv.toEmbedding opEquiv) (s ^ n * s) =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
rw₂ :
  map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) (s ^ n) =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
⊢ map (Equiv.toEmbedding opEquiv) (s ^ (n + 1)) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
have rw₃ : map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n =
  map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
Tactic: rw [pow_succ, pow_succ', map_op_mul, map_op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(s ^ Int.negSucc n) : Set α) = (↑s : Set α) ^ Int.negSucc n
have refine : (↑(npowRec n.succ s) : Set α)⁻¹ = (↑s : Set α) ^ Int.negSucc n
Tactic: refine (coe_inv _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have simp_rw : (↑(s * t) : Set α) = (↑1 : Set α) ↔
  ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
Tactic: simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
simp_rw :
  (↑(s * t) : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have simp_rw₁ : (↑s : Set α) * (↑t : Set α) = (↑1 : Set α) ↔
  ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
Tactic: simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
simp_rw :
  (↑(s * t) : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₁ :
  (↑s : Set α) * (↑t : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have simp_rw₂ : (↑s : Set α) * (↑t : Set α) = 1 ↔
  ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
Tactic: simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
simp_rw :
  (↑(s * t) : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₁ :
  (↑s : Set α) * (↑t : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₂ :
  (↑s : Set α) * (↑t : Set α) = 1 ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
have simp_rw₃ : (∃ (a : α) (b : α), (↑s : Set α) = {a} ∧ (↑t : Set α) = {b} ∧ a * b = 1) ↔
  ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
Tactic: simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
⊢ 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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
⊢ ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a
have mp : ∀ (a b : α) (ha : (↑u : Finset α) = {a}) (hb : (↑u⁻¹ : Finset α) = {b}) (h : a * b = 1),
  ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a
Tactic: obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
⊢ ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a
have mp : Eq (α := Finset α) {b * a} {1}
Tactic: refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
⊢ Eq (α := Finset α) {b * a} {1}
have mp : (↑u⁻¹ : Finset α) * (↑u : Finset α) = {1}
Tactic: rw [← singleton_mul_singleton, ← ha, ← hb]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
⊢ IsUnit (↑s : Set α) ↔ IsUnit s
have simp_rw : IsUnit (↑s : Set α) ↔ ∃ (a : α), s = {a} ∧ IsUnit a
Tactic: simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
simp_rw : IsUnit (↑s : Set α) ↔ ∃ (a : α), s = {a} ∧ IsUnit a
⊢ IsUnit (↑s : Set α) ↔ IsUnit s
have simp_rw₁ : (∃ (a : α), (↑s : Set α) = {a} ∧ IsUnit a) ↔ ∃ (a : α), s = {a} ∧ IsUnit a
Tactic: simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Finset α) ∅ n = ∅
have ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Finset α) ∅ (Int.ofNat a) = ∅
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
n : ℤ
hn : n ≠ 0
ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Finset α) ∅ (Int.ofNat a) = ∅
⊢ HPow.hPow (α := Finset α) ∅ n = ∅
have negSucc : ∀ (a : ℕ) (hn : Int.negSucc a ≠ 0), HPow.hPow (α := Finset α) ∅ (Int.negSucc a) = ∅
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
have mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
n : ℤ
⊢ HPow.hPow (α := Finset α) {a} n = {a ^ n}
have ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Finset α) {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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
n : ℤ
ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Finset α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}
⊢ HPow.hPow (α := Finset α) {a} n = {a ^ n}
have negSucc : ∀ (a_1 : ℕ), HPow.hPow (α := Finset α) {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.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
have rw : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint s t
Tactic: rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
rw : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint s t
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
have rw₁ : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
Tactic: rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
rw : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint s t
rw₁ : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
have rw₂ : 1 ∈ (↑s : Set α) / (↑t : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
Tactic: rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
rw : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint s t
rw₁ : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
rw₂ : 1 ∈ (↑s : Set α) / (↑t : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
have rw₃ : ¬Disjoint (↑s : Set α) (↑t : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
Tactic: rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}
have rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
Tactic: rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}
have rw₁ : Eq (α := Finset α) {a⁻¹ * b} {a⁻¹ * b}
Tactic: rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}
have classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
Tactic: classical rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}
have classical₁ : Eq (α := Finset α) {a⁻¹ * b} {a⁻¹ * b}
Tactic: classical rw [← image_mul_left', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}
have rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
Tactic: rw [← image_mul_right', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}
have rw₁ : Eq (α := Finset α) {b * a⁻¹} {b * a⁻¹}
Tactic: rw [← image_mul_right', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}
have classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
Tactic: classical rw [← image_mul_right', image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a b : α
classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}
have classical₁ : Eq (α := Finset α) {b * a⁻¹} {b * a⁻¹}
Tactic: classical rw [← image_mul_right', image_singleton]
-- 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 α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}
have rw₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
rw₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}
have rw₂ : Eq (α := Finset α) {a⁻¹} {a⁻¹}
Tactic: rw [← image_mul_left', image_one, mul_one]
-- 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 classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
Tactic: classical rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}
have classical₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
Tactic: classical rw [← image_mul_left', image_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
classical₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}
have classical₂ : Eq (α := Finset α) {a⁻¹} {a⁻¹}
Tactic: classical rw [← image_mul_left', image_one, mul_one]
-- 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 α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
Tactic: 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 : α
rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}
have rw₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
Tactic: 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 : α
rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
rw₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}
have rw₂ : Eq (α := Finset α) {b⁻¹} {b⁻¹}
Tactic: rw [← image_mul_right', image_one, one_mul]