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

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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso n A₂ B₂ f₂
s t : Multiset (α₁ × α₂)
hsA : ∀ ⦃x : α₁ × α₂⦄, x ∈ s → x ∈ A₁ ×ˢ A₂
htA : ∀ ⦃x : α₁ × α₂⦄, x ∈ t → x ∈ A₁ ×ˢ A₂
hs : s.card = n
ht : t.card = n
⊢ (map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod ↔ s.prod = t.prod

Tactic:
simp only [mem_prod, forall_and, Prod.forall] at hsA htA

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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod ↔ s.prod = 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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ ∀ ⦃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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod ↔ s.prod = t.prod

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

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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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 ↔
    (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd 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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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 ↔
    (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod

Tactic:
rw [← Function.comp_def, ← map_map, ← map_map, ← Function.comp_def f₂, ← map_map, ← map_map,
  h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa) (by simpa),
  h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2)
  (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by 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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ (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₁ : IsMulFreimanIso n A₁ B₁ f₁
h₂ : IsMulFreimanIso 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₂
⊢ ∀ ⦃x : α₂⦄, x ∈ map Prod.snd t → x ∈ A₂

Tactic:
simpa [@forall_swap α₁] using htA.2

Result:
no goals