ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (_root_.Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Set.PairwiseDisjoint ↑s fun i => map (Embedding.sigmaMk i) (t i)
intro i _ j _ hij
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → ¬a ∈ map (Embedding.sigmaMk j) (t j)
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (_root_.Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j
rw [Function.onFun, disjoint_left]
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄,
    (∃ a_1, a_1 ∈ t i ∧ { fst := i, snd := a_1 } = a) → ¬∃ a_2, a_2 ∈ t j ∧ { fst := j, snd := a_2 } = a
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → ¬a ∈ map (Embedding.sigmaMk j) (t j)
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : { fst := j, snd := z } = { fst := i, snd := y }
⊢ False
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄,
    (∃ a_1, a_1 ∈ t i ∧ { fst := i, snd := a_1 } = a) → ¬∃ a_2, a_2 ∈ t j ∧ { fst := j, snd := a_2 } = a
rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩
no goals
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
β : Type ?u.7974
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : { fst := j, snd := z } = { fst := i, snd := y }
⊢ False
exact hij (congr_arg Sigma.fst hz'.symm)