no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ : α × β
a' : α
b : β
hab : ↑(prodExtendRight a σ) (a', b) ≠ (a', b)
x✝ : ↑(prodExtendRight a σ) (↑(prodExtendRight a σ) (a', b)) ≠ ↑(prodExtendRight a σ) (a', b)
⊢ (fun ab x => ab.snd) (↑(prodExtendRight a σ) (a', b)) x✝ = ↑σ ((fun ab x => ab.snd) (a', b) hab)
simp [eq_of_prodExtendRight_ne hab]
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : ↑(prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : ↑(prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (fun ab x => ab.snd) (a₁, b₁) hab₁ = (fun ab x => ab.snd) (a₂, b₂) hab₂
⊢ (a₁, b₁) = (a₂, b₂)
simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : ↑σ y ≠ y
⊢ ↑(prodExtendRight a σ) (a, y) ≠ (a, y)
simpa
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : ↑σ y ≠ y
⊢ (fun ab x => ab.snd) (a, y) (_ : ↑(prodExtendRight a σ) (a, y) ≠ (a, y)) = y
simp