case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : ↑card s = 0
ht : ↑card t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)

case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : m > 0
⊢ prod (map (↑f) s) = prod (map (↑f) t)
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
obtain rfl | hm := m.eq_zero_or_pos
case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : ∃ a, a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : m > 0
⊢ prod (map (↑f) s) = prod (map (↑f) t)
simp [← hs, card_pos_iff_exists_mem] at hm
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : ∃ a, a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
obtain ⟨a, ha⟩ := hm
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
suffices
  ((s + Multiset.replicate (n - m) a).map f).prod =
    ((t + Multiset.replicate (n - m) a).map f).prod by
  simp_rw [Multiset.map_add, prod_add] at this
  exact mul_right_cancel this
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
replace ha := hsA _ ha
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ s + replicate (n - m) a → x ∈ A

F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ t + replicate (n - m) a → x ∈ A

F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (s + replicate (n - m) a) = n

F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (t + replicate (n - m) a) = n

F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (s + replicate (n - m) a) = prod (t + replicate (n - m) a)
case inr.intro
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
apply map_prod_eq_map_prod f (A := A) (β := β) (n := n) (fun x hx => _) (fun x hx => _) _ _ _
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : s = 0
ht : t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : ↑card s = 0
ht : ↑card t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
rw [card_eq_zero] at hs ht
no goals
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : s = 0
ht : t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
rw [hs, ht]
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
this :
  prod (map (fun x => ↑f x) s) * prod (map (fun x => ↑f x) (replicate (n - m) a)) =
    prod (map (fun x => ↑f x) t) * prod (map (fun x => ↑f x) (replicate (n - m) a))
⊢ prod (map (↑f) s) = prod (map (↑f) t)
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
this : prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
⊢ prod (map (↑f) s) = prod (map (↑f) t)
simp_rw [Multiset.map_add, prod_add] at this
no goals
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
this :
  prod (map (fun x => ↑f x) s) * prod (map (fun x => ↑f x) (replicate (n - m) a)) =
    prod (map (fun x => ↑f x) t) * prod (map (fun x => ↑f x) (replicate (n - m) a))
⊢ prod (map (↑f) s) = prod (map (↑f) t)
exact mul_right_cancel this
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s + replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ s + replicate (n - m) a → x ∈ A
intro x hx
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s + replicate (n - m) a
⊢ x ∈ A
rw [mem_add] at hx
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s
⊢ x ∈ A

case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
cases' hx with hx hx
no goals
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s
⊢ x ∈ A
exact hsA x hx
no goals
case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
rwa [eq_of_mem_replicate hx]
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t + replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ t + replicate (n - m) a → x ∈ A
intro x hx
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t + replicate (n - m) a
⊢ x ∈ A
rw [mem_add] at hx
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t
⊢ x ∈ A

case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
cases' hx with hx hx
no goals
case inl
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t
⊢ x ∈ A
exact htA x hx
no goals
case inr
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
rwa [eq_of_mem_replicate hx]
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (s + replicate (n - m) a) = n
rw [_root_.map_add, card_replicate, hs]
no goals
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
simp [h]
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (t + replicate (n - m) a) = n
rw [_root_.map_add, card_replicate, ht]
no goals
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
simp [h]
no goals
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.82361
δ : Type ?u.82364
G : Type ?u.82367
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (s + replicate (n - m) a) = prod (t + replicate (n - m) a)
rw [prod_add, prod_add, hst]