α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ (∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b) ↔ Disjoint m1 m2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ _root_.Disjoint (toFinset m1) (toFinset m2) ↔ Disjoint m1 m2
rw [Finset.disjoint_iff_ne]
case refine'_1
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1 : a ∈ m1
ha2 : a ∈ m2
⊢ False

case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1 m2 → ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ (∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b) ↔ Disjoint m1 m2
refine' ⟨fun h a ha1 ha2 => _, _⟩
case refine'_1
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1✝ : a ∈ m1
ha1 : a ∈ toFinset m1
ha2✝ : a ∈ m2
ha2 : a ∈ toFinset m2
⊢ False
case refine'_1
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1 : a ∈ m1
ha2 : a ∈ m2
⊢ False
rw [← Multiset.mem_toFinset] at ha1 ha2
no goals
case refine'_1
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1✝ : a ∈ m1
ha1 : a ∈ toFinset m1
ha2✝ : a ∈ m2
ha2 : a ∈ toFinset m2
⊢ False
exact h _ ha1 _ ha2 rfl
case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ toFinset m1
hb : a ∈ toFinset m2
⊢ False
case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1 m2 → ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
rintro h a ha b hb rfl
case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ m1
hb : a ∈ m2
⊢ False
case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ toFinset m1
hb : a ∈ toFinset m2
⊢ False
rw [Multiset.mem_toFinset] at ha hb
no goals
case refine'_2
α : Type u_1
β : Type ?u.559305
γ : Type ?u.559308
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ m1
hb : a ∈ m2
⊢ False
exact h ha hb