awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Finset ι
f : ι → Set α
a : α
empty :
  ∀ (a : α),
    Membership.mem (γ := Set α) (∏ i ∈ ∅, f i) a ↔
      ∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) ∅ i → g i ∈ f i), ∏ i ∈ ∅, g i = a
insert insert₁ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    Membership.mem (γ := Set α) (∏ i ∈ Insert.insert i is, f i) a ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), ∏ i ∈ Insert.insert i is, g i = a
insert₂ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), ∏ i ∈ Insert.insert i is, g i = a
insert₃ :
  ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
    (ih :
      ∀ (a : α),
        Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
          ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
    (a : α),
    (∃ x ∈ f i, ∃ (y : α), Membership.mem (γ := Set α) (∏ x ∈ is, f x) y ∧ x * y = a) ↔
      ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
⊢ Membership.mem (γ := Set α) (∏ i ∈ t, f i) a ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
have insert₄ : ∀ (i : ι) (is : Finset ι) (hi : i ∉ is)
  (ih :
    ∀ (a : α),
      Membership.mem (γ := Set α) (∏ i ∈ is, f i) a ↔
        ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a)
  (a : α),
  (∃ x ∈ f i, ∃ (y : α), (∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) ↔
    ∃ (g : ι → α) (_ : ∀ {i_1 : ι}, i_1 ∈ Insert.insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Tactic: classical
    induction t using Finset.induction_on generalizing a with
    | empty =>
      simp_rw [Finset.prod_empty, Set.mem_one]
      exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩
    | insert i is hi ih => ?_
    rw [Finset.prod_insert hi, Set.mem_mul]
    simp_rw [Finset.prod_insert hi]
    simp_rw [ih]
    constructor
    · rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
      refine ⟨Function.update g i x, ?_, ?_⟩
      · intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj
      · rw [Finset.prod_update_of_notMem hi, Function.update_self]
    · rintro ⟨g, hg, rfl⟩
      exact ⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
Cleared hypotheses: t, a
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Fintype ι
f : ι → Set α
a : α
⊢ Membership.mem (γ := Set α) (∏ i : ι, f i) a ↔ ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
have rw : (∃ (g : ι → α) (_ : ∀ {i : ι}, Membership.mem (γ := Finset ι) Finset.univ i → g i ∈ f i), ∏ i : ι, g i = a) ↔
  ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
Tactic: rw [mem_finsetProd]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i
⊢ (List.map g []).prod ∈ (List.map f []).prod
have nil : Membership.mem (γ := Set α) (List.prod []) (List.prod [])
Tactic: simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i
nil : Membership.mem (γ := Set α) (List.prod []) (List.prod [])
⊢ (List.map g []).prod ∈ (List.map f []).prod
have nil₁ : Membership.mem (γ := Set α) 1 1
Tactic: simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod
have cons : g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod
Tactic: simp_rw [List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (List.map g t).prod ∈ (List.map f t).prod
have nil : ∀ (hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i), (List.map g []).prod ∈ (List.map f []).prod
Tactic: induction t with
  | nil => simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)
Cleared hypotheses: t, hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
nil : ∀ (hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i), (List.map g []).prod ∈ (List.map f []).prod
⊢ (List.map g t).prod ∈ (List.map f t).prod
have cons : ∀ (h : ι) (tl : List ι) (ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod)
  (hg : ∀ i ∈ h :: tl, g i ∈ f i), (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod
Tactic: induction t with
  | nil => simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)
Cleared hypotheses: t, hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod
have nil : ∀ (hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f₁ i ⊆ f₂ i), (List.map f₁ []).prod ⊆ (List.map f₁ []).prod
Tactic: induction t with
  | nil => rfl
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)
Cleared hypotheses: t, hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
nil : ∀ (hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f₁ i ⊆ f₂ i), (List.map f₁ []).prod ⊆ (List.map f₁ []).prod
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod
have cons : ∀ (h : ι) (tl : List ι) (ih : ∀ (hf : ∀ i ∈ tl, f₁ i ⊆ f₂ i), (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod)
  (hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i), (List.map f₁ (h :: tl)).prod ⊆ (List.map f₂ (h :: tl)).prod
Tactic: induction t with
  | nil => rfl
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)
Cleared hypotheses: t, hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (Multiset.map g t).prod ∈ (Multiset.map f t).prod
have h : ∀ (a : List ι) (hg : ∀ i ∈ ⟦a⟧, g i ∈ f i), (Multiset.map g ⟦a⟧).prod ∈ (Multiset.map f ⟦a⟧).prod
Tactic: induction t using Quotient.inductionOn
Cleared hypotheses: t, hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod
have h : ∀ (a : List ι) (hf : ∀ i ∈ ⟦a⟧, f₁ i ⊆ f₂ i), (Multiset.map f₁ ⟦a⟧).prod ⊆ (Multiset.map f₂ ⟦a⟧).prod
Tactic: induction t using Quotient.inductionOn
Cleared hypotheses: t, hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S)
    (∏ i ∈ l, S i)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
x : α
⊢ Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
have h : Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
  ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
Tactic: simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
x : α
h :
  Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
⊢ Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
have h₁ : (∃ x_1 ∈ (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S, ∏ i ∈ l, x_1 i = x) ↔
  ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
Tactic: simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
x : α
h :
  Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₁ :
  (∃ x_1 ∈ (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S, ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
⊢ Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
have h₂ : (∃ (x_1 : ι → α), (∀ i ∈ (↑l : Set ι), x_1 i ∈ S i) ∧ ∏ i ∈ l, x_1 i = x) ↔
  ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
Tactic: simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
x : α
h :
  Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₁ :
  (∃ x_1 ∈ (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S, ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₂ :
  (∃ (x_1 : ι → α), (∀ i ∈ (↑l : Set ι), x_1 i ∈ S i) ∧ ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
⊢ Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
have h₃ : (∃ (x_1 : ι → α), (∀ i ∈ (↑l : Set ι), x_1 i ∈ S i) ∧ ∏ i ∈ l, x_1 i = x) ↔
  ∃ (g : ι → α), (∀ {i : ι}, i ∈ l → g i ∈ S i) ∧ ∏ i ∈ l, g i = x
Tactic: simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
have inl : ∀ (h : (s * t).Infinite),
  Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
Tactic: obtain h | h := (s * t).infinite_or_finite
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
inl :
  ∀ (h : (s * t).Infinite),
    Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
have inr : ∀ (h : (s * t).Finite),
  Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
Tactic: obtain h | h := (s * t).infinite_or_finite
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
have inr : LE.le (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) #(↑(s * t) : Type u_2) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) (#(↑s : Type u_2) * #(↑t : Type u_2)) : ℕ)
Tactic: simp only [Nat.card, ← Cardinal.toNat_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
⊢ LE.le (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) #(↑(s * t) : Type u_2) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) (#(↑s : Type u_2) * #(↑t : Type u_2)) : ℕ)
have inr : #(↑s : Type u_2) * #(↑t : Type u_2) < ℵ₀
Tactic: refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
⊢ #(↑s⁻¹ : Type u_1) = #(↑s : Type u_1)
have rw : #(↑((fun (x : G) ↦ x⁻¹) '' s) : Type u_1) = #(↑s : Type u_1)
Tactic: rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
rw : #(↑((fun (x : G) ↦ x⁻¹) '' s) : Type u_1) = #(↑s : Type u_1)
⊢ #(↑s⁻¹ : Type u_1) = #(↑s : Type u_1)
have rw₁ : #(↑s : Type u_1) = #(↑s : Type u_1)
Tactic: rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Card (goal)
Goal:
G : Type u_1
inst : Group G
s t : Set G
⊢ Nat.card.{u_1} (↑(s / t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t : Type u_1)
have rw : Nat.card.{u_1} (↑(s * t⁻¹) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t⁻¹ : Type u_1)
Tactic: rw [div_eq_mul_inv, ← natCard_inv t]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
ih : DecidablePred fun (x : α) ↦ x ∈ s ^ n
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ (n + 1)
have succ : DecidablePred fun (x : α) ↦ x ∈ s ^ n * s
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ n
have zero : DecidablePred fun (x : α) ↦ x ∈ HPow.hPow (β := ℕ) s 0
Tactic: induction n with
  | zero =>
    simp only [pow_zero, mem_one]
    infer_instance
  | succ n ih =>
    rw [pow_succ]
    infer_instance
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
zero : DecidablePred fun (x : α) ↦ x ∈ HPow.hPow (β := ℕ) s 0
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ n
have succ : (n : ℕ) → (ih : DecidablePred fun (x : α) ↦ x ∈ s ^ n) → DecidablePred fun (x : α) ↦ x ∈ s ^ (n + 1)
Tactic: induction n with
  | zero =>
    simp only [pow_zero, mem_one]
    infer_instance
  | succ n ih =>
    rw [pow_succ]
    infer_instance
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ s⁻¹.Finite ↔ s.Finite
have rw : Set.Finite (α := α) ((fun (x : α) ↦ x⁻¹) '' s) ↔ s.Finite
Tactic: rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
rw : Set.Finite (α := α) ((fun (x : α) ↦ x⁻¹) '' s) ↔ s.Finite
⊢ s⁻¹.Finite ↔ s.Finite
have rw₁ : s.Finite ↔ s.Finite
Tactic: rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (hypothesis)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have hG : 0 < Fintype.card G
Tactic: have hG : 0 < Fintype.card G := Fintype.card_pos
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have inl : ∀ [inst_3 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k] (k : ℕ),
  Fintype.card G ≤ k →
    Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
Tactic: rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)
Cleared hypotheses: S, inst_2
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
inl :
  ∀ [inst_3 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k] (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
        Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have inr : ∀ (a : G) (ha : a ∈ S) (k : ℕ),
  Fintype.card G ≤ k → Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
Tactic: rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
hG : 0 < Fintype.card G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
        Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
have inl : (k : ℕ) →
  (hk : Fintype.card G ≤ k) →
    (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
Tactic: refine fun k hk ↦ Fintype.card_congr ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
hG : 0 < Fintype.card G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
have inl : (↑∅ : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
Tactic: rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
hG : 0 < Fintype.card G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k
k : ℕ
hk : Fintype.card G ≤ k
inl : (↑∅ : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
⊢ (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
have inl₁ : (↑∅ : Type u_5) ≃ (↑∅ : Type u_5)
Tactic: rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (goal)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
have refine : ∀ (a : G) (s t : Set G) (x : Fintype (↑s : Type u_5)) (x : Fintype (↑t : Type u_5)) (h : ∀ b ∈ s, b * a ∈ t),
  Function.Injective (β := (↑t : Type u_5)) fun (x : (↑s : Type u_5)) ↦
    match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
    | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) sorry
Tactic: refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (hypothesis)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have key : ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
  (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
Tactic: have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
      (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
    refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
    rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
    exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Finite (hypothesis)
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)
have mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
Tactic: have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
    monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha