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 : α → β
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
⊢ ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B

Tactic:
simp_all [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 f s).card = n

Tactic:
simp_all [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 f t).card = n

Tactic:
simp_all [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 f s).prod = (map f t).prod

Tactic:
simp_all [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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

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]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rwa₁ : ∀ (this : (map (g ∘ f) s).prod = (map g (map f t)).prod) (x : α) (hx : x ∈ s), (g ∘ f) x = id x
⊢ s.prod = t.prod

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

Premises used: Multiset.map_id, Multiset.map_congr, Multiset.map_map, rfl
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x

Tactic:
h.1 (hsA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x

Tactic:
exact h.1 (hsA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 ∘ f) s).prod = (map g (map f t)).prod
x : α
hx : x ∈ s
⊢ (g ∘ f) x = id x

Tactic:
case g1 => exact h.1 (hsA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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_1 : (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:
h.1 (htA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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_1 : (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:
exact h.1 (htA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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_1 : (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:
case g2 => exact h.1 (htA hx)

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanIso n A B f
⊢ IsMulFreimanIso n B A (Function.invFunOn f A)

Tactic:
hf.symm hf.bijOn.surjOn.mapsTo_invFunOn hf.bijOn.surjOn.rightInvOn_invFunOn

Premises used: Set.SurjOn.mapsTo_invFunOn, IsMulFreimanIso.symm, IsMulFreimanIso.bijOn, Set.SurjOn.rightInvOn_invFunOn, Set.BijOn.surjOn
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Finset α
hsA : (↑s : Set α) ⊆ A
htA : (↑t : Set α) ⊆ A
hs : s.card = n
ht : t.card = n
⊢ Eq (α := α) (∏ i ∈ s, i) (∏ i ∈ t, i) → Eq.{u_3 + 1} (α := β) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
simpa using hf.map_prod_eq_map_prod hsA htA hs ht

Premises used: IsMulFreimanHom.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
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})
⊢ f a * f b = f c * f d

Tactic:
simp_rw [← prod_pair] at h ⊢

Premises used: Multiset.prod_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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})

Tactic:
hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h

Premises used: Multiset.map, IsMulFreimanHom.map_prod_eq_map_prod, List.map, Multiset.cons, Multiset.ofList, Multiset.card_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
refine_2 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} x → x ∈ A
⊢ Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d})

Tactic:
refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Multiset.card_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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})
⊢ ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A

Tactic:
simp [ha, hb, hc, hd]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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})
⊢ ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} x → x ∈ A

Tactic:
simp [ha, hb, hc, hd]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
simp_rw :
  Eq (α := β) (Multiset.prod {f a, f b}) (Multiset.prod {f c, f d}) ↔
    Eq (α := α) (Multiset.prod {a, b}) (Multiset.prod {c, d})
⊢ f a * f b = f c * f d ↔ a * b = c * d

Tactic:
simp_rw [← prod_pair]

Premises used: Multiset.prod_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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})

Tactic:
hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _)

Premises used: Multiset.map, List.map, IsMulFreimanIso.map_prod_eq_map_prod, Multiset.cons, Multiset.ofList, Multiset.card_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
refine_2 : ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} 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})

Tactic:
refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _)

Premises used: IsMulFreimanIso.map_prod_eq_map_prod, Multiset.card_pair
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {a, b} x → x ∈ A

Tactic:
simp [ha, hb, hc, hd]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : α⦄, Membership.mem (γ := Multiset α) {c, d} x → x ∈ A

Tactic:
simp [ha, hb, hc, hd]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
⊢ ∀ ⦃s t : Multiset α⦄ (hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : s.card = 2)
    (ht : t.card = 2) (h : s.prod = t.prod), (map f s).prod = (map f t).prod

Tactic:
aesop (add simp card_eq_two)

Premises used: Multiset.card_eq_two
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d
⊢ ∀ ⦃s t : Multiset α⦄ (hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : s.card = 2)
    (ht : t.card = 2), (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
aesop (add simp card_eq_two)

Premises used: Multiset.card_eq_two
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
inst : CommMonoid α
A₁ A₂ : Set α
n : ℕ
hA : A₁ ⊆ A₂
s t : Multiset α
h_1 : ∀ ⦃x : α⦄, x ∈ s → x ∈ A₁
h_2 : ∀ ⦃x : α⦄, x ∈ t → x ∈ A₁
h_3 : s.card = n
h_4 : t.card = n
h : s.prod = t.prod
⊢ (map id s).prod = (map id t).prod

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
inst : CommMonoid α
A : Set α
n : ℕ
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
⊢ (map id s).prod = (map id t).prod ↔ s.prod = t.prod

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rw : (map g (map f s)).prod = (map g (map f t)).prod
⊢ (map (g ∘ f) s).prod = (map (g ∘ f) t).prod

Tactic:
rw [← map_map, ← map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rwa rwa₁ rwa₂ rwa₃ : s.card = n
⊢ (map f s).card = n

Tactic:
rwa [card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rwa rwa₁ rwa₂ rwa₃ : t.card = n
⊢ (map f t).card = n

Tactic:
rwa [card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
refine_2 : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod

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)

Premises used: IsMulFreimanHom.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

Tactic:
simpa using fun a h ↦ hf.mapsTo (hsA h)

Premises used: IsMulFreimanHom.mapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B

Tactic:
simpa using fun a h ↦ hf.mapsTo (htA h)

Premises used: IsMulFreimanHom.mapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 : (map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod
⊢ (map (g ∘ f) s).prod = (map (g ∘ f) t).prod ↔ s.prod = t.prod

Tactic:
rw [← map_map, ← map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rwa rwa₁ rwa₂ rwa₃ : s.card = n
⊢ (map f s).card = n

Tactic:
rwa [card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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 rwa rwa₁ rwa₂ rwa₃ : t.card = n
⊢ (map f t).card = n

Tactic:
rwa [card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
rw₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
⊢ (map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod

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]

Premises used: IsMulFreimanIso.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

Tactic:
simpa using fun a h ↦ hf.bijOn.mapsTo (hsA h)

Premises used: IsMulFreimanIso.bijOn, Set.BijOn.mapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
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
⊢ ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B

Tactic:
simpa using fun a h ↦ hf.bijOn.mapsTo (htA h)

Premises used: IsMulFreimanIso.bijOn, Set.BijOn.mapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B₁ B₂ : Set β
f : α → β
n : ℕ
hB : B₁ ⊆ B₂
hf : IsMulFreimanHom n A B₁ f
⊢ IsMulFreimanHom n A B₂ f

Tactic:
(isMulFreimanHom_id hB).comp hf

Premises used: IsMulFreimanHom.comp, isMulFreimanHom_id
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A₁ A₂ : Set α
B₁ B₂ : Set β
f : α → β
n : ℕ
hA : A₁ ⊆ A₂
hf : IsMulFreimanIso n A₂ B₂ f
hf' : BijOn f A₁ B₁
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

Tactic:
hf.map_prod_eq_map_prod (fun a ha ↦ hA (hsA ha)) (fun a ha ↦ hA (htA ha)) hs ht

Premises used: IsMulFreimanIso.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A₁ A₂ : Set α
B₁ B₂ : Set β
f : α → β
n : ℕ
hA : A₁ ⊆ A₂
hf : IsMulFreimanIso n A₂ B₂ f
hf' : BijOn f A₁ B₁
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

Tactic:
refine hf.map_prod_eq_map_prod (fun a ha ↦ hA (hsA ha)) (fun a ha ↦ hA (htA ha)) hs ht

Premises used: IsMulFreimanIso.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
n : ℕ
b : β
hb : b ∈ B
s t : Multiset α
h : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
h_1 : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h_2 : s.prod = t.prod
⊢ Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (x : α) ↦ b) s)) (Multiset.prod (map (fun (x : α) ↦ b) t))

Tactic:
simp only [map_const', hs, prod_replicate, ht]

Premises used: Multiset.prod_replicate, Multiset.map_const'
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
h : MapsTo f A B
⊢ ∀ ⦃s t : Multiset α⦄ (hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : s.card = 0)
    (ht : t.card = 0) (h : s.prod = t.prod), (map f s).prod = (map f t).prod

Tactic:
simp_all
-- 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 = 0)
    (ht : t.card = 0), (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
h : MapsTo 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) (h : s.prod = t.prod), (map f s).prod = (map f t).prod

Tactic:
aesop (add simp card_eq_one)

Premises used: Multiset.card_eq_one