awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0
have obtain : ∀ (t : Finset (ZMod n × ℕ)) (hts : t ⊆ s.toEnumFinset) (ht : #t = n ∧ Eq (α := ZMod n) (∑ i ∈ t, i.1) 0),
  ∃ t ≤ s, t.card = n ∧ t.sum = 0
Tactic: obtain ⟨t, hts, ht⟩ := ZMod.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)
-- 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 : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
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 : (map f₁ s).prod = (map f₂ t).prod
Tactic: rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
      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 : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
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 : (map f₁ s).prod = (map f₂ t).prod
⊢ (map f₂ s).prod = (map f₂ t).prod
have rw₁ : (map f₁ s).prod = (map f₁ t).prod
Tactic: rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
      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 : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
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 : (map f₁ s).prod = (map f₂ t).prod
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 [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
      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 : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod
have rw : Multiset.prod (map (fun (x : α) ↦ f₁ x) s) = (map f₂ t).prod ↔ s.prod = t.prod
Tactic: rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
      hf₁.map_prod_eq_map_prod hsA htA hs ht]
-- 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 : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
rw : Multiset.prod (map (fun (x : α) ↦ f₁ x) s) = (map f₂ t).prod ↔ s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod
have rw₁ : Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (x : α) ↦ f₁ x) s)) (Multiset.prod (map (fun (x : α) ↦ f₁ x) t)) ↔
  s.prod = t.prod
Tactic: rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
      hf₁.map_prod_eq_map_prod hsA htA hs ht]
-- 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 : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
rw : Multiset.prod (map (fun (x : α) ↦ f₁ x) s) = (map f₂ t).prod ↔ s.prod = t.prod
rw₁ :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (x : α) ↦ f₁ x) s)) (Multiset.prod (map (fun (x : α) ↦ f₁ x) t)) ↔
    s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod
have rw₂ : s.prod = t.prod ↔ s.prod = t.prod
Tactic: rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
      hf₁.map_prod_eq_map_prod hsA htA hs ht]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod
have rw : ∀ x ∈ t, (f ∘ g) x = id x
Tactic: rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id,
      map_map, map_congr rfl, map_id]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
rw : ∀ x ∈ t, (f ∘ g) x = id x
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod
have rw₁ : ∀ x ∈ s, (f ∘ g) x = id x
Tactic: rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id,
      map_map, map_congr rfl, map_id]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
rw : ∀ x ∈ t, (f ∘ g) x = id x
rw₁ : ∀ x ∈ s, (f ∘ g) x = id x
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod
have rw₂ : ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A
Tactic: rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id,
      map_map, map_congr rfl, map_id]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
rw : ∀ x ∈ t, (f ∘ g) x = id x
rw₁ : ∀ x ∈ s, (f ∘ g) x = id x
rw₂ : ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod
have rw₃ : ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A
Tactic: rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id,
      map_map, map_congr rfl, map_id]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod
have refine : ∀ (h' : (map f s).prod = (map f t).prod), s.prod = t.prod
Tactic: refine ⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have this : MapsTo f A B
Tactic: have := hf.mapsTo
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have hsA₁ : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
Tactic: apply hg.map_prod_eq_map_prod
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
hsA₁ : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have htA₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
Tactic: apply hg.map_prod_eq_map_prod
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
hsA₁ : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
htA₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have hs₁ : (map f s).card = n
Tactic: apply hg.map_prod_eq_map_prod
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
hsA₁ : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
htA₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
hs₁ : (map f s).card = n
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have ht₁ : (map f t).card = n
Tactic: apply hg.map_prod_eq_map_prod
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
⊢ s.prod = t.prod
have this : (map g (map f s)).prod = (map g (map f t)).prod
Tactic: have : (map g (map f s)).prod = (map g (map f t)).prod := by
      have := hf.mapsTo
      apply hg.map_prod_eq_map_prod <;> simp_all [MapsTo]
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map g (map f s)).prod = (map g (map f t)).prod
⊢ s.prod = t.prod
have rwa : ∀ (this : (map (g ∘ f) s).prod = (map g (map f t)).prod) (this : s.prod = (map (g ∘ f) t).prod) (x : α) (hx : x ∈ t),
  (g ∘ f) x = id x
Tactic: rwa [map_map, map_congr rfl fun x hx => ?g1, map_id, map_map,
      map_congr rfl fun x hx => ?g2, map_id] at this
Cleared hypotheses: this
-- 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 : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : (map g (map f s)).prod = (map g (map f t)).prod
rwa :
  ∀ (this : (map (g ∘ f) s).prod = (map g (map f t)).prod) (this : s.prod = (map (g ∘ f) t).prod) (x : α) (hx : x ∈ t),
    (g ∘ f) x = id x
⊢ s.prod = t.prod
have rwa₁ : ∀ (this : (map (g ∘ f) s).prod = (map g (map f t)).prod) (x : α) (hx : x ∈ s), (g ∘ f) x = id x
Tactic: rwa [map_map, map_congr rfl fun x hx => ?g1, map_id, map_map,
      map_congr rfl fun x hx => ?g2, map_id] at this
Cleared hypotheses: this
-- 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 : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : a * b = c * d
⊢ f a * f b = f c * f d
have simp_rw : ∀ (h : Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})),
  Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d})
Tactic: simp_rw [← prod_pair] at h ⊢
Cleared hypotheses: h
-- 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 : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
⊢ Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d})
have refine_1 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A
Tactic: refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h
-- 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 : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
refine_1 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A
⊢ Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d})
have refine_2 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} x → x ∈ A
Tactic: refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h
-- 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 : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ f a * f b = f c * f d ↔ a * b = c * d
have simp_rw : Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d}) ↔
  Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
Tactic: simp_rw [← prod_pair]
-- 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 : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d}) ↔
    Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
have refine_1 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A
Tactic: refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _)
-- 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 : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
refine_1 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A
⊢ Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d}) ↔
    Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
have refine_2 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} x → x ∈ A
Tactic: refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanHom n B C g
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 (g ∘ f) s).prod = (map (g ∘ f) t).prod
have rw : (map g (map f s)).prod = (map g (map f t)).prod
Tactic: rw [← map_map, ← map_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanHom n B C g
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 g (map f s)).prod = (map g (map f t)).prod
have refine_1 : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
Tactic: refine hg.map_prod_eq_map_prod ?_ ?_ (by rwa [card_map]) (by rwa [card_map])
      (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
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanHom n B C g
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
refine_1 : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod
have refine_2 : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
Tactic: refine hg.map_prod_eq_map_prod ?_ ?_ (by rwa [card_map]) (by rwa [card_map])
      (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
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso 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
⊢ (map (g ∘ f) s).prod = (map (g ∘ f) t).prod ↔ s.prod = t.prod
have rw : (map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod
Tactic: rw [← map_map, ← map_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso 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
⊢ (map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod
have rw : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
Tactic: rw [hg.map_prod_eq_map_prod _ _ (by rwa [card_map]) (by rwa [card_map]),
      hf.map_prod_eq_map_prod hsA htA hs ht]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.FreimanHom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso 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
rw : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod
have rw₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
Tactic: rw [hg.map_prod_eq_map_prod _ _ (by rwa [card_map]) (by rwa [card_map]),
      hf.map_prod_eq_map_prod hsA htA hs ht]
-- 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
⊢ (map (f₁ * f₂) s).prod = (map (f₁ * f₂) t).prod
have 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))
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:
α : 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))
⊢ (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.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:
α : 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)
⊢ (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.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:
α : 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
⊢ (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.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]