awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
h : BijOn f A B
⊢ ∀ ⦃s t : Multiset α⦄ (hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : s.card = 1)
    (ht : t.card = 1), (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
aesop (add simp [card_eq_one, BijOn])

Premises used: Set.BijOn, Multiset.card_eq_one
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
B : Set β
f : α → β
n : ℕ
s t : Multiset α
⊢ ∀ (hsA : ∀ ⦃x : α⦄, x ∈ s → Membership.mem (γ := Set α) ∅ x)
    (htA : ∀ ⦃x : α⦄, x ∈ t → Membership.mem (γ := Set α) ∅ x) (hs : s.card = n) (ht : t.card = n)
    (h : s.prod = t.prod), (map f s).prod = (map f t).prod

Tactic:
aesop (add simp eq_zero_of_forall_notMem)

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
f : α → β
n : ℕ
s t : Multiset α
hs : ∀ ⦃x : α⦄, x ∈ s → Membership.mem (γ := Set α) ∅ x
ht : ∀ ⦃x : α⦄, x ∈ t → Membership.mem (γ := Set α) ∅ x
⊢ ∀ (hs : s.card = n) (ht : t.card = n), (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
simp [eq_zero_of_forall_notMem hs, eq_zero_of_forall_notMem ht]

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rw₄ rw₅ : (map f₁ t).prod * (map f₂ t).prod = (map f₁ t).prod * (map f₂ t).prod
⊢ (map (f₁ * f₂) s).prod = (map (f₁ * 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]

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Multiset.prod_map_mul, Pi.mul_def
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f : (a : α) → β) A B
⊢ IsMulFreimanHom 0 A B (⇑f : (a : α) → β)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ s ≠ 0

Tactic:
grind [Multiset.card_eq_zero]

Premises used: Multiset.card_eq_zero
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ t ≠ 0

Tactic:
grind [Multiset.card_eq_zero]

Premises used: Multiset.card_eq_zero
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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) : β)
rw₂ rw₃ : Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) t)) (Multiset.prod (map (⇑f : (a : α) → β) t))
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (⇑f : (a : α) → β) s)) (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])]

Premises used: map_multiset_ne_zero_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rw₂ rw₃ : s.prod = 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

Tactic:
rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]

Premises used: EquivLike.apply_eq_iff_eq, map_multiset_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
inst : CommMonoid α
n : ℕ
S : Type u_5
inst_1 : SetLike S α
inst_2 : SubmonoidClass S α
s : S
⊢ IsMulFreimanHom.{u_2, u_2} (α := ↥s) n univ univ (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
MulHomClass.isMulFreimanHom (SubmonoidClass.subtype s) (mapsTo_univ ..)

Premises used: Set.mapsTo_univ, SubmonoidClass.subtype, MulHomClass.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
hf : IsMulFreimanHom (HAdd.hAdd (α := ℕ) 0 1) A B f
hs : s.card = 0
h_1 : t.card = 0
⊢ (map f s).prod = (map f t).prod

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ 0 < s.card

Tactic:
simp [hs]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
have : ∀ (a : α) (ha : a ∈ s), (map f s).prod = (map f t).prod
⊢ (map f s).prod = (map f t).prod

Tactic:
have ⟨a, ha⟩ : ∃ a, a ∈ s := card_pos_iff_exists_mem.1 (by simp [hs])
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
a : α
ha : a ∈ s
⊢ ∀ ⦃x : α⦄, x ∈ a ::ₘ s → x ∈ A

Tactic:
simpa [hsA ha]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
a : α
ha : a ∈ s
⊢ ∀ ⦃x : α⦄, x ∈ a ::ₘ t → x ∈ A

Tactic:
simpa [hsA ha]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
a : α
ha : a ∈ s
⊢ (map f s).prod = (map f t).prod

Tactic:
simpa [*] using hf.map_prod_eq_map_prod (s := a ::ₘ s) (t := a ::ₘ t)
            (by simpa [hsA ha]) (by simpa [hsA ha])

Premises used: IsMulFreimanHom.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
⊢ IsMulFreimanHom m A B f

Tactic:
isMulFreimanHom_antitone hmn hf

Premises used: isMulFreimanHom_antitone
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CancelCommMonoid α
inst_1 : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
⊢ IsMulFreimanIso m A B f

Tactic:
(hf.isMulFreimanHom.mono hmn).to_isMulFreimanIso hf.bijOn.invOn_invFunOn
    (hf.invFunOn.isMulFreimanHom.mono hmn)

Premises used: IsMulFreimanHom.mono, IsMulFreimanIso.bijOn, IsMulFreimanIso.invFunOn, Set.BijOn.invOn_invFunOn, IsMulFreimanHom.to_isMulFreimanIso, IsMulFreimanIso.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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⁻¹
rw₃ rw₄ : (map f t).prod⁻¹ = (map f t).prod⁻¹
⊢ (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]

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Pi.inv_def, Multiset.prod_map_inv
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rw₄ rw₅ : (map f₁ t).prod / (map f₂ t).prod = (map f₁ t).prod / (map f₂ t).prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / 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]

Premises used: Pi.div_def, IsMulFreimanHom.map_prod_eq_map_prod, Multiset.prod_map_div
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
⊢ IsMulFreimanHom n (A ×ˢ B) A Prod.fst

Tactic:
MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) mapsTo_fst_prod

Premises used: Set.mapsTo_fst_prod, MonoidHom.fst, MulHomClass.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
⊢ IsMulFreimanHom n (A ×ˢ B) B Prod.snd

Tactic:
MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) mapsTo_snd_prod

Premises used: Set.mapsTo_snd_prod, MulHomClass.isMulFreimanHom, MonoidHom.snd
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_5
β₁ : Type u_6
β₂ : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid β₁
inst_2 : CommMonoid β₂
A : Set α
B₁ : Set β₁
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
⊢ Eq (α := β₁ × β₂) (Multiset.prod (map (fun (x : α) ↦ (f₁ x, f₂ x)) s))
    (Multiset.prod (map (fun (x : α) ↦ (f₁ x, f₂ x)) t))

Tactic:
simp [Prod.ext_iff, fst_prod, snd_prod,
      h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h]

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Prod.ext_iff, Multiset.snd_prod, Multiset.fst_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst : CommMonoid α₁
inst_1 : CommMonoid α₂
inst_2 : CommMonoid β₁
inst_3 : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
⊢ IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

Tactic:
(h₁.comp .fst).prodMk (h₂.comp .snd)

Premises used: IsMulFreimanHom.comp, Prod.map, IsMulFreimanHom.snd, IsMulFreimanHom.prodMk, IsMulFreimanHom.fst
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst : CommMonoid α₁
inst_1 : CommMonoid α₂
inst_2 : CommMonoid β₁
inst_3 : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso n A₂ B₂ f₂
⊢ IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

Tactic:
(h₁.isMulFreimanHom.prodMap h₂.isMulFreimanHom).to_isMulFreimanIso
    (h₁.bijOn.invOn_invFunOn.prodMap h₂.bijOn.invOn_invFunOn)
    (h₁.invFunOn.isMulFreimanHom.prodMap h₂.invFunOn.isMulFreimanHom)

Premises used: IsMulFreimanIso.bijOn, Set.InvOn.prodMap, IsMulFreimanIso.invFunOn, Set.BijOn.invOn_invFunOn, IsMulFreimanHom.prodMap, IsMulFreimanHom.to_isMulFreimanIso, IsMulFreimanIso.isMulFreimanHom
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
⊢ k < n + 1

Tactic:
Nat.lt_succ_iff.2 <| le_trans (Nat.le_mul_of_pos_left _ hm.bot_lt) hkmn

Premises used: Iff.mpr, Nat.lt_succ_iff, Nat.le_mul_of_pos_left, Ne.bot_lt, le_trans
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
⊢ MapsTo (α := Fin (n + 1)) val (Iic (↑k : Fin (n + 1))) (Iic k)

Tactic:
simp [MapsTo, Fin.le_iff_val_le_val, Nat.mod_eq_of_lt, aux hm hkmn]

Premises used: _private.0.Fin.aux, Nat.mod_eq_of_lt, Set.MapsTo, Fin.le_iff_val_le_val
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
x : ℕ
hx : x ≤ k
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Iic (↑k : Fin (n + 1))) (↑x : Fin (n + 1)) ∧ (↑(↑x : Fin (n + 1)) : ℕ) = x

Tactic:
simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn, hx.trans_lt]

Premises used: _private.0.Fin.aux, Nat.mod_eq_of_lt, LE.le.trans_lt, Fin.val_fin_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
u : Multiset (Fin (n + 1))
⊢ (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ (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
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
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))
⊢ (map val s).sum = (map val t).sum ↔ s.sum = t.sum

Tactic:
rw [← this, ← this]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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) → ℕ
rw₁ : Type
⊢ (map val u).sum ≤ m * k

Tactic:
rw [← hu, ← card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 ≤ (map val u).card * k

Tactic:
sum_le_card_nsmul (u.map val) k ?_

Premises used: Multiset.map, Multiset.sum_le_card_nsmul, Fin.val
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ x ∈ map val u, x ≤ k

Tactic:
simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk

Premises used: _private.0.Fin.aux, Nat.mod_eq_of_lt, Fin.val_fin_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 < 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
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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_1 : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
this : ∀ {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))) (hu : u.card = m), (map val u).sum < n + 1
⊢ (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:
⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩

Premises used: CharP.natCast_injOn_Iio, congr_arg, HAdd.hAdd, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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_1 : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1)) : (a : ℕ) → Fin (n + 1)) (map val u).sum = u.sum
this : ∀ {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ (↑k : Fin (n + 1))) (hu : u.card = m), (map val u).sum < n + 1
⊢ (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:
exact ⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
succ :
  ∀ (k : ℕ) (hkmn : m * (k + 1) ≤ n),
    IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑k : Fin (n + 1))) (Iio k) val

Tactic:
obtain _ | k := k
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
hkmn : m * 0 ≤ n
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑0 : Fin (n + 1))) (Iio 0) val

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
⊢ m * k ≤ n

Tactic:
have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iic (↑k : Fin (n + 1))) (Iic k) val

Tactic:
isAddFreimanIso_Iic hm hkmn'

Premises used: Fin.isAddFreimanIso_Iic
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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)))
h₁ : Iio (k + 1) = Iic k
⊢ IsAddFreimanIso (α := Fin (n + 1)) m (Iio (↑(k + 1) : Fin (n + 1))) (Iio (k + 1)) val

Tactic:
convert! isAddFreimanIso_Iic hm hkmn' using 1

Premises used: Fin.isAddFreimanIso_Iic