[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) → ∃ u, q u
[PROOFSTEP]
rintro ⟨u, h₂⟩
[GOAL]
case mpr
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, q u) → ∃ u, P u
[PROOFSTEP]
rintro ⟨u, h₂⟩
[GOAL]
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u
[PROOFSTEP]
refine ⟨f <$$> u, ?_⟩
[GOAL]
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)
[PROOFSTEP]
apply (h₁ u).mp h₂
[GOAL]
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
[PROOFSTEP]
refine ⟨g <$$> u, ?_⟩
[GOAL]
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ P (g <$$> u)
[PROOFSTEP]
apply (h₁ _).mpr _
[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ q (f <$$> g <$$> u)
[PROOFSTEP]
simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]
[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x : F α
⊢ ∀ (u : F fun i => Subtype ((fun i x => ofRepeat (P i x)) i)),
    (fun i => Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x
[PROOFSTEP]
simp [MvFunctor.map_map]
[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.fst p.snd }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (prod.fst ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = x ∧ (prod.snd ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = y
[PROOFSTEP]
simp only [map_map, comp_assoc, subtypeVal_toSubtype']
[GOAL]
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.fst p.snd }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (prod.fst ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = x ∧
        (prod.snd ⊚ fun i x => prod.mk i (↑x).fst (↑x).snd) <$$> u = y
[PROOFSTEP]
simp [comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (PredLast' α pp i p_1) }) (Fin2.fs i)
⊢ ofRepeat (PredLast' α pp (Fin2.fs i) ↑x) = PredLast α pp ↑x
[PROOFSTEP]
simp only [PredLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (PredLast' α pp i p_1) }) (Fin2.fs i)
⊢ ofRepeat (PredLast' α pp (Fin2.fs i) ↑x) = True
[PROOFSTEP]
erw [const_iff_true]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // PredLast α pp p_1 }) (Fin2.fs i)
⊢ PredLast α pp ↑x = ofRepeat (PredLast' α pp (Fin2.fs i) ↑x)
[PROOFSTEP]
simp only [PredLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // PredLast α pp p_1 }) (Fin2.fs i)
⊢ True = ofRepeat (PredLast' α pp (Fin2.fs i) ↑x)
[PROOFSTEP]
erw [const_iff_true]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (PredLast' α P) x ↔ LiftP (PredLast α P) x
[PROOFSTEP]
dsimp only [LiftP, LiftP']
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ (∃ u, (fun i => Subtype.val) <$$> u = x) ↔ ∃ u, (fun i => Subtype.val) <$$> u = x
[PROOFSTEP]
apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ MvFunctor.f P n α ⊚ MvFunctor.g P n α = TypeVec.id
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₀.a.h.mk.a
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) i { val := x, property := property✝ }) =
    ↑(TypeVec.id i { val := x, property := property✝ })
[PROOFSTEP]
cases i
[GOAL]
case h₀.a.h.mk.a.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) Fin2.fz { val := x, property := property✝ }) =
    ↑(TypeVec.id Fin2.fz { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₀.a.h.mk.a.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝)
property✝ : PredLast α P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) (Fin2.fs a✝) { val := x, property := property✝ }) =
    ↑(TypeVec.id (Fin2.fs a✝) { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }),
    (fun i => Subtype.val) <$$> u = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u = x
[PROOFSTEP]
intros
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u✝ = x
[PROOFSTEP]
rw [MvFunctor.map_map]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ ((fun i => Subtype.val) ⊚ MvFunctor.f P n α) <$$> u✝ = x
[PROOFSTEP]
dsimp [(· ⊚ ·)]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x
[PROOFSTEP]
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
this : (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x
[PROOFSTEP]
rw [this]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
⊢ (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.h.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (PredLast' α P i x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α i { val := x, property := property✝ })
[PROOFSTEP]
cases i
[GOAL]
case h₁.h.h.mk.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (PredLast' α P Fin2.fz x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α Fin2.fz { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.h.mk.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β✝ : Type u
pp : β✝ → Prop
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (PredLast' α P i p_1) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (PredLast' α P (Fin2.fs a✝) x)
⊢ ↑{ val := x, property := property✝ } = ↑(MvFunctor.f P n α (Fin2.fs a✝) { val := x, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }) (Fin2.fs i)
⊢ ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd)) = RelLast α rr (↑x).fst (↑x).snd
[PROOFSTEP]
simp only [RelLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }) (Fin2.fs i)
⊢ ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd)) = ((↑x).fst = (↑x).snd)
[PROOFSTEP]
erw [repeatEq_iff_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // RelLast α rr p_1.fst p_1.snd }) (Fin2.fs i)
⊢ RelLast α rr (↑x).fst (↑x).snd = ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd))
[PROOFSTEP]
simp only [RelLast]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec x✝
i : Fin2 x✝
x : (fun i => { p_1 // RelLast α rr p_1.fst p_1.snd }) (Fin2.fs i)
⊢ ((↑x).fst = (↑x).snd) = ofRepeat (RelLast' α rr (Fin2.fs i) (prod.mk (Fin2.fs i) (↑x).fst (↑x).snd))
[PROOFSTEP]
erw [repeatEq_iff_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ LiftR' (RelLast' α rr) x y ↔ LiftR (fun {i} => RelLast α rr) x y
[PROOFSTEP]
dsimp only [LiftR, LiftR']
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ (∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y) ↔
    ∃ u, (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y
[PROOFSTEP]
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
[GOAL]
case h₀
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id
[PROOFSTEP]
ext i ⟨x, _⟩ : 2
[GOAL]
case h₀.a.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) i { val := x, property := property✝ } =
    TypeVec.id i { val := x, property := property✝ }
[PROOFSTEP]
cases i
[GOAL]
case h₀.a.h.mk.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) Fin2.fz { val := x, property := property✝ } =
    TypeVec.id Fin2.fz { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
case h₀.a.h.mk.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : RelLast α rr x.fst x.snd
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) (Fin2.fs a✝) { val := x, property := property✝ } =
    TypeVec.id (Fin2.fs a✝) { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }),
    (fun i t => (↑t).fst) <$$> u = x ∧ (fun i t => (↑t).snd) <$$> u = y ↔
      (fun i t => (↑t).fst) <$$> MvFunctor.f' rr n α <$$> u = x ∧
        (fun i t => (↑t).snd) <$$> MvFunctor.f' rr n α <$$> u = y
[PROOFSTEP]
intros
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i t => (↑t).fst) <$$> MvFunctor.f' rr n α <$$> u✝ = x ∧
      (fun i t => (↑t).snd) <$$> MvFunctor.f' rr n α <$$> u✝ = y
[PROOFSTEP]
simp [MvFunctor.map_map, (· ⊚ ·)]
  -- porting note: proof was
      -- rw [MvFunctor.map_map, MvFunctor.map_map, (· ⊚ ·), (· ⊚ ·)]
      -- congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
[PROOFSTEP]
suffices
  (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst)) ∧
    (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd))
  by
  rcases this with ⟨left, right⟩
  rw [left, right];
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
this :
  ((fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst) ∧
    (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
[PROOFSTEP]
rcases this with ⟨left, right⟩
[GOAL]
case intro
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
left : (fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst
right : (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
⊢ (fun i t => (↑t).fst) <$$> u✝ = x ∧ (fun i t => (↑t).snd) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).fst) <$$> u✝ = x ∧
      (fun i x => (↑(MvFunctor.f' rr n α i x)).snd) <$$> u✝ = y
[PROOFSTEP]
rw [left, right]
[GOAL]
case h₁
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ ((fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst) ∧
    (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
[PROOFSTEP]
constructor
[GOAL]
case h₁.left
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).fst) = fun i x => (↑(MvFunctor.f' rr n α i x)).fst
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.right
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
⊢ (fun i t => (↑t).snd) = fun i x => (↑(MvFunctor.f' rr n α i x)).snd
[PROOFSTEP]
ext i ⟨x, _⟩
[GOAL]
case h₁.left.h.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (RelLast' α rr i (prod.mk i x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst = (↑(MvFunctor.f' rr n α i { val := x, property := property✝ })).fst
[PROOFSTEP]
cases i
[GOAL]
case h₁.right.h.h.mk
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (RelLast' α rr i (prod.mk i x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd = (↑(MvFunctor.f' rr n α i { val := x, property := property✝ })).snd
[PROOFSTEP]
cases i
[GOAL]
case h₁.left.h.h.mk.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (RelLast' α rr Fin2.fz (prod.mk Fin2.fz x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst = (↑(MvFunctor.f' rr n α Fin2.fz { val := x, property := property✝ })).fst
[PROOFSTEP]
rfl
[GOAL]
case h₁.left.h.h.mk.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (RelLast' α rr (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).fst =
    (↑(MvFunctor.f' rr n α (Fin2.fs a✝) { val := x, property := property✝ })).fst
[PROOFSTEP]
rfl
[GOAL]
case h₁.right.h.h.mk.fz
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (RelLast' α rr Fin2.fz (prod.mk Fin2.fz x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd = (↑(MvFunctor.f' rr n α Fin2.fz { val := x, property := property✝ })).snd
[PROOFSTEP]
rfl
[GOAL]
case h₁.right.h.h.mk.fs
n : ℕ
F : TypeVec (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (RelLast' α rr i (prod.mk i p_1.fst p_1.snd)) }
a✝ : Fin2 (Nat.add n 0)
x : (α ::: β) (Fin2.fs a✝) × (α ::: β) (Fin2.fs a✝)
property✝ : ofRepeat (RelLast' α rr (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd))
⊢ (↑{ val := x, property := property✝ }).snd =
    (↑(MvFunctor.f' rr n α (Fin2.fs a✝) { val := x, property := property✝ })).snd
[PROOFSTEP]
rfl


[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α : Type u} (x : WriterT ω M α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [Functor.map, WriterT.mk]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β : Type u} (x : α) (f : α → WriterT ω M β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → WriterT ω M β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp [Bind.bind, Pure.pure, WriterT.mk]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β γ : Type u} (x : WriterT ω M α) (f : α → WriterT ω M β) (g : β → WriterT ω M γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝ : WriterT ω M α✝
f✝ : α✝ → WriterT ω M β✝
g✝ : β✝ → WriterT ω M γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β : Type u} (f : α → β) (x : WriterT ω M α),
    (do
        let y ← x
        pure (f y)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
      let y ← x✝
      pure (f✝ y)) =
    f✝ <$> x✝
[PROOFSTEP]
simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp]


[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
x : Option α
⊢ Option.traverse pure x = x
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
⊢ Option.traverse pure none = none
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
val✝ : α
⊢ Option.traverse pure (some val✝) = some val✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) none =
    Comp.mk (Option.traverse f <$> Option.traverse g none)
[PROOFSTEP]
simp! [functor_norm]
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))
[PROOFSTEP]
simp! [functor_norm]
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Comp.mk (((fun x => some <$> x) ∘ f) <$> g val✝) = Comp.mk ((Option.traverse f ∘ some) <$> g val✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
⊢ Option.traverse (pure ∘ f) none = pure (f <$> none)
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
val✝ : α
⊢ Option.traverse (pure ∘ f) (some val✝) = pure (f <$> some val✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f x) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
cases' x with x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f none) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) none
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f (some x)) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (some x)
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
xs : List α
⊢ List.traverse pure xs = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
⊢ List.traverse pure [] = []
[PROOFSTEP]
simp! [*, List.traverse, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ List.traverse pure (head✝ :: tail✝) = head✝ :: tail✝
[PROOFSTEP]
simp! [*, List.traverse, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ (Seq.seq (cons head✝) fun x => tail✝) = head✝ :: tail✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (head✝ :: tail✝) =
    Comp.mk (List.traverse f <$> List.traverse g (head✝ :: tail✝))
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))
[PROOFSTEP]
rfl
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk
      (Seq.seq
        (((fun x => x ∘ List.traverse f) ∘ (fun x x_1 => Seq.seq x fun x => x_1) ∘ (fun x => cons <$> x) ∘ f) <$>
          g head✝)
        fun x => List.traverse g tail✝) =
    Comp.mk (Seq.seq (((fun x => List.traverse f ∘ x) ∘ cons) <$> g head✝) fun x => List.traverse g tail✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
x : List α
⊢ List.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
⊢ List.traverse (pure ∘ f) [] = pure (f <$> [])
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ List.traverse (pure ∘ f) (head✝ :: tail✝) = pure (f <$> (head✝ :: tail✝))
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ (Seq.seq (cons (f head✝)) fun x => map f tail✝) = f head✝ :: map f tail✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f x) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f []) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) []
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ :
  (fun {α} => ApplicativeTransformation.app η α) (List.traverse f tail✝) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) tail✝
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f (head✝ :: tail✝)) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (head✝ :: tail✝)
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f []) fun x => traverse f bs
[PROOFSTEP]
simp [functor_norm]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f (a :: as)) fun x => traverse f bs
[PROOFSTEP]
simp [traverse_append as bs, functor_norm]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (Seq.seq
      (Seq.seq (((fun x => x ∘ fun x x_1 => x ++ x_1) ∘ Function.comp ∘ fun x x_1 => x :: x_1) <$> f a) fun x =>
        traverse f as)
      fun x => traverse f bs) =
    Seq.seq (Seq.seq (((fun x => (fun x x_1 => x ++ x_1) ∘ x) ∘ fun x x_1 => x :: x_1) <$> f a) fun x => traverse f as)
      fun x => traverse f bs
[PROOFSTEP]
congr
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) [] []
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) [] (a :: as)
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) []
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) (a :: as)
[PROOFSTEP]
simp [mem_traverse as bs]
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ Sum.traverse f (g <$> inl val✝) = Sum.traverse (f ∘ g) (inl val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ Sum.traverse f (g <$> inr val✝) = Sum.traverse (f ∘ g) (inr val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ (match g <$> inl val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    pure (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ (match g <$> inr val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    inr <$> f (g val✝)
[PROOFSTEP]
rfl
[GOAL]
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
val✝ : σ
⊢ Sum.traverse pure (inl val✝) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
val✝ : α
⊢ Sum.traverse pure (inr val✝) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (inl val✝) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val✝))
[PROOFSTEP]
simp! [Sum.traverse, map_id, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (inr val✝) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))
[PROOFSTEP]
simp! [Sum.traverse, map_id, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ pure (inl val✝) = Comp.mk (pure (pure (inl val✝)))
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Comp.mk (((fun x => inr <$> x) ∘ f) <$> g val✝) = Comp.mk ((Sum.traverse f ∘ inr) <$> g val✝)
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
induction x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : σ
⊢ inl val✝ = f <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : α
⊢ inr (f val✝) = f <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g x = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g (inl val✝) = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) (inl val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g (inr val✝) = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) (inr val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ pure (f <$> inl val✝) = pure (inl val✝)
[PROOFSTEP]
congr
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ ((fun x => f <$> x) ∘ inr) <$> g val✝ = (inr ∘ f) <$> g val✝
[PROOFSTEP]
congr
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f x) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f (inl val✝)) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (inl val✝)
[PROOFSTEP]
simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f (inr val✝)) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (inr val✝)
[PROOFSTEP]
simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]


[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x
[PROOFSTEP]
rw [IsPeriodicPt, iterate_add]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x
[PROOFSTEP]
exact hn.comp hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
rw [IsPeriodicPt, iterate_add] at hn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
exact hn.left_of_comp hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
rw [add_comm] at hn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
exact hn.left_of_add hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
cases' le_total n m with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
refine' left_of_add _ hn
[GOAL]
case inl
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x
[PROOFSTEP]
rwa [tsub_add_cancel_of_le h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x
[PROOFSTEP]
apply isPeriodicPt_zero
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x
[PROOFSTEP]
simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x
[PROOFSTEP]
simp only [mul_comm n, hm.mul_const n]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x
[PROOFSTEP]
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x
[PROOFSTEP]
exact hf.isFixedPt.iterate m
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x
[PROOFSTEP]
rw [IsPeriodicPt, hco.comp_iterate]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
[PROOFSTEP]
exact IsFixedPt.comp hf hg
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
rw [IsPeriodicPt, hco.comp_iterate] at hfg
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
exact hfg.left_of_comp hg
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x
[PROOFSTEP]
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
revert hm hn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
refine' Nat.gcd.induction m n (fun n _ hn => _) fun m n _ ih hm hn => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x
[PROOFSTEP]
rwa [Nat.gcd_zero_left]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
rw [Nat.gcd_rec]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd (n % m) m) x
[PROOFSTEP]
exact ih (hn.mod hm) hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
⊢ x = y
[PROOFSTEP]
rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[Nat.pred n] x) = x
[PROOFSTEP]
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
⊢ IsPeriodicPt f m x
[PROOFSTEP]
rcases hx with ⟨r, hr, hr'⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
suffices n ≤ (n / r + 1) * r by
  -- porting note: convert used to unfold IsPeriodicPt
  change _ = _
  convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
    rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x
[PROOFSTEP]
change _ = _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x
[PROOFSTEP]
convert (hm.apply_iterate ((n / r + 1) * r - n)).eq
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
[PROOFSTEP]
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
[PROOFSTEP]
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
[PROOFSTEP]
exact (Nat.lt_div_mul_add hr).le
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
x : α
⊢ x ∈ ⋃ (n : ℕ) (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f
[PROOFSTEP]
simp [mem_periodicPts]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x
[PROOFSTEP]
delta minimalPeriod
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x
[PROOFSTEP]
exact (Nat.find_spec hx).2
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ IsPeriodicPt f 0 x
[PROOFSTEP]
exact isPeriodicPt_zero f x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x
[PROOFSTEP]
rw [iterate_add_apply]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[minimalPeriod f x] x = x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod f x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x
[PROOFSTEP]
simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : ¬x ∈ periodicPts f
⊢ minimalPeriod f x = 0
[PROOFSTEP]
simp only [minimalPeriod, dif_neg hx]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : ¬x ∈ periodicPts f
⊢ ¬0 < minimalPeriod f x
[PROOFSTEP]
simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n
[PROOFSTEP]
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (_ : x ∈ periodicPts f) ≤ n
[PROOFSTEP]
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x
[PROOFSTEP]
apply
  (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
    ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
      (minimalPeriod_pos_of_mem_periodicPts _))
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
[PROOFSTEP]
rcases hx with ⟨m, hm, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f
[PROOFSTEP]
exact ⟨m, hm, hx.apply_iterate n⟩
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m ≤ n
[PROOFSTEP]
by_contra' hmn'
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False
[PROOFSTEP]
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False
[PROOFSTEP]
exact
  ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
            (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
              (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
        (Nat.sub_le m n)).not_lt
    hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f x
[PROOFSTEP]
rw [← iterate_one f]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x
[PROOFSTEP]
refine' Function.IsPeriodicPt.isFixedPt _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x
[PROOFSTEP]
rw [← h]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod f x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
[PROOFSTEP]
exact
  ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y✝ : α
m n : ℕ
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y
[PROOFSTEP]
simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x = p ^ (k + 1)
[PROOFSTEP]
apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out
[GOAL]
case h₁
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬minimalPeriod f x ∣ p ^ k
[PROOFSTEP]
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)
[PROOFSTEP]
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ lcm (minimalPeriod f x) (minimalPeriod g x)
[PROOFSTEP]
rw [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) (lcm (minimalPeriod f x) (minimalPeriod g x)) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
[PROOFSTEP]
apply h.minimalPeriod_of_comp_dvd_mul.antisymm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
suffices :
  ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
this :
  ∀ {f g : α → α},
    Function.Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
exact hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
[GOAL]
case this
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
intro f g h hco
[GOAL]
case this
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
refine' hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h _ _).minimalPeriod_dvd
[GOAL]
case this.refine'_1
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod _ _).const_mul _
[GOAL]
case this.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod _ _).mul_const _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f^[n] x = minimalPeriod f x / gcd (minimalPeriod f x) n
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / gcd (minimalPeriod f x) n
[PROOFSTEP]
apply IsPeriodicPt.minimalPeriod_dvd
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt f^[n] (minimalPeriod f x / gcd (minimalPeriod f x) n) x
[PROOFSTEP]
rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _), mul_comm,
  Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ f^[n / gcd (minimalPeriod f x) n]^[minimalPeriod f x] x = x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).iterate _
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod f^[n] x
[PROOFSTEP]
apply coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod f^[n] x * (n / gcd (minimalPeriod f x) n)
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_right h
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n * gcd (minimalPeriod f x) n ∣
    minimalPeriod f^[n] x * (n / gcd (minimalPeriod f x) n) * gcd (minimalPeriod f x) n
[PROOFSTEP]
rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _), mul_comm]
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x
[PROOFSTEP]
apply IsPeriodicPt.minimalPeriod_dvd
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x
[PROOFSTEP]
rw [IsPeriodicPt, IsFixedPt, iterate_mul]
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod _ _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.length (periodicOrbit f x) = minimalPeriod f x
[PROOFSTEP]
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ periodicOrbit f x = Cycle.nil ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
simp [periodicOrbit]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
exact minimalPeriod_eq_zero_iff_nmem_periodicPts
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y
[PROOFSTEP]
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ a, a < minimalPeriod f x ∧ f^[a] x = y) ↔ ∃ n, f^[n] x = y
[PROOFSTEP]
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ n, f^[n] x = y) → ∃ a, a < minimalPeriod f x ∧ f^[a] x = y
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a, a < minimalPeriod f x ∧ f^[a] x = f^[n] x
[PROOFSTEP]
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
[GOAL]
case right
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x
[PROOFSTEP]
rw [iterate_mod_minimalPeriod_eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.Nodup (periodicOrbit f x)
[PROOFSTEP]
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on (List.nodup_range _)]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ List.range (minimalPeriod f x) → ∀ (y : ℕ), y ∈ List.range (minimalPeriod f x) → f^[x_1] x = f^[y] x → x_1 = y
[PROOFSTEP]
intro m hm n hn hmn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n
[PROOFSTEP]
rw [List.mem_range] at hm hn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n
[PROOFSTEP]
rwa [eq_iff_lt_minimalPeriod_of_iterate_eq hm hn] at hmn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n =
    List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))
[PROOFSTEP]
apply List.ext_nthLe _ fun m _ _ => _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.length (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n) =
    List.length (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))
[PROOFSTEP]
simp [minimalPeriod_apply_iterate hx]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∀ (m : ℕ) (x_1 : m < List.length (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n))
    (x_2 : m < List.length (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))),
    List.nthLe (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n) m x_1 =
      List.nthLe (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))) m x_2
[PROOFSTEP]
simp [List.nthLe_rotate, iterate_add_apply]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
by_cases hx : x ∈ periodicPts f
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
have hx' := minimalPeriod_pos_of_mem_periodicPts hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)) ↔
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
refine' ⟨_, fun H => ⟨_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)) →
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rintro ⟨hr, H⟩ n hn
[GOAL]
case pos.refine'_1.intro
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
cases' eq_or_lt_of_le (lt_succ_iff.1 hn) with hM' hM'
[GOAL]
case pos.refine'_1.intro.inl
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rwa [hM', hM, iterate_minimalPeriod]
[GOAL]
case pos.refine'_1.intro.inr
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
exact H _ hM'
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
[PROOFSTEP]
rw [iterate_zero_apply]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x
[PROOFSTEP]
nth_rw 3 [← @iterate_minimalPeriod α f x]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
[PROOFSTEP]
nth_rw 2 [← hM]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)
[PROOFSTEP]
exact H _ (Nat.lt_succ_self _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_nmem_periodicPts hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ (n : ℕ), n < 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit_chain r]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
refine' ⟨fun H n => _, fun H n _ => H n⟩
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n), ← iterate_succ_apply,
  minimalPeriod_apply hx]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[succ (n % minimalPeriod f x)] x)
[PROOFSTEP]
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))
[GOAL]
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n✝ : ℕ
f : α → α
g : β → β
n : ℕ
⊢ (Prod.map f g)^[n] = Prod.map f^[n] g^[n]
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
⊢ (Prod.map f g)^[Nat.zero] = Prod.map f^[Nat.zero] g^[Nat.zero]
[PROOFSTEP]
simp [*, Prod.map_comp_map]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
n✝ : ℕ
n_ih✝ : (Prod.map f g)^[n✝] = Prod.map f^[n✝] g^[n✝]
⊢ (Prod.map f g)^[Nat.succ n✝] = Prod.map f^[Nat.succ n✝] g^[Nat.succ n✝]
[PROOFSTEP]
simp [*, Prod.map_comp_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x✝ : α × β
a : α
b : β
m n : ℕ
x : α × β
⊢ IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.fst ∧ IsPeriodicPt g n x.snd
[PROOFSTEP]
simp [IsPeriodicPt]
[GOAL]
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x✝ : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
x : α × β
⊢ ∀ (c : ℕ), minimalPeriod (Prod.map f g) x ∣ c ↔ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd) ∣ c
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
fst✝ : α
snd✝ : β
⊢ ∀ (c : ℕ),
    minimalPeriod (Prod.map f g) (fst✝, snd✝) ∣ c ↔
      Nat.lcm (minimalPeriod f (fst✝, snd✝).fst) (minimalPeriod g (fst✝, snd✝).snd) ∣ c
[PROOFSTEP]
simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod f x.fst ∣ minimalPeriod (Prod.map f g) x
[PROOFSTEP]
rw [minimalPeriod_prod_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod f x.fst ∣ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd)
[PROOFSTEP]
exact Nat.dvd_lcm_left _ _
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod g x.snd ∣ minimalPeriod (Prod.map f g) x
[PROOFSTEP]
rw [minimalPeriod_prod_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod g x.snd ∣ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd)
[PROOFSTEP]
exact Nat.dvd_lcm_right _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod ((fun x x_1 => x • x_1) a) b ∣ n
[PROOFSTEP]
rw [← isPeriodicPt_iff_minimalPeriod_dvd, IsPeriodicPt, IsFixedPt, smul_iterate]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.ofNat a✝
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat, Int.coe_nat_dvd, pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.negSucc a✝
[PROOFSTEP]
rw [Int.negSucc_coe, zpow_neg, zpow_ofNat, inv_smul_eq_iff, eq_comm, dvd_neg, Int.coe_nat_dvd,
  pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
⊢ a ^ (n % minimalPeriod ((fun x x_1 => x • x_1) a) b) • b = a ^ n • b
[PROOFSTEP]
conv_rhs =>
  rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
  pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
⊢ a ^ (n % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) • b = a ^ n • b
[PROOFSTEP]
conv_rhs =>
  rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
  zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]


[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, ¬g x ∈ U
[PROOFSTEP]
refine fun U hU ↦ h.ae_mem_or_ae_nmem₀ (s := g ⁻¹' U) (hgm hU) ?_b
[GOAL]
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' (g ⁻¹' U) =ᵐ[μ] g ⁻¹' U
[PROOFSTEP]
refine (hg_eq.mono fun x hx ↦ ?_).set_eq
[GOAL]
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ f ⁻¹' (g ⁻¹' U) ↔ x ∈ g ⁻¹' U
[PROOFSTEP]
rw [← preimage_comp, mem_preimage, mem_preimage, hx]
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : HasCountableSeparatingOn X MeasurableSet univ
f : α → α
g : α → X
h : PreErgodic f
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' (g ⁻¹' U) = g ⁻¹' U
[PROOFSTEP]
rw [← preimage_comp, hg_eq]
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
borelize X
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩
[GOAL]
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
haveI := ht.secondCountableTopology
[GOAL]
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology ↑t
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq