Imports
module
public import Mathlib.Algebra.GroupWithZero.Nat
public import Mathlib.Algebra.Order.Group.Nat
public import Mathlib.Data.Fin.SuccPred
List lemmas
@[ expose ] public section lemma insertIdx_map { I J : Type } ( f : I → J ) : ( i : ℕ ) → ( r : List I ) → ( r0 : I ) →
( List.insertIdx r i r0 ) . map f = List.insertIdx ( r . map f ) i ( f r0 )
| 0 , [ ] , r0 => I : Type J : Type f : I → J r0 : I ⊢ List.map f ( [ ] . insertIdx 0 r0 ) = ( List.map f [ ] ) . insertIdx 0 ( f r0 ) by I : Type J : Type f : I → J r0 : I ⊢ List.map f ( [ ] . insertIdx 0 r0 ) = ( List.map f [ ] ) . insertIdx 0 ( f r0 ) simp All goals completed! 🐙
| n + 1 , [ ] , r0 => I : Type J : Type f : I → J n : ℕ r0 : I ⊢ List.map f ( [ ] . insertIdx ( n + 1 ) r0 ) = ( List.map f [ ] ) . insertIdx ( n + 1 ) ( f r0 ) by I : Type J : Type f : I → J n : ℕ r0 : I ⊢ List.map f ( [ ] . insertIdx ( n + 1 ) r0 ) = ( List.map f [ ] ) . insertIdx ( n + 1 ) ( f r0 ) simp All goals completed! 🐙
| 0 , a :: as , r0 => I : Type J : Type f : I → J a : I as : List I r0 : I ⊢ List.map f ( ( a :: as ) . insertIdx 0 r0 ) = ( List.map f ( a :: as ) ) . insertIdx 0 ( f r0 ) by I : Type J : Type f : I → J a : I as : List I r0 : I ⊢ List.map f ( ( a :: as ) . insertIdx 0 r0 ) = ( List.map f ( a :: as ) ) . insertIdx 0 ( f r0 ) simp All goals completed! 🐙
| n + 1 , a :: as , r0 => I : Type J : Type f : I → J n : ℕ a : I as : List I r0 : I ⊢ List.map f ( ( a :: as ) . insertIdx ( n + 1 ) r0 ) = ( List.map f ( a :: as ) ) . insertIdx ( n + 1 ) ( f r0 ) by I : Type J : Type f : I → J n : ℕ a : I as : List I r0 : I ⊢ List.map f ( ( a :: as ) . insertIdx ( n + 1 ) r0 ) = ( List.map f ( a :: as ) ) . insertIdx ( n + 1 ) ( f r0 )
simp only [ List.insertIdx_succ_cons , List.map_cons , List.cons.injEq , true_and ] I : Type J : Type f : I → J n : ℕ a : I as : List I r0 : I ⊢ List.map f ( as . insertIdx n r0 ) = ( List.map f as ) . insertIdx n ( f r0 )
exact insertIdx_map f n as r0 All goals completed! 🐙 lemma eraseIdx_sorted { I : Type } ( le : I → I → Prop ) :
( r : List I ) → ( n : ℕ ) →
List.Pairwise le r → List.Pairwise le ( r . eraseIdx n )
| [ ] , _ , _ => I : Type le : I → I → Prop x✝¹ : ℕ x✝ : List.Pairwise le [ ] ⊢ List.Pairwise le ( [ ] . eraseIdx x✝¹ ) by I : Type le : I → I → Prop x✝¹ : ℕ x✝ : List.Pairwise le [ ] ⊢ List.Pairwise le ( [ ] . eraseIdx x✝¹ ) simp All goals completed! 🐙
| a :: as , 0 , h => I : Type le : I → I → Prop a : I as : List I h : List.Pairwise le ( a :: as ) ⊢ List.Pairwise le ( ( a :: as ) . eraseIdx 0 ) by I : Type le : I → I → Prop a : I as : List I h : List.Pairwise le ( a :: as ) ⊢ List.Pairwise le ( ( a :: as ) . eraseIdx 0 )
simp only [ List.eraseIdx ] I : Type le : I → I → Prop a : I as : List I h : List.Pairwise le ( a :: as ) ⊢ List.Pairwise le as
simp only [ List.pairwise_cons ] at h I : Type le : I → I → Prop a : I as : List I h : (∀ ( a' : I ), a' ∈ as → le a a' ) ∧ List.Pairwise le as ⊢ List.Pairwise le as
exact h . 2 All goals completed! 🐙
| a :: as , n + 1 , h => I : Type le : I → I → Prop a : I as : List I n : ℕ h : List.Pairwise le ( a :: as ) ⊢ List.Pairwise le ( ( a :: as ) . eraseIdx ( n + 1 ) ) by I : Type le : I → I → Prop a : I as : List I n : ℕ h : List.Pairwise le ( a :: as ) ⊢ List.Pairwise le ( ( a :: as ) . eraseIdx ( n + 1 ) )
simp only [ List.eraseIdx_cons_succ , List.pairwise_cons ] I : Type le : I → I → Prop a : I as : List I n : ℕ h : List.Pairwise le ( a :: as ) ⊢ (∀ ( a' : I ), a' ∈ as . eraseIdx n → le a a' ) ∧ List.Pairwise le ( as . eraseIdx n )
simp only [ List.pairwise_cons ] at h I : Type le : I → I → Prop a : I as : List I n : ℕ h : (∀ ( a' : I ), a' ∈ as → le a a' ) ∧ List.Pairwise le as ⊢ (∀ ( a' : I ), a' ∈ as . eraseIdx n → le a a' ) ∧ List.Pairwise le ( as . eraseIdx n )
refine And.intro ? _ ( eraseIdx_sorted le as n h . 2 ) I : Type le : I → I → Prop a : I as : List I n : ℕ h : (∀ ( a' : I ), a' ∈ as → le a a' ) ∧ List.Pairwise le as ⊢ ∀ ( a' : I ), a' ∈ as . eraseIdx n → le a a'
intro b hb I : Type le : I → I → Prop a : I as : List I n : ℕ h : (∀ ( a' : I ), a' ∈ as → le a a' ) ∧ List.Pairwise le as b : I hb : b ∈ as . eraseIdx n ⊢ le a b
refine h . 1 _ ? _ I : Type le : I → I → Prop a : I as : List I n : ℕ h : (∀ ( a' : I ), a' ∈ as → le a a' ) ∧ List.Pairwise le as b : I hb : b ∈ as . eraseIdx n ⊢ b ∈ as
exact List.mem_of_mem_eraseIdx hb All goals completed! 🐙
lemma mem_eraseIdx_nodup { I : Type } ( i : I ) :
( l : List I ) → ( n : ℕ ) → ( hn : n < l . length ) → ( h : List.Nodup l ) →
i ∈ l . eraseIdx n ↔ i ∈ l ∧ i ≠ l [ n ]
| [ ] , _ , _ , _ => I : Type i : I x✝² : ℕ x✝¹ : x✝² < [ ] . length x✝ : [ ] . Nodup ⊢ i ∈ [ ] . eraseIdx x✝² ↔ i ∈ [ ] ∧ i ≠ [ ] [ x✝² ] by I : Type i : I x✝² : ℕ x✝¹ : x✝² < [ ] . length x✝ : [ ] . Nodup ⊢ i ∈ [ ] . eraseIdx x✝² ↔ i ∈ [ ] ∧ i ≠ [ ] [ x✝² ] simp All goals completed! 🐙
| a1 :: as , 0 , _ , h => I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i ∈ ( a1 :: as ) . eraseIdx 0 ↔ i ∈ a1 :: as ∧ i ≠ ( a1 :: as ) [ 0 ] by I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i ∈ ( a1 :: as ) . eraseIdx 0 ↔ i ∈ a1 :: as ∧ i ≠ ( a1 :: as ) [ 0 ]
simp only [ List.eraseIdx_zero , List.tail_cons , List.mem_cons , List.getElem_cons_zero , ne_eq ] I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i ∈ as ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = a1
by_cases hi : i = a1 pos I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup hi : i = a1 ⊢ i ∈ as ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = a1 neg I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup hi : ¬ i = a1 ⊢ i ∈ as ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = a1
· pos I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup hi : i = a1 ⊢ i ∈ as ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = a1 subst hi pos I : Type i : I as : List I x✝ : 0 < ( i :: as ) . length h : ( i :: as ) . Nodup ⊢ i ∈ as ↔ ( i = i ∨ i ∈ as ) ∧ ¬ i = i
simp only [ List.nodup_cons ] at h pos I : Type i : I as : List I x✝ : 0 < ( i :: as ) . length h : ¬ i ∈ as ∧ as . Nodup ⊢ i ∈ as ↔ ( i = i ∨ i ∈ as ) ∧ ¬ i = i
simp [ h ] All goals completed! 🐙
· neg I : Type i : I a1 : I as : List I x✝ : 0 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup hi : ¬ i = a1 ⊢ i ∈ as ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = a1 simp [ hi ] All goals completed! 🐙
| a1 :: as , n + 1 , hn , h => I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i ∈ ( a1 :: as ) . eraseIdx ( n + 1 ) ↔ i ∈ a1 :: as ∧ i ≠ ( a1 :: as ) [ n + 1 ] by I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i ∈ ( a1 :: as ) . eraseIdx ( n + 1 ) ↔ i ∈ a1 :: as ∧ i ≠ ( a1 :: as ) [ n + 1 ]
simp only [ List.eraseIdx_cons_succ , List.mem_cons , List.getElem_cons_succ , ne_eq ] I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ( a1 :: as ) . Nodup ⊢ i = a1 ∨ i ∈ as . eraseIdx n ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
simp only [ List.nodup_cons ] at h I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ¬ a1 ∈ as ∧ as . Nodup ⊢ i = a1 ∨ i ∈ as . eraseIdx n ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
rw [ mem_eraseIdx_nodup i as n ( Nat.succ_lt_succ_iff . mp hn ) h . 2 I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ¬ a1 ∈ as ∧ as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ i ≠ as [ n ] ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ¬ a1 ∈ as ∧ as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ i ≠ as [ n ] ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] ] I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ¬ a1 ∈ as ∧ as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ i ≠ as [ n ] ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
simp_all only [ ne_eq ] I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length h : ¬ a1 ∈ as ∧ as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
obtain ⟨ left , right ⟩ := h I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] ↔ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
apply Iff.intro mp I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] → ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] mpr I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup ⊢ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] → i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ]
· mp I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup ⊢ i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] → ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] intro a mp I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup a : i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] ⊢ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
cases a with
| inl h => mp.inl I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup h : i = a1 ⊢ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ]
subst h mp.inl I : Type i : I as : List I n : ℕ right : as . Nodup hn : n + 1 < ( i :: as ) . length left : ¬ i ∈ as ⊢ ( i = i ∨ i ∈ as ) ∧ ¬ i = as [ n ]
simp_all only [ or_false , true_and ] mp.inl I : Type i : I as : List I n : ℕ right : as . Nodup hn : n + 1 < ( i :: as ) . length left : ¬ i ∈ as ⊢ ¬ i = as [ n ]
apply Aesop.BuiltinRules.not_intro mp.inl I : Type i : I as : List I n : ℕ right : as . Nodup hn : n + 1 < ( i :: as ) . length left : ¬ i ∈ as ⊢ i = as [ n ] → False
intro a mp.inl I : Type i : I as : List I n : ℕ right : as . Nodup hn : n + 1 < ( i :: as ) . length left : ¬ i ∈ as a : i = as [ n ] ⊢ False
simp_all only [ List.getElem_mem , not_true_eq_false ] All goals completed! 🐙
| inr h_1 => mp.inr I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup h_1 : i ∈ as ∧ ¬ i = as [ n ] ⊢ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] simp_all only [ or_true , not_false_eq_true , and_self ] All goals completed! 🐙
· mpr I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup ⊢ ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] → i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ] intro a mpr I : Type i : I a1 : I as : List I n : ℕ hn : n + 1 < ( a1 :: as ) . length left : ¬ a1 ∈ as right : as . Nodup a : ( i = a1 ∨ i ∈ as ) ∧ ¬ i = as [ n ] ⊢ i = a1 ∨ i ∈ as ∧ ¬ i = as [ n ]
simp_all only [ not_false_eq_true , and_true ] All goals completed! 🐙 lemma insertIdx_eq_take_drop { I : Type } ( i : I ) : ( r : List I ) → ( n : Fin r . length . succ ) →
List.insertIdx r n i = List.take n r ++ i :: r . drop n
| [ ] , 0 => I : Type i : I ⊢ [ ] . insertIdx (↑ 0 ) i = List.take ↑ 0 [ ] ++ i :: List.drop ↑ 0 [ ] by I : Type i : I ⊢ [ ] . insertIdx (↑ 0 ) i = List.take ↑ 0 [ ] ++ i :: List.drop ↑ 0 [ ] simp All goals completed! 🐙
| a :: as , 0 => I : Type i : I a : I as : List I ⊢ ( a :: as ) . insertIdx (↑ 0 ) i = List.take (↑ 0 ) ( a :: as ) ++ i :: List.drop (↑ 0 ) ( a :: as ) by I : Type i : I a : I as : List I ⊢ ( a :: as ) . insertIdx (↑ 0 ) i = List.take (↑ 0 ) ( a :: as ) ++ i :: List.drop (↑ 0 ) ( a :: as )
simp All goals completed! 🐙
| a :: as , ⟨ n + 1 , h ⟩ => I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i = List.take (↑ ⟨ n + 1 , h ⟩ ) ( a :: as ) ++ i :: List.drop (↑ ⟨ n + 1 , h ⟩ ) ( a :: as ) by I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i = List.take (↑ ⟨ n + 1 , h ⟩ ) ( a :: as ) ++ i :: List.drop (↑ ⟨ n + 1 , h ⟩ ) ( a :: as )
simp only [ List.insertIdx_succ_cons , List.take_succ_cons , List.drop_succ_cons , List.cons_append ,
List.cons.injEq , true_and ] I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ as . insertIdx n i = List.take n as ++ i :: List.drop n as
exact insertIdx_eq_take_drop i as ⟨ n , Nat.succ_lt_succ_iff . mp h ⟩ All goals completed! 🐙 @[ simp ]
lemma insertIdx_length_fin { I : Type } ( i : I ) :
( r : List I ) → ( n : Fin r . length . succ ) →
( List.insertIdx r n i ) . length = r . length . succ
| [ ] , 0 => I : Type i : I ⊢ ( [ ] . insertIdx (↑ 0 ) i ) . length = [ ] . length . succ by I : Type i : I ⊢ ( [ ] . insertIdx (↑ 0 ) i ) . length = [ ] . length . succ simp All goals completed! 🐙
| a :: as , 0 => I : Type i : I a : I as : List I ⊢ ( ( a :: as ) . insertIdx (↑ 0 ) i ) . length = ( a :: as ) . length . succ by I : Type i : I a : I as : List I ⊢ ( ( a :: as ) . insertIdx (↑ 0 ) i ) . length = ( a :: as ) . length . succ simp All goals completed! 🐙
| a :: as , ⟨ n + 1 , h ⟩ => I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) . length = ( a :: as ) . length . succ by I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) . length = ( a :: as ) . length . succ
simp only [ List.insertIdx_succ_cons , List.length_cons , Nat.succ_eq_add_one , add_left_inj ] I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ ⊢ ( as . insertIdx n i ) . length = as . length + 1
exact insertIdx_length_fin i as ⟨ n , Nat.succ_lt_succ_iff . mp h ⟩ All goals completed! 🐙 @[ simp ]
lemma insertIdx_getElem_fin { I : Type } ( i : I ) :
( r : List I ) → ( k : Fin r . length . succ ) → ( m : Fin r . length ) →
( List.insertIdx r k i ) [ ( k . succAbove m ) . val ] = r [ m . val ]
| [ ] , 0 , m => I : Type i : I m : Fin [ ] . length ⊢ ( [ ] . insertIdx (↑ 0 ) i ) [ ↑ ( succAbove 0 m ) ] = [ ] [ ↑ m ] by I : Type i : I m : Fin [ ] . length ⊢ ( [ ] . insertIdx (↑ 0 ) i ) [ ↑ ( succAbove 0 m ) ] = [ ] [ ↑ m ] exact Fin.elim0 m All goals completed! 🐙
| a :: as , 0 , m => I : Type i : I a : I as : List I m : Fin ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ 0 ) i ) [ ↑ ( succAbove 0 m ) ] = ( a :: as ) [ ↑ m ] by I : Type i : I a : I as : List I m : Fin ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ 0 ) i ) [ ↑ ( succAbove 0 m ) ] = ( a :: as ) [ ↑ m ] simp All goals completed! 🐙
| a :: as , ⟨ n + 1 , h ⟩ , ⟨ 0 , h0 ⟩ => I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ h0 : 0 < ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) [ ↑ ( ⟨ n + 1 , h ⟩ . succAbove ⟨ 0 , h0 ⟩ ) ] = ( a :: as ) [ ↑ ⟨ 0 , h0 ⟩ ] by I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ h0 : 0 < ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) [ ↑ ( ⟨ n + 1 , h ⟩ . succAbove ⟨ 0 , h0 ⟩ ) ] = ( a :: as ) [ ↑ ⟨ 0 , h0 ⟩ ]
simp [ Fin.succAbove , Fin.lt_def ] All goals completed! 🐙
| a :: as , ⟨ n + 1 , h ⟩ , ⟨ m + 1 , hm ⟩ => I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) [ ↑ ( ⟨ n + 1 , h ⟩ . succAbove ⟨ m + 1 , hm ⟩ ) ] = ( a :: as ) [ ↑ ⟨ m + 1 , hm ⟩ ] by I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length ⊢ ( ( a :: as ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) i ) [ ↑ ( ⟨ n + 1 , h ⟩ . succAbove ⟨ m + 1 , hm ⟩ ) ] = ( a :: as ) [ ↑ ⟨ m + 1 , hm ⟩ ]
simp only [ List.insertIdx_succ_cons , List.length_cons , Nat.succ_eq_add_one ,
List.getElem_cons_succ ] I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length ⊢ ( a :: as . insertIdx n i ) [ ↑ ( ⟨ n + 1 , h ⟩ . succAbove ⟨ m + 1 , hm ⟩ ) ] = as [ m ]
conv_rhs => rw [ ← insertIdx_getElem_fin i as ⟨ n , Nat.succ_lt_succ_iff . mp h ⟩
⟨ m , Nat.lt_of_succ_lt_succ hm ⟩ ] I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length | ( as . insertIdx (↑ ⟨ n , ⋯ ⟩ ) i ) [ ↑ ( ⟨ n , ⋯ ⟩ . succAbove ⟨ m , ⋯ ⟩ ) ]
simp only [ Fin.succAbove , Fin.castSucc_mk , Fin.lt_def , add_lt_add_iff_right , Fin.succ_mk ,
Nat.succ_eq_add_one ] I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length ⊢ ( a :: as . insertIdx n i ) [ ↑ ( if m < n then ⟨ m + 1 , ⋯ ⟩ else ⟨ m + 1 + 1 , ⋯ ⟩ ) ] =
( as . insertIdx n i ) [ ↑ ( if m < n then ⟨ m , ⋯ ⟩ else ⟨ m + 1 , ⋯ ⟩ ) ]
split isTrue I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length h✝ : m < n ⊢ ( a :: as . insertIdx n i ) [ ↑ ⟨ m + 1 , ⋯ ⟩ ] = ( as . insertIdx n i ) [ ↑ ⟨ m , ⋯ ⟩ ] isFalse I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length h✝ : ¬ m < n ⊢ ( a :: as . insertIdx n i ) [ ↑ ⟨ m + 1 + 1 , ⋯ ⟩ ] = ( as . insertIdx n i ) [ ↑ ⟨ m + 1 , ⋯ ⟩ ]
· isTrue I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length h✝ : m < n ⊢ ( a :: as . insertIdx n i ) [ ↑ ⟨ m + 1 , ⋯ ⟩ ] = ( as . insertIdx n i ) [ ↑ ⟨ m , ⋯ ⟩ ] simp_all only [ List.getElem_cons_succ ] All goals completed! 🐙
· isFalse I : Type i : I a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length . succ m : ℕ hm : m + 1 < ( a :: as ) . length h✝ : ¬ m < n ⊢ ( a :: as . insertIdx n i ) [ ↑ ⟨ m + 1 + 1 , ⋯ ⟩ ] = ( as . insertIdx n i ) [ ↑ ⟨ m + 1 , ⋯ ⟩ ] simp_all only [ List.getElem_cons_succ ] All goals completed! 🐙 lemma insertIdx_eraseIdx_fin { I : Type } :
( r : List I ) → ( k : Fin r . length ) →
( List.eraseIdx r k ) . insertIdx k r [ k ] = r
| [ ] , k => I : Type k : Fin [ ] . length ⊢ ( [ ] . eraseIdx ↑ k ) . insertIdx ↑ k [ ] [ k ] = [ ] by I : Type k : Fin [ ] . length ⊢ ( [ ] . eraseIdx ↑ k ) . insertIdx ↑ k [ ] [ k ] = [ ] exact Fin.elim0 k All goals completed! 🐙
| a :: as , ⟨ 0 , h ⟩ => I : Type a : I as : List I h : 0 < ( a :: as ) . length ⊢ ( ( a :: as ) . eraseIdx ↑ ⟨ 0 , h ⟩ ) . insertIdx (↑ ⟨ 0 , h ⟩ ) ( a :: as ) [ ⟨ 0 , h ⟩ ] = a :: as by I : Type a : I as : List I h : 0 < ( a :: as ) . length ⊢ ( ( a :: as ) . eraseIdx ↑ ⟨ 0 , h ⟩ ) . insertIdx (↑ ⟨ 0 , h ⟩ ) ( a :: as ) [ ⟨ 0 , h ⟩ ] = a :: as simp All goals completed! 🐙
| a :: as , ⟨ n + 1 , h ⟩ => I : Type a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length ⊢ ( ( a :: as ) . eraseIdx ↑ ⟨ n + 1 , h ⟩ ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) ( a :: as ) [ ⟨ n + 1 , h ⟩ ] = a :: as by I : Type a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length ⊢ ( ( a :: as ) . eraseIdx ↑ ⟨ n + 1 , h ⟩ ) . insertIdx (↑ ⟨ n + 1 , h ⟩ ) ( a :: as ) [ ⟨ n + 1 , h ⟩ ] = a :: as
simp only [ List.length_cons , Fin.getElem_fin , List.getElem_cons_succ , List.eraseIdx_cons_succ ,
List.insertIdx_succ_cons , List.cons.injEq , true_and ] I : Type a : I as : List I n : ℕ h : n + 1 < ( a :: as ) . length ⊢ ( as . eraseIdx n ) . insertIdx n as [ n ] = as
exact insertIdx_eraseIdx_fin as ⟨ n , Nat.lt_of_succ_lt_succ h ⟩ All goals completed! 🐙 lemma insertIdx_length_fst_append { I : Type } ( φ : I ) : ( φs φs' : List I ) →
List.insertIdx ( φs ++ φs' ) φs . length φ = ( φs ++ φ :: φs' )
| [ ] , φs' => I : Type φ : I φs' : List I ⊢ ( [ ] ++ φs' ) . insertIdx [ ] . length φ = [ ] ++ φ :: φs' by I : Type φ : I φs' : List I ⊢ ( [ ] ++ φs' ) . insertIdx [ ] . length φ = [ ] ++ φ :: φs' simp All goals completed! 🐙
| φ' :: φs , φs' => I : Type φ : I φ' : I φs : List I φs' : List I ⊢ ( φ' :: φs ++ φs' ) . insertIdx ( φ' :: φs ) . length φ = φ' :: φs ++ φ :: φs' by I : Type φ : I φ' : I φs : List I φs' : List I ⊢ ( φ' :: φs ++ φs' ) . insertIdx ( φ' :: φs ) . length φ = φ' :: φs ++ φ :: φs'
simp only [ List.length_cons , List.cons_append , List.insertIdx_succ_cons , List.cons.injEq ,
true_and ] I : Type φ : I φ' : I φs : List I φs' : List I ⊢ ( φs ++ φs' ) . insertIdx φs . length φ = φs ++ φ :: φs'
exact insertIdx_length_fst_append φ φs φs' All goals completed! 🐙 lemma get_eq_insertIdx_succAbove { I : Type } ( i : I ) ( r : List I ) ( k : Fin r . length . succ ) :
r . get = ( List.insertIdx r k i ) . get ∘
( finCongr ( insertIdx_length_fin i r k ) . symm ) ∘ k . succAbove := by I : Type i : I r : List I k : Fin r . length . succ ⊢ r . get = ( r . insertIdx (↑ k ) i ) . get ∘ ⇑ ( finCongr ⋯ ) ∘ k . succAbove
funext i I : Type i✝ : I r : List I k : Fin r . length . succ i : Fin r . length ⊢ r . get i = ( ( r . insertIdx (↑ k ) i✝ ) . get ∘ ⇑ ( finCongr ⋯ ) ∘ k . succAbove ) i
simp All goals completed! 🐙 lemma take_insert_same { I : Type } ( i : I ) :
( n : ℕ ) → ( r : List I ) →
List.take n ( List.insertIdx r n i ) = List.take n r
| 0 , _ => I : Type i : I x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx 0 i ) = List.take 0 x✝ by I : Type i : I x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx 0 i ) = List.take 0 x✝ simp All goals completed! 🐙
| _ + 1 , [ ] => I : Type i : I n✝ : ℕ ⊢ List.take ( n✝ + 1 ) ( [ ] . insertIdx ( n✝ + 1 ) i ) = List.take ( n✝ + 1 ) [ ] by I : Type i : I n✝ : ℕ ⊢ List.take ( n✝ + 1 ) ( [ ] . insertIdx ( n✝ + 1 ) i ) = List.take ( n✝ + 1 ) [ ] simp All goals completed! 🐙
| n + 1 , a :: as => I : Type i : I n : ℕ a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . insertIdx ( n + 1 ) i ) = List.take ( n + 1 ) ( a :: as ) by I : Type i : I n : ℕ a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . insertIdx ( n + 1 ) i ) = List.take ( n + 1 ) ( a :: as )
simp only [ List.insertIdx_succ_cons , List.take_succ_cons , List.cons.injEq , true_and ] I : Type i : I n : ℕ a : I as : List I ⊢ List.take n ( as . insertIdx n i ) = List.take n as
exact take_insert_same i n as All goals completed! 🐙 lemma take_eraseIdx_same { I : Type } :
( n : ℕ ) → ( r : List I ) →
List.take n ( List.eraseIdx r n ) = List.take n r
| 0 , _ => I : Type x✝ : List I ⊢ List.take 0 ( x✝ . eraseIdx 0 ) = List.take 0 x✝ by I : Type x✝ : List I ⊢ List.take 0 ( x✝ . eraseIdx 0 ) = List.take 0 x✝ simp All goals completed! 🐙
| _ + 1 , [ ] => I : Type n✝ : ℕ ⊢ List.take ( n✝ + 1 ) ( [ ] . eraseIdx ( n✝ + 1 ) ) = List.take ( n✝ + 1 ) [ ] by I : Type n✝ : ℕ ⊢ List.take ( n✝ + 1 ) ( [ ] . eraseIdx ( n✝ + 1 ) ) = List.take ( n✝ + 1 ) [ ] simp All goals completed! 🐙
| n + 1 , a :: as => I : Type n : ℕ a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . eraseIdx ( n + 1 ) ) = List.take ( n + 1 ) ( a :: as ) by I : Type n : ℕ a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . eraseIdx ( n + 1 ) ) = List.take ( n + 1 ) ( a :: as )
simp only [ List.eraseIdx_cons_succ , List.take_succ_cons , List.cons.injEq , true_and ] I : Type n : ℕ a : I as : List I ⊢ List.take n ( as . eraseIdx n ) = List.take n as
exact take_eraseIdx_same n as All goals completed! 🐙
lemma drop_eraseIdx_succ { I : Type } :
( n : ℕ ) → ( r : List I ) → ( hn : n < r . length ) →
r [ n ] :: List.drop n ( List.eraseIdx r n ) = List.drop n r
| 0 , _ , _ => I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ [ 0 ] :: List.drop 0 ( x✝¹ . eraseIdx 0 ) = List.drop 0 x✝¹ by I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ [ 0 ] :: List.drop 0 ( x✝¹ . eraseIdx 0 ) = List.drop 0 x✝¹
simp only [ List.eraseIdx_zero , List.drop_tail , zero_add , List.drop_one , List.drop_zero ] I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ [ 0 ] :: x✝¹ . tail = x✝¹
rw [ @ List.getElem_zero I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ . head ⋯ :: x✝¹ . tail = x✝¹ I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ . head ⋯ :: x✝¹ . tail = x✝¹ ] I : Type x✝¹ : List I x✝ : 0 < x✝¹ . length ⊢ x✝¹ . head ⋯ :: x✝¹ . tail = x✝¹
exact List.cons_head_tail _ All goals completed! 🐙
| n + 1 , [ ] , hn => I : Type n : ℕ hn : n + 1 < [ ] . length ⊢ [ ] [ n + 1 ] :: List.drop ( n + 1 ) ( [ ] . eraseIdx ( n + 1 ) ) = List.drop ( n + 1 ) [ ] by I : Type n : ℕ hn : n + 1 < [ ] . length ⊢ [ ] [ n + 1 ] :: List.drop ( n + 1 ) ( [ ] . eraseIdx ( n + 1 ) ) = List.drop ( n + 1 ) [ ] simp at hn All goals completed! 🐙
| n + 1 , a :: as , hn => I : Type n : ℕ a : I as : List I hn : n + 1 < ( a :: as ) . length ⊢ ( a :: as ) [ n + 1 ] :: List.drop ( n + 1 ) ( ( a :: as ) . eraseIdx ( n + 1 ) ) = List.drop ( n + 1 ) ( a :: as ) by I : Type n : ℕ a : I as : List I hn : n + 1 < ( a :: as ) . length ⊢ ( a :: as ) [ n + 1 ] :: List.drop ( n + 1 ) ( ( a :: as ) . eraseIdx ( n + 1 ) ) = List.drop ( n + 1 ) ( a :: as )
simp only [ List.getElem_cons_succ , List.eraseIdx_cons_succ , List.drop_succ_cons ] I : Type n : ℕ a : I as : List I hn : n + 1 < ( a :: as ) . length ⊢ as [ n ] :: List.drop n ( as . eraseIdx n ) = List.drop n as
refine drop_eraseIdx_succ n as _ All goals completed! 🐙 lemma take_insert_gt { I : Type } ( i : I ) :
( n m : ℕ ) → ( h : n < m ) → ( r : List I ) →
List.take n ( List.insertIdx r m i ) = List.take n r
| 0 , 0 , _ , _ => I : Type i : I x✝¹ : 0 < 0 x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx 0 i ) = List.take 0 x✝ by I : Type i : I x✝¹ : 0 < 0 x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx 0 i ) = List.take 0 x✝ simp All goals completed! 🐙
| 0 , m + 1 , _ , _ => I : Type i : I m : ℕ x✝¹ : 0 < m + 1 x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx ( m + 1 ) i ) = List.take 0 x✝ by I : Type i : I m : ℕ x✝¹ : 0 < m + 1 x✝ : List I ⊢ List.take 0 ( x✝ . insertIdx ( m + 1 ) i ) = List.take 0 x✝ simp All goals completed! 🐙
| n + 1 , m + 1 , _ , [ ] => I : Type i : I n : ℕ m : ℕ x✝ : n + 1 < m + 1 ⊢ List.take ( n + 1 ) ( [ ] . insertIdx ( m + 1 ) i ) = List.take ( n + 1 ) [ ] by I : Type i : I n : ℕ m : ℕ x✝ : n + 1 < m + 1 ⊢ List.take ( n + 1 ) ( [ ] . insertIdx ( m + 1 ) i ) = List.take ( n + 1 ) [ ] simp All goals completed! 🐙
| n + 1 , m + 1 , h , a :: as => I : Type i : I n : ℕ m : ℕ h : n + 1 < m + 1 a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . insertIdx ( m + 1 ) i ) = List.take ( n + 1 ) ( a :: as ) by I : Type i : I n : ℕ m : ℕ h : n + 1 < m + 1 a : I as : List I ⊢ List.take ( n + 1 ) ( ( a :: as ) . insertIdx ( m + 1 ) i ) = List.take ( n + 1 ) ( a :: as )
simp only [ List.insertIdx_succ_cons , List.take_succ_cons , List.cons.injEq , true_and ] I : Type i : I n : ℕ m : ℕ h : n + 1 < m + 1 a : I as : List I ⊢ List.take n ( as . insertIdx m i ) = List.take n as
refine take_insert_gt i n m ( Nat.succ_lt_succ_iff . mp h ) as All goals completed! 🐙
lemma take_insert_let { I : Type } ( i : I ) :
( n m : ℕ ) → ( h : m ≤ n ) → ( r : List I ) → ( hm : m ≤ r . length ) →
( List.take ( n + 1 ) ( List.insertIdx r m i ) ) . Perm ( i :: List.take n r )
| 0 , 0 , h , _ , _ => I : Type i : I h : 0 ≤ 0 x✝¹ : List I x✝ : 0 ≤ x✝¹ . length ⊢ ( List.take ( 0 + 1 ) ( x✝¹ . insertIdx 0 i ) ) . Perm ( i :: List.take 0 x✝¹ ) by I : Type i : I h : 0 ≤ 0 x✝¹ : List I x✝ : 0 ≤ x✝¹ . length ⊢ ( List.take ( 0 + 1 ) ( x✝¹ . insertIdx 0 i ) ) . Perm ( i :: List.take 0 x✝¹ ) simp All goals completed! 🐙
| m + 1 , 0 , h , r , _ => I : Type i : I m : ℕ h : 0 ≤ m + 1 r : List I x✝ : 0 ≤ r . length ⊢ ( List.take ( m + 1 + 1 ) ( r . insertIdx 0 i ) ) . Perm ( i :: List.take ( m + 1 ) r ) by I : Type i : I m : ℕ h : 0 ≤ m + 1 r : List I x✝ : 0 ≤ r . length ⊢ ( List.take ( m + 1 + 1 ) ( r . insertIdx 0 i ) ) . Perm ( i :: List.take ( m + 1 ) r ) simp All goals completed! 🐙
| n + 1 , m + 1 , h , [ ] , hm => I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 hm : m + 1 ≤ [ ] . length ⊢ ( List.take ( n + 1 + 1 ) ( [ ] . insertIdx ( m + 1 ) i ) ) . Perm ( i :: List.take ( n + 1 ) [ ] ) by I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 hm : m + 1 ≤ [ ] . length ⊢ ( List.take ( n + 1 + 1 ) ( [ ] . insertIdx ( m + 1 ) i ) ) . Perm ( i :: List.take ( n + 1 ) [ ] )
simp at hm All goals completed! 🐙
| n + 1 , m + 1 , h , a :: as , hm => I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length ⊢ ( List.take ( n + 1 + 1 ) ( ( a :: as ) . insertIdx ( m + 1 ) i ) ) . Perm ( i :: List.take ( n + 1 ) ( a :: as ) ) by I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length ⊢ ( List.take ( n + 1 + 1 ) ( ( a :: as ) . insertIdx ( m + 1 ) i ) ) . Perm ( i :: List.take ( n + 1 ) ( a :: as ) )
simp only [ List.insertIdx_succ_cons , List.take_succ_cons ] I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length ⊢ ( a :: List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( i :: a :: List.take n as )
have hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) := by I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length ⊢ ( List.take ( n + 1 + 1 ) ( ( a :: as ) . insertIdx ( m + 1 ) i ) ) . Perm ( i :: List.take ( n + 1 ) ( a :: as ) ) I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) ⊢ ( a :: List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( i :: a :: List.take n as )
exact List.Perm.swap a i ( List.take n as ) I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) ⊢ ( a :: List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( i :: a :: List.take n as ) I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) ⊢ ( a :: List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( i :: a :: List.take n as )
refine List.Perm.trans ? _ hp . symm I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) ⊢ ( a :: List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( a :: i :: List.take n as )
refine List.Perm.cons a ? _ I : Type i : I n : ℕ m : ℕ h : m + 1 ≤ n + 1 a : I as : List I hm : m + 1 ≤ ( a :: as ) . length hp : ( i :: a :: List.take n as ) . Perm ( a :: i :: List.take n as ) ⊢ ( List.take ( n + 1 ) ( as . insertIdx m i ) ) . Perm ( i :: List.take n as )
exact take_insert_let i n m ( Nat.le_of_succ_le_succ h ) as ( Nat.le_of_succ_le_succ hm ) All goals completed! 🐙