-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanHom.prod (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) :
    IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where
  mapsTo := h₁.mapsTo.prodMap h₂.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht h

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ ∀ ⦃x : α₁⦄, x ∈ map Prod.fst s → x ∈ A₁

Tactic:
simpa using hsA.1

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map Prod.fst s).card = n

Tactic:
simpa

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map Prod.snd s).card = n

Tactic:
simpa

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map Prod.fst t).card = n

Tactic:
simpa

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
⊢ (map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod

Tactic:
simp only [Prod.ext_iff, fst_prod, snd_prod, map_map, Function.comp_apply, Prod.map_fst,
  Prod.map_snd] at h ⊢

Result:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map (fun x => f₁ x.1) s).prod = (map (fun x => f₁ x.1) t).prod ∧
    (map (fun x => f₂ x.2) s).prod = (map (fun x => f₂ x.2) t).prod

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ ∀ ⦃x : α₁⦄, x ∈ map Prod.fst t → x ∈ A₁

Tactic:
simpa using htA.1

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map Prod.snd t).card = n

Tactic:
simpa

Result:
no goals

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
inst✝³ : CommMonoid α₁
inst✝² : CommMonoid α₂
inst✝¹ : CommMonoid β₁
inst✝ : CommMonoid β₂
A₁ : Set α₁
A₂ : Set α₂
B₁ : Set β₁
B₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
n : ℕ
h₁ : IsMulFreimanHom n A₁ B₁ f₁
h₂ : IsMulFreimanHom n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hs : s.card = n
ht : t.card = n
hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂
htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂
h : (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
⊢ (map f₁ (map Prod.fst s)).prod = (map f₁ (map Prod.fst t)).prod ∧
    (map f₂ (map Prod.snd s)).prod = (map f₂ (map Prod.snd t)).prod

Tactic:
exact ⟨h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa)
  (by simpa) h.1, h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2)
  (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa) h.2⟩

Result:
no goals