awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B₁ B₂ : Set β
f₁ f₂ : α → β
n : ℕ
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i * f₂ i) s))
    (Multiset.prod (map (fun (i : α) ↦ f₁ i * f₂ i) t))
rw₁ : (map f₁ s).prod * (map f₂ s).prod = Multiset.prod (map (fun (i : α) ↦ f₁ i * f₂ i) t)
rw₂ : (map f₁ s).prod * (map f₂ s).prod = (map f₁ t).prod * (map f₂ t).prod
rw₃ : (map f₁ t).prod * (map f₂ s).prod = (map f₁ t).prod * (map f₂ t).prod
⊢ (map (f₁ * f₂) s).prod = (map (f₁ * f₂) t).prod
have rw₄ : (map f₁ t).prod * (map f₂ t).prod = (map f₁ t).prod * (map f₂ t).prod
Tactic: rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n_1 : ℕ
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f : (a : α) → β) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t))
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β)
Tactic: rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),
        h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n_1 : ℕ
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f : (a : α) → β) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β)
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t))
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) t.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β)
Tactic: rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),
        h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n_1 : ℕ
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f : (a : α) → β) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) t.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β)
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t))
have rw₂ : Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) t)) (Multiset.prod (map (⇑f : (a : α) → β) t))
Tactic: rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),
        h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
hfAB : BijOn (⇑f : (a : α) → β) A B
s t : Multiset α
h : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
h_1 : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h_2 : s.card = n
h_3 : t.card = n
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t)) ↔
    s.prod = t.prod
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β) ↔ s.prod = t.prod
Tactic: rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
hfAB : BijOn (⇑f : (a : α) → β) A B
s t : Multiset α
h : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
h_1 : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h_2 : s.card = n
h_3 : t.card = n
rw :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β) ↔ s.prod = t.prod
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t)) ↔
    s.prod = t.prod
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) ((f : (a : α) → β) t.prod : β) ↔ s.prod = t.prod
Tactic: rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
hfAB : BijOn (⇑f : (a : α) → β) A B
s t : Multiset α
h : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
h_1 : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h_2 : s.card = n
h_3 : t.card = n
rw :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) (Multiset.prod (map (⇑f : (a : α) → β) t) : β) ↔ s.prod = t.prod
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) s.prod : β) ((f : (a : α) → β) t.prod : β) ↔ s.prod = t.prod
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (Multiset.prod (map (⇑f : (a : α) → β) t)) ↔
    s.prod = t.prod
have rw₂ : s.prod = t.prod ↔ s.prod = t.prod
Tactic: rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n_1 : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
n : ℕ
hf : IsMulFreimanHom (n + 1 + 1) A B f
hs : s.card = n + 1
h_1 : t.card = n + 1
⊢ (map f s).prod = (map f t).prod
have have : ∀ (a : α) (ha : a ∈ s), (map f s).prod = (map f t).prod
Tactic: have ⟨a, ha⟩ : ∃ a, a ∈ s := card_pos_iff_exists_mem.1 (by simp [hs])
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : DivisionCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map f⁻¹ s).prod = (map f⁻¹ t).prod
have rw : Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) s)) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t))
Tactic: rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : DivisionCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) s)) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t))
⊢ (map f⁻¹ s).prod = (map f⁻¹ t).prod
have rw₁ : (map f s).prod⁻¹ = Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t)
Tactic: rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : DivisionCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) s)) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t))
rw₁ : (map f s).prod⁻¹ = Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t)
⊢ (map f⁻¹ s).prod = (map f⁻¹ t).prod
have rw₂ : (map f s).prod⁻¹ = (map f t).prod⁻¹
Tactic: rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : DivisionCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) s)) (Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t))
rw₁ : (map f s).prod⁻¹ = Multiset.prod (map (fun (i : α) ↦ (f i)⁻¹) t)
rw₂ : (map f s).prod⁻¹ = (map f t).prod⁻¹
⊢ (map f⁻¹ s).prod = (map f⁻¹ t).prod
have rw₃ : (map f t).prod⁻¹ = (map f t).prod⁻¹
Tactic: rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst_1 : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
have rw : Eq.{u_5 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) s))
  (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t))
Tactic: rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst_1 : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_5 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) s))
    (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t))
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
have rw₁ : (map f₁ s).prod / (map f₂ s).prod = Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t)
Tactic: rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst_1 : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_5 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) s))
    (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t))
rw₁ : (map f₁ s).prod / (map f₂ s).prod = Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t)
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
have rw₂ : (map f₁ s).prod / (map f₂ s).prod = (map f₁ t).prod / (map f₂ t).prod
Tactic: rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst_1 : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_5 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) s))
    (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t))
rw₁ : (map f₁ s).prod / (map f₂ s).prod = Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t)
rw₂ : (map f₁ s).prod / (map f₂ s).prod = (map f₁ t).prod / (map f₂ t).prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
have rw₃ : (map f₁ t).prod / (map f₂ s).prod = (map f₁ t).prod / (map f₂ t).prod
Tactic: rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst_1 : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
rw :
  Eq.{u_5 + 1} (α := β) (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) s))
    (Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t))
rw₁ : (map f₁ s).prod / (map f₂ s).prod = Multiset.prod (map (fun (i : α) ↦ f₁ i / f₂ i) t)
rw₂ : (map f₁ s).prod / (map f₂ s).prod = (map f₁ t).prod / (map f₂ t).prod
rw₃ : (map f₁ t).prod / (map f₂ s).prod = (map f₁ t).prod / (map f₂ t).prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
have rw₄ : (map f₁ t).prod / (map f₂ t).prod = (map f₁ t).prod / (map f₂ t).prod
Tactic: rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (hypothesis)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
⊢ (map val s).sum = (map val t).sum ↔ s.sum = t.sum
have this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
Tactic: have (u : Multiset (Fin (n + 1))) : Nat.castRingHom _ (u.map val).sum = u.sum := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
⊢ (map val s).sum = (map val t).sum ↔ s.sum = t.sum
have rw : (map val s).sum = (map val t).sum ↔
  Eq (α := Fin (n + 1)) ((Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val s).sum : Fin (n + 1))
    ((Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val t).sum : Fin (n + 1))
Tactic: rw [← this, ← this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))
hu : u.card = m
⊢ (map val u).sum ≤ m * k
have rw : (map val u).sum ≤ (map val u).card * k
Tactic: rw [← hu, ← card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))
hu : u.card = m
rw : (map val u).sum ≤ (map val u).card * k
⊢ (map val u).sum ≤ m * k
have f : Fin (n + 1) → ℕ
Tactic: rw [← hu, ← card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))
hu : u.card = m
rw : (map val u).sum ≤ (map val u).card * k
f : Fin (n + 1) → ℕ
⊢ (map val u).sum ≤ m * k
have rw₁ : Type
Tactic: rw [← hu, ← card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (hypothesis)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
⊢ (map val s).sum = (map val t).sum ↔
    Eq (α := Fin (n + 1)) ((Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val s).sum : Fin (n + 1))
      ((Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val t).sum : Fin (n + 1))
have this₁ : ∀ {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))) (hu : u.card = m), (map val u).sum < n + 1
Tactic: have {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ k) (hu : card u = m) :
        (u.map val).sum < (n + 1) := Nat.lt_succ_iff.2 <| hkmn.trans' <| by
      rw [← hu, ← card_map]
      refine sum_le_card_nsmul (u.map val) k ?_
      simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑k : Fin (n + 1))) (Iio k) val
have zero : ∀ (hkmn : m * 0 ≤ n), IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑0 : Fin (n + 1))) (Iio 0) val
Tactic: obtain _ | k := k
Cleared hypotheses: k, hkmn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
zero : ∀ (hkmn : m * 0 ≤ n), IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑0 : Fin (n + 1))) (Iio 0) val
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑k : Fin (n + 1))) (Iio k) val
have succ : ∀ (k : ℕ) (hkmn : m * (k + 1) ≤ n),
  IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val
Tactic: obtain _ | k := k
Cleared hypotheses: k, hkmn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (hypothesis)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val
have hkmn' : m * k ≤ n
Tactic: have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val
have h : Eq (α := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) (Iic (↑k : Fin (n + 1)))
Tactic: convert! isAddFreimanIso_Iic hm hkmn' using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
h : Eq (α := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) (Iic (↑k : Fin (n + 1)))
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val
have h₁ : Iio (k + 1) = Iic k
Tactic: convert! isAddFreimanIso_Iic hm hkmn' using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Eq (α := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) (Iic (↑k : Fin (n + 1)))
have h : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) x ↔
    Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio (k + 1) = Iic k
have h : ∀ (x : ℕ), x ∈ Iio (k + 1) ↔ x ∈ Iic k
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Iio (↑(k + 1) : Fin (n + 1))) x ↔
    Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) x
have h : (↑x : ℕ) < (↑(HAdd.hAdd (α := Fin (n + 1)) (↑k : Fin (n + 1)) 1) : ℕ) ↔ (↑x : ℕ) ≤ k
Tactic: simp only [Nat.cast_add, Nat.cast_one, mem_Iio, lt_def, mem_Iic, le_iff_val_le_val,
      val_natCast, aux hm hkmn', Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ (↑x : ℕ) < (↑(HAdd.hAdd (α := Fin (n + 1)) (↑k : Fin (n + 1)) 1) : ℕ) ↔ (↑x : ℕ) ≤ k
have h : (↑x : ℕ) < (↑(↑(k + 1) : Fin (n + 1)) : ℕ) ↔ (↑x : ℕ) ≤ k
Tactic: simp_rw [← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ (↑x : ℕ) < (↑(↑(k + 1) : Fin (n + 1)) : ℕ) ↔ (↑x : ℕ) ≤ k
have h : (↑x : ℕ) < k + 1 ↔ (↑x : ℕ) ≤ k
Tactic: rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
h : (↑x : ℕ) < k + 1 ↔ (↑x : ℕ) ≤ k
⊢ (↑x : ℕ) < (↑(↑(k + 1) : Fin (n + 1)) : ℕ) ↔ (↑x : ℕ) ≤ k
have h₁ : (↑x : ℕ) ≤ k ↔ (↑x : ℕ) ≤ k
Tactic: rw [Fin.val_cast_of_lt (aux hm hkmn), Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(C / B)
have rw : #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
Tactic: rw [← card_product (A / B), ← mul_one #((A / B) ×ˢ (C / B))]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #((A / B) ×ˢ (C / B)) * 1
have refine_1 : ∀ (x : G) (hx : x ∈ A / C),
  #B ≤
    #(bipartiteAbove
        (fun (b : G) (x : G × G) ↦
          match (motive := G × G → Prop) x with
          | (a, c) => a / c = b)
        ((A / B) ×ˢ (C / B)) x)
Tactic: refine card_mul_le_card_mul (fun b (a, c) ↦ a / c = b) (fun x hx ↦ ?_)
    fun x _ ↦ card_le_one_iff.2 fun hu hv ↦
      ((mem_bipartiteBelow _).1 hu).2.symm.trans ?_