no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
⊢ ∀ (x : α), ↑f x ≠ x ↔ ↑f (↑f x) ≠ ↑f x
simp
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
⊢ ∀ (x : β), ↑g x ≠ x ↔ ↑g (↑g x) ≠ ↑g x
simp
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ ↑g (i ↑x (_ : ↑f ↑x ≠ ↑x)) ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
⊢ ↑g (i ↑x (_ : ↑f ↑x ≠ ↑x)) ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ i (↑f ↑x) this ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ ↑g (i ↑x (_ : ↑f ↑x ≠ ↑x)) ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
rw [← h _ x.2 this]
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ i (↑f ↑x) this ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
exact mt (hi _ _ this x.2) x.2