-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanIso.mono {hmn : m ≤ n} (hf : IsMulFreimanIso n A B f) :
    IsMulFreimanIso m A B f where
  bijOn := hf.bijOn
  map_prod_eq_map_prod s t hsA htA hs ht

Proof state:
case inr.intro.refine_1.inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ replicate (n - m) a✝
⊢ a ∈ A

Tactic:
rwa [eq_of_mem_replicate ha]

Result:
no goals

Proof state:
case inr.intro.refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ t
⊢ a ∈ A

Tactic:
exact htA ha

Result:
no goals

Proof state:
case inr.intro.refine_1.inl
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ s
⊢ a ∈ A

Tactic:
exact hsA ha

Result:
no goals

Proof state:
case inr.intro.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ t ∨ a ∈ replicate (n - m) a✝
⊢ a ∈ A

Tactic:
obtain ha | ha := ha

Result:
case inr.intro.refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ t
⊢ a ∈ A

case inr.intro.refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ replicate (n - m) a✝
⊢ a ∈ A

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
hm : m > 0
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
simp only [← hs, card_pos_iff_exists_mem] at hm

Result:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
hm : ∃ a, a ∈ s
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Proof state:
case inr.intro.refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ s + replicate (n - m) a✝
⊢ a ∈ A

Tactic:
rw [Multiset.mem_add] at ha

Result:
case inr.intro.refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ s ∨ a ∈ replicate (n - m) a✝
⊢ a ∈ A

Proof state:
case inr.intro
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a : α
ha : a ∈ s
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
suffices
  ((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod ↔
  (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod by
  simpa only [Multiset.map_add, prod_add, mul_right_cancel_iff] using this

Result:
case inr.intro
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a : α
ha : a ∈ s
⊢ (map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod ↔
    (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
obtain rfl | hm := m.eq_zero_or_pos

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hmn : 0 ≤ n
hs : s.card = 0
ht : t.card = 0
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

case inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
hm : m > 0
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Proof state:
case inr.intro.refine_3
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a : α
ha : a ∈ A
⊢ (s + replicate (n - m) a).card = n

Tactic:
rw [card_add, card_replicate, hs, Nat.add_sub_cancel' hmn]

Result:
no goals

Proof state:
case inr.intro.refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ replicate (n - m) a✝
⊢ a ∈ A

Tactic:
rwa [eq_of_mem_replicate ha]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
a : α
ha : a ∈ s
this :
  (map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod ↔
    (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
simpa only [Multiset.map_add, prod_add, mul_right_cancel_iff] using this

Result:
no goals