Basic

📁 Source: Mathlib/Data/Fin/Tuple/Basic.lean

Statistics

Metric	Count
Definitions `append`, `cons`, `consCases`, `consEquiv`, `consInduction`, `contractNth`, `find`, `init`, `insertNth`, `insertNthEquiv`, `removeNth`, `repeat`, `snoc`, `snocCases`, `snocEquiv`, `snocInduction`, `succAboveCases`, `tail`, `piFinTwoEquiv`	19
Theorems `addCases_castAdd_natAdd`, `append_assoc`, `append_castAdd_natAdd`, `append_cast_left`, `append_cast_right`, `append_comp_rev`, `append_comp_sumElim`, `append_cons`, `append_elim0`, `append_injective_iff`, `append_left`, `append_left'`, `append_left_eq_cons`, `append_left_nil`, `append_left_snoc`, `append_rev`, `append_right`, `append_right_cons`, `append_right_eq_snoc`, `append_right_nil`, `append_snoc`, `comp_cons`, `comp_contractNth`, `comp_init`, `comp_snoc`, `comp_tail`, `consCases_cons`, `consEquiv_apply`, `consEquiv_symm_apply`, `cons_comp_rev`, `cons_eq_append`, `cons_inj`, `cons_injective2`, `cons_injective_iff`, `cons_injective_of_injective`, `cons_last`, `cons_le`, `cons_le_cons`, `cons_left_injective`, `cons_one`, `cons_rev`, `cons_right_injective`, `cons_self_tail`, `cons_snoc_eq_snoc_cons`, `cons_succ`, `cons_update`, `cons_zero`, `contractNth_apply_of_eq`, `contractNth_apply_of_gt`, `contractNth_apply_of_lt`, `contractNth_apply_of_ne`, `elim0_append`, `eq_insertNth_iff`, `eq_self_or_eq_succAbove`, `exists_cons`, `exists_fin_succ_pi`, `exists_fin_zero_pi`, `exists_iff_castSucc`, `exists_iff_succ`, `exists_iff_succAbove`, `find?_decide_eq_dite`, `find?_decide_get_eq_find`, `find?_eq_dite`, `find?_eq_some_find_of_exists`, `find?_eq_some_find_of_isSome`, `find_congr`, `find_congr'`, `find_eq_dite`, `find_eq_iff`, `find_eq_zero`, `find_le`, `find_le_iff`, `find_le_of_pos`, `find_lt_iff`, `find_mem_find?_decide`, `find_min`, `find_mono`, `find_mono_of_le`, `find_nat_lt`, `find_of_find_le`, `find_of_not_zero`, `find_pos`, `find_spec`, `forall_fin_add`, `forall_fin_add_pi`, `forall_fin_succ_pi`, `forall_fin_zero_pi`, `forall_iff_castSucc`, `forall_iff_succ`, `forall_iff_succAbove`, `get_find?_eq_find_of_eq_true`, `init_def`, `init_snoc`, `init_update_castSucc`, `init_update_last`, `insertNthEquiv_apply`, `insertNthEquiv_last`, `insertNthEquiv_symm_apply`, `insertNthEquiv_zero`, `insertNth_apply_above`, `insertNth_apply_below`, `insertNth_apply_same`, `insertNth_apply_succAbove`, `insertNth_binop`, `insertNth_comp_rev`, `insertNth_comp_succAbove`, `insertNth_eq_iff`, `insertNth_inj`, `insertNth_injective2`, `insertNth_last`, `insertNth_last'`, `insertNth_le_iff`, `insertNth_left_injective`, `insertNth_removeNth`, `insertNth_rev`, `insertNth_right_injective`, `insertNth_self_removeNth`, `insertNth_succ_cons`, `insertNth_update`, `insertNth_zero`, `insertNth_zero'`, `le_cons`, `le_find_iff`, `le_insertNth_iff`, `lt_find_iff`, `mem_find?_iff`, `range_cons`, `range_fin_succ`, `range_snoc`, `removeNth_apply`, `removeNth_fun_const`, `removeNth_insertNth`, `removeNth_last`, `removeNth_removeNth_eq_swap`, `removeNth_removeNth_heq_swap`, `removeNth_update`, `removeNth_update_succAbove`, `removeNth_zero`, `repeat_add`, `repeat_apply`, `repeat_comp_rev`, `repeat_one`, `repeat_rev`, `repeat_succ`, `repeat_zero`, `sigma_eq_iff_eq_comp_cast`, `sigma_eq_of_eq_comp_cast`, `snocCases_snoc`, `snocEquiv_apply`, `snocEquiv_symm_apply`, `snoc_apply_zero`, `snoc_castAdd`, `snoc_castSucc`, `snoc_comp_castAdd`, `snoc_comp_castSucc`, `snoc_comp_natAdd`, `snoc_comp_rev`, `snoc_eq_append`, `snoc_init_self`, `snoc_inj`, `snoc_injective2`, `snoc_injective_iff`, `snoc_injective_of_injective`, `snoc_last`, `snoc_left_injective`, `snoc_rev`, `snoc_right_injective`, `snoc_update`, `snoc_zero`, `succAbove_cases_eq_insertNth`, `tail_cons`, `tail_def`, `tail_init_eq_init_tail`, `tail_update_succ`, `tail_update_zero`, `tuple0_le`, `update_cons_zero`, `update_insertNth`, `update_snoc_last`, `val_find`, `piFinTwoEquiv_apply`, `piFinTwoEquiv_symm_apply`	182
Total	201

Fin

Definitions

Name	Category	Theorems
`append` 📖	CompOp	39 math math: `append_right_cons`, `appendHomeomorph_apply`, `append_elim0`, `append_assoc`, `List.ofFn_fin_append`, `append_left_eq_cons`, `appendIsometryOfEq_apply`, `append_right_nil`, `ExteriorAlgebra.ιMulti_mul_ιMulti`, `elim0_append`, `append_left_snoc`, `append_right_eq_snoc`, `Embedding.coe_append`, `TensorPower.tprod_mul_tprod`, `append_right`, `append_cons`, `append_comp_sumElim`, `cons_eq_append`, `append_snoc`, `append_injective_iff`, `succFunEquiv_symm_apply`, `append_left'`, `repeat_add`, `take_append_left`, `snoc_eq_append`, `append_left`, `append_cast_right`, `repeat_succ`, `append_rev`, `append_cast_left`, `append_castAdd_natAdd`, `append_comp_rev`, `appendIsometry_apply`, `continuous_append`, `take_append_right`, `appendEquiv_apply`, `edist_append_eq_max_edist`, `append_left_nil`, `RelSeries.append_toFun`
`cons` 📖	CompOp	133 math math: `ContinuousAlternatingMap.cons_add`, `differentiableWithinAt_finCons'`, `insertNth_succ_cons`, `DifferentiableAt.finCons`, `cons_inj`, `DifferentiableWithinAt.finCons`, `Embedding.coe_cons`, `Matrix.Fin.cons_vecCons`, `cons_injective_of_injective`, `HasStrictFDerivAt.finCons`, `cons_succ`, `ContinuousOn.finCons`, `Module.Basis.coe_mkFinConsOfLE`, `LinearEquiv.piFinTwo_symm_apply`, `torusIntegral_succ`, `consEquiv_apply`, `Set.iUnion_cons`, `append_right_cons`, `MeasurableEquiv.piFinTwo_symm_apply`, `HasDerivAt.finCons`, `differentiable_finCons'`, `exists_linearIndependent_cons_of_lt_finrank`, `Function.FromTypes.uncurry_apply_cons`, `Matrix.vandermonde_succ`, `consEquivL_apply`, `consCases_cons`, `Differentiable.finCons`, `preimage_apply_01_prod`, `hasFDerivAt_finCons`, `hasFDerivWithinAt_finCons`, `Function.FromTypes.curry_apply_succ`, `exists_linearIndependent_cons_of_lt_rank`, `MvPolynomial.eval_eq_eval_mv_eval'`, `exists_cons`, `differentiableOn_finCons'`, `linearIndependent_fin_cons`, `append_left_eq_cons`, `ContinuousMultilinearMap.cons_smul`, `sum_cons`, `hasFDerivWithinAt_finCons'`, `exists_fin_succ_pi`, `append_left_snoc`, `hasStrictFDerivAt_finCons`, `cons_comp_rev`, `cons_le_cons`, `snoc_eq_cons_rotate`, `cons_last`, `ContinuousMultilinearMap.cons_add`, `hasFDerivAt_finCons'`, `HasFDerivAt.finCons`, `cons_snoc_eq_snoc_cons`, `cons_apply_cycleRange`, `hasStrictDerivAt_finCons'`, `hasStrictDerivAt_finCons`, `update_cons_zero`, `append_cons`, `HasFDerivWithinAt.finCons`, `differentiableAt_finCons`, `cons_one`, `OrderedFinpartition.extendLeft_partSize`, `cons_le`, `Continuous.finCons`, `ContinuousWithinAt.finCons`, `IsometryEquiv.piFinTwo_symm_apply`, `cons_self_tail`, `MultilinearMap.cons_add`, `cons_eq_append`, `consOrderIso_apply`, `MultilinearMap.curryLeft_apply`, `insertNth_zero'`, `cons_left_injective`, `MultilinearMap.cons_smul`, `LinearIndependent.fin_cons`, `ContinuousAlternatingMap.cons_smul`, `hasStrictFDerivAt_finCons'`, `prodEquivPiFinTwo_apply`, `Matrix.vandermonde_cons`, `FirstOrder.Language.Formula.realize_graph`, `hasDerivAtFilter_finCons'`, `hasDerivWithinAt_finCons'`, `range_cons`, `hasFDerivAtFilter_finCons`, `continuousMultilinearCurryLeftEquiv_apply`, `LinearIndependent.fin_cons'`, `pi_lex_lt_cons_cons`, `insertNth_zero`, `snoc_eq_append`, `prodEquivPiFinTwo_symm_apply`, `Equiv.coe_embeddingFinSucc_symm`, `differentiableAt_finCons'`, `MeasurableEquiv.finTwoArrow_symm_apply`, `insertNth_comp_cycleRange_symm`, `HasStrictDerivAt.finCons`, `cons_mem_piFinset_cons`, `hasDerivAtFilter_finCons`, `forall_fin_succ_pi`, `cons_injective_iff`, `comp_cons`, `ContinuousMultilinearMap.curryLeft_apply`, `snoc_rev`, `hasDerivAt_finCons'`, `cons_injective2`, `DifferentiableOn.finCons`, `ContinuousAt.finCons`, `le_cons`, `HasDerivAtFilter.finCons`, `hasFDerivAtFilter_finCons'`, `Matrix.Fin.cons_vecEmpty`, `HasFDerivAtFilter.finCons`, `Module.Basis.coe_mkFinCons`, `ContinuousMultilinearMap.norm_map_cons_le`, `cons_right_injective`, `differentiable_finCons`, `differentiableOn_finCons`, `hasDerivWithinAt_finCons`, `UniformEquiv.piFinTwo_symm_apply`, `Homeomorph.piFinTwo_symm_apply`, `piFinTwoEquiv_symm_apply`, `prod_cons`, `cons_comp_cycleRange`, `Filter.Tendsto.finCons`, `cons_update`, `hasDerivAt_finCons`, `ContinuousLinearEquiv.piFinTwo_symm_apply`, `snoc_comp_rev`, `List.ofFn_cons`, `cons_zero`, `Function.FromTypes.curry_apply_cons`, `HasDerivWithinAt.finCons`, `differentiableWithinAt_finCons`, `insertNth_apply_cycleRange_symm`, `tail_cons`, `cons_rev`
`consCases` 📖	CompOp	1 math math: `consCases_cons`
`consEquiv` 📖	CompOp	9 math math: `Action.diagonalSuccIsoTensorDiagonal_inv_hom`, `Finset.map_consEquiv_filter_piFinset`, `consEquiv_apply`, `insertNthEquiv_zero`, `Finset.filter_piFinset_eq_map_consEquiv`, `consEquiv_symm_apply`, `consOrderIso_toEquiv`, `consLinearEquiv_symm_apply`, `consLinearEquiv_apply`
`consInduction` 📖	CompOp	—
`contractNth` 📖	CompOp	12 math math: `partialProd_contractNth`, `contractNth_apply_of_gt`, `contractNth_apply_of_ne`, `groupHomology.inhomogeneousChains.d_single`, `inhomogeneousCochains.d_hom_apply`, `inv_partialProd_mul_eq_contractNth`, `neg_partialSum_add_eq_contractNth`, `contractNth_apply_of_eq`, `Rep.barComplex.d_single`, `comp_contractNth`, `partialSum_contractNth`, `contractNth_apply_of_lt`
`find` 📖	CompOp	26 math math: `find_eq_iff`, `find_pos`, `find_congr'`, `find_eq_zero`, `find_mono_of_le`, `find_of_find_le`, `find?_eq_dite`, `find_le_iff`, `le_find_iff`, `find?_eq_some_find_of_isSome`, `find_le_of_pos`, `find_spec`, `find_congr`, `find_mono`, `lt_find_iff`, `find?_eq_some_find_of_exists`, `get_find?_eq_find_of_eq_true`, `find_nat_lt`, `find_mem_find?_decide`, `find_eq_dite`, `find_lt_iff`, `find_of_not_zero`, `val_find`, `find?_decide_get_eq_find`, `find?_decide_eq_dite`, `find_le`
`init` 📖	CompOp	31 math math: `init_def`, `init_update_last`, `Finset.map_snocEquiv_filter_piFinset`, `Finset.card_snocEquiv_filter_piFinset`, `SchwartzMap.iteratedPDeriv_succ_right`, `take_init`, `iteratedFDerivWithin_succ_apply_right`, `continuousMultilinearCurryRightEquiv_symm_apply`, `Filter.Tendsto.finInit`, `ContinuousMultilinearMap.norm_map_init_le`, `ContinuousAt.finInit`, `linearIndependent_fin_succ'`, `snocOrderIso_symm_apply`, `take_eq_init`, `ContinuousMultilinearMap.uncurryRight_apply`, `partialProd_init`, `snoc_init_self`, `iteratedFDeriv_succ_apply_right`, `tail_init_eq_init_tail`, `MultilinearMap.uncurryRight_apply`, `Finset.filter_piFinset_eq_map_snocEquiv`, `continuousMultilinearCurryRightEquiv_symm_apply'`, `init_update_castSucc`, `mem_piFinset_iff_last_init`, `Continuous.finInit`, `partialSum_init`, `removeNth_last`, `init_snoc`, `LineDeriv.iteratedLineDerivOp_succ_right`, `comp_init`, `snocEquiv_symm_apply`
`insertNth` 📖	CompOp	74 math math: `insertNth_succ_cons`, `preimage_insertNth_Icc_of_mem`, `insertNth_comp_succAbove`, `MultilinearMap.map_insertNth_add`, `nndist_insertNth_insertNth`, `insertNth_rev`, `ContinuousAlternatingMap.map_insertNth`, `insertNth_one_right`, `ContinuousAt.finInsertNth`, `insertNthEquiv_apply`, `insertNth_comp_rev`, `MultilinearMap.map_insertNth_smul`, `insertNth_le_iff`, `BoxIntegral.hasIntegral_GP_pderiv`, `insertNth_mem_piFinset_insertNth`, `BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`, `insertNth_right_injective`, `insertNth_apply_succAbove`, `insertNth_self_removeNth`, `insertNth_binop`, `insertNth_injective2`, `insertNth_mul`, `MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv`, `insertNth_apply_below`, `cons_apply_cycleRange`, `BoxIntegral.Box.continuousOn_face_Icc`, `update_insertNth`, `MultilinearMap.curryMid_apply_apply`, `MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable'`, `preimage_insertNth_Icc_of_notMem`, `Continuous.finInsertNth`, `insertNth_apply_same`, `succAbove_cases_eq_insertNth`, `BoxIntegral.Box.mapsTo_insertNth_face`, `insertNth_zero'`, `Filter.Tendsto.finInsertNth`, `BoxIntegral.Box.mapsTo_insertNth_face_Icc`, `RelSeries.insertNth_toFun`, `insertNth_last'`, `insertNth_apply_above`, `insertNth_div`, `insertNth_update`, `BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le`, `insertNth_last`, `insertNth_div_same`, `insertNth_zero`, `insertNth_mem_Icc`, `ContinuousMultilinearMap.curryMid_apply`, `insertNthOrderIso_apply`, `insertNth_comp_cycleRange_symm`, `insertNth_add`, `MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`, `insertNth_removeNth`, `insertNth_zero_right`, `dist_insertNth_insertNth`, `prod_insertNth`, `ContinuousMultilinearMap.norm_map_insertNth_le`, `AlternatingMap.neg_one_pow_smul_map_insertNth`, `AlternatingMap.map_insertNth`, `ContinuousAlternatingMap.neg_one_pow_smul_map_insertNth`, `le_insertNth_iff`, `insertNth_eq_iff`, `insertNth_inj`, `removeNth_insertNth`, `sum_insertNth`, `eq_insertNth_iff`, `ContinuousWithinAt.finInsertNth`, `insertNth_left_injective`, `cons_comp_cycleRange`, `torusIntegral_succAbove`, `insertNth_sub`, `ContinuousOn.finInsertNth`, `insertNth_apply_cycleRange_symm`, `insertNth_sub_same`
`insertNthEquiv` 📖	CompOp	9 math math: `insertNthEquiv_apply`, `insertNthEquiv_last`, `insertNthOrderIso_toEquiv`, `insertNthEquiv_zero`, `insertNthEquiv_symm_apply`, `Finset.filter_piFinset_eq_map_insertNthEquiv`, `Finset.map_insertNthEquiv_filter_piFinset`, `MeasurableEquiv.piFinSuccAbove_symm_apply`, `MeasurableEquiv.piFinSuccAbove_apply`
`removeNth` 📖	CompOp	37 math math: `removeNth_zero`, `removeNth_apply`, `Finset.card_insertNthEquiv_filter_piFinset`, `mem_piFinset_iff_pivot_removeNth`, `removeNth_removeNth_eq_swap`, `insertNthOrderIso_symm_apply`, `AlternatingMap.alternatizeUncurryFin_apply`, `insertNth_self_removeNth`, `extDeriv_apply_vectorField`, `ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply`, `extDerivWithin_apply_vectorField_of_pairwise_commute`, `AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq`, `removeNth_update_succAbove`, `insertNthEquiv_symm_apply`, `AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply`, `mul_prod_removeNth`, `Finset.filter_piFinset_eq_map_insertNthEquiv`, `LinearMap.uncurryMid_apply`, `extDerivWithin_apply_vectorField`, `add_sum_removeNth`, `removeNth_removeNth_heq_swap`, `ContinuousLinearMap.uncurryMid_apply`, `removeNth_update`, `Finset.map_insertNthEquiv_filter_piFinset`, `extDeriv_apply_vectorField_of_pairwise_commute`, `removeNth_last`, `ContinuousAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq`, `insertNth_removeNth`, `AlternatingMap.uncurryFin_apply`, `removeNth_fun_const`, `extDerivWithin_apply`, `insertNth_eq_iff`, `removeNth_insertNth`, `ContinuousLinearMap.norm_map_removeNth_le`, `eq_insertNth_iff`, `ContinuousAlternatingMap.alternatizeUncurryFin_apply`, `extDeriv_apply`
`repeat` 📖	CompOp	9 math math: `repeat_one`, `repeat_zero`, `repeat_comp_rev`, `List.ofFn_fin_repeat`, `repeat_add`, `repeat_rev`, `repeat_succ`, `repeat_apply`, `take_repeat`
`snoc` 📖	CompOp	62 math math: `comp_snoc`, `exists_linearIndependent_snoc_of_lt_finrank`, `ContinuousMultilinearMap.norm_map_snoc_le`, `snoc_inj`, `snoc_castSucc`, `snocCases_snoc`, `FirstOrder.Language.BoundedFormula.realize_ex`, `snocEquiv_apply`, `append_right_cons`, `sum_snoc`, `snoc_left_injective`, `MultilinearMap.curryRight_apply`, `Embedding.coe_snoc`, `snoc_comp_natAdd`, `Matrix.Fin.snoc_vecEmpty`, `snoc_comp_castSucc`, `snoc_injective_iff`, `ContinuousAt.finSnoc`, `snoc_apply_zero`, `FirstOrder.Language.BoundedFormula.realize_all`, `append_left_snoc`, `cons_comp_rev`, `append_right_eq_snoc`, `snoc_eq_cons_rotate`, `Set.iUnion_snoc`, `snoc_update`, `cons_snoc_eq_snoc_cons`, `range_snoc`, `snoc_mem_piFinset_snoc`, `snocOrderIso_apply`, `snoc_zero`, `Matrix.Fin.snoc_vecCons`, `linearIndependent_fin_snoc`, `append_snoc`, `snoc_init_self`, `ContinuousMultilinearMap.curryRight_apply`, `prod_snoc`, `insertNth_last'`, `take_succ_eq_snoc`, `insertNth_last`, `Continuous.finSnoc`, `snoc_eq_append`, `snoc_right_injective`, `update_snoc_last`, `MultilinearMap.snoc_add`, `ContinuousOn.finSnoc`, `snoc_comp_castAdd`, `snoc_injective_of_injective`, `init_snoc`, `snoc_rev`, `continuousMultilinearCurryRightEquiv_apply'`, `exists_linearIndependent_snoc_of_lt_rank`, `ContinuousWithinAt.finSnoc`, `continuousMultilinearCurryRightEquiv_apply`, `MultilinearMap.snoc_smul`, `snoc_last`, `snoc_comp_rev`, `snoc_injective2`, `Filter.Tendsto.finSnoc`, `snoc_castAdd`, `cons_rev`, `continuousMultilinearCurryFin1_apply`
`snocCases` 📖	CompOp	1 math math: `snocCases_snoc`
`snocEquiv` 📖	CompOp	6 math math: `snocEquiv_apply`, `Finset.map_snocEquiv_filter_piFinset`, `insertNthEquiv_last`, `Finset.filter_piFinset_eq_map_snocEquiv`, `snocOrderIso_toEquiv`, `snocEquiv_symm_apply`
`snocInduction` 📖	CompOp	—
`succAboveCases` 📖	CompOp	1 math math: `succAbove_cases_eq_insertNth`
`tail` 📖	CompOp	39 math math: `removeNth_zero`, `comp_tail`, `Finset.map_consEquiv_filter_piFinset`, `Matrix.vandermonde_succ`, `RelSeries.tail_toFun`, `tail_vecCons`, `Embedding.coe_tail`, `LineDeriv.iteratedLineDerivOp_succ_left`, `Finset.filter_piFinset_eq_map_consEquiv`, `Function.FromTypes.uncurry_apply_succ`, `ContinuousLinearMap.uncurryLeft_apply`, `Finsupp.sum_cons'`, `cons_le`, `iteratedFDerivWithin_succ_apply_left`, `Finset.card_consEquiv_filter_piFinset`, `ContinuousLinearMap.norm_map_tail_le`, `cons_self_tail`, `consEquiv_symm_apply`, `ContinuousAt.finTail`, `linearIndependent_fin_succ`, `consOrderIso_symm_apply`, `tail_init_eq_init_tail`, `range_fin_succ`, `partialProd_succ'`, `Continuous.finTail`, `Filter.Tendsto.finTail`, `tail_update_succ`, `SchwartzMap.iteratedPDeriv_succ_left`, `partialSum_succ'`, `tail_update_zero`, `Action.diagonalSuccIsoTensorDiagonal_hom_hom`, `le_cons`, `mem_piFinset_iff_zero_tail`, `tail_def`, `continuousMultilinearCurryLeftEquiv_symm_apply`, `consEquivL_symm_apply`, `LinearMap.uncurryLeft_apply`, `tail_cons`, `iteratedFDeriv_succ_apply_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCases_castAdd_natAdd` 📖	—	—	—	—	—
`append_assoc` 📖	mathematical	—	`append`	—	`append_left` `append_right`
`append_castAdd_natAdd` 📖	mathematical	—	`append`	—	—
`append_cast_left` 📖	mathematical	—	`append`	—	—
`append_cast_right` 📖	mathematical	—	`append`	—	—
`append_comp_rev` 📖	mathematical	—	`append`	—	`append_rev`
`append_comp_sumElim` 📖	mathematical	—	`append`	—	`append_left` `append_right`
`append_cons` 📖	mathematical	—	`append` `cons`	—	—
`append_elim0` 📖	mathematical	—	`append`	—	`append_right_nil`
`append_injective_iff` 📖	mathematical	—	`append`	—	`Sum.elim_injective` `append_comp_sumElim` `Equiv.injective_comp`
`append_left` 📖	mathematical	—	`append`	—	—
`append_left'` 📖	mathematical	—	`append`	—	—
`append_left_eq_cons` 📖	mathematical	—	`append` `cons`	—	`append_left` `cons_zero` `append_right` `cons_succ`
`append_left_nil` 📖	mathematical	—	`append`	—	`append_right`
`append_left_snoc` 📖	mathematical	—	`append` `snoc` `cons`	—	`snoc_eq_append` `append_assoc` `append_left_eq_cons` `append_cast_right`
`append_rev` 📖	mathematical	—	`append`	—	`rev_surjective` `append_left` `append_right` `cast_rev`
`append_right` 📖	mathematical	—	`append`	—	—
`append_right_cons` 📖	mathematical	—	`append` `cons` `snoc`	—	`append_left_snoc`
`append_right_eq_snoc` 📖	mathematical	—	`append` `snoc`	—	`append_left` `snoc_castSucc` `append_right` `snoc_last`
`append_right_nil` 📖	mathematical	—	`append`	—	`append_left`
`append_snoc` 📖	mathematical	—	`append` `snoc`	—	—
`comp_cons` 📖	mathematical	—	`cons`	—	`cons_succ`
`comp_contractNth` 📖	mathematical	—	`contractNth`	—	`lt_trichotomy` `contractNth_apply_of_lt` `contractNth_apply_of_eq` `contractNth_apply_of_gt`
`comp_init` 📖	mathematical	—	`init`	—	—
`comp_snoc` 📖	mathematical	—	`snoc`	—	`snoc_last`
`comp_tail` 📖	mathematical	—	`tail`	—	—
`consCases_cons` 📖	mathematical	—	`consCases` `cons`	—	`consCases.eq_1`
`consEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `consEquiv` `cons`	—	—
`consEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `consEquiv` `tail`	—	—
`cons_comp_rev` 📖	mathematical	—	`cons` `snoc`	—	`cons_rev`
`cons_eq_append` 📖	mathematical	—	`cons` `append`	—	`append_left_eq_cons` `cons_zero`
`cons_inj` 📖	mathematical	—	`cons`	—	`Function.Injective2.eq_iff` `cons_injective2`
`cons_injective2` 📖	mathematical	—	`Function.Injective2` `cons`	—	`cons_succ`
`cons_injective_iff` 📖	mathematical	—	`cons` `Set` `Set.instMembership` `Set.range`	—	`cons_succ` `cons_zero` `succ_injective` `cons_injective_of_injective`
`cons_injective_of_injective` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`cons`	—	`cons_zero` `cons_succ`
`cons_last` 📖	mathematical	—	`cons`	—	`cons_succ`
`cons_le` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `cons` `tail`	—	`le_cons`
`cons_le_cons` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `cons`	—	`cons_succ`
`cons_left_injective` 📖	mathematical	—	`cons`	—	`Function.Injective2.left` `cons_injective2`
`cons_one` 📖	mathematical	—	`cons`	—	`cons_succ`
`cons_rev` 📖	mathematical	—	`cons` `snoc`	—	`insertNth_zero'` `insertNth_last'` `insertNth_rev`
`cons_right_injective` 📖	mathematical	—	`cons`	—	`Function.Injective2.right` `cons_injective2`
`cons_self_tail` 📖	mathematical	—	`cons` `tail`	—	`cons_zero` `cons_succ`
`cons_snoc_eq_snoc_cons` 📖	mathematical	—	`cons` `snoc`	—	`cons_zero` `snoc_apply_zero` `cons_last` `snoc_last` `cons_succ` `snoc_castSucc`
`cons_succ` 📖	mathematical	—	`cons`	—	—
`cons_update` 📖	mathematical	—	`cons` `Function.update`	—	`cons_zero` `Function.update_of_ne` `cons_succ` `Function.update_apply_of_injective` `succ_injective` `Function.update.congr_simp`
`cons_zero` 📖	mathematical	—	`cons`	—	—
`contractNth_apply_of_eq` 📖	mathematical	—	`contractNth`	—	`not_lt` `le_of_eq` `contractNth.eq_1`
`contractNth_apply_of_gt` 📖	mathematical	—	`contractNth`	—	`contractNth.eq_1` `not_lt_of_gt` `ne_of_lt`
`contractNth_apply_of_lt` 📖	mathematical	—	`contractNth`	—	—
`contractNth_apply_of_ne` 📖	mathematical	—	`contractNth` `succAbove`	—	`lt_trichotomy` `succAbove_of_castSucc_lt` `contractNth_apply_of_lt` `succAbove_of_le_castSucc` `le_iff_val_le_val` `le_of_lt` `contractNth_apply_of_gt`
`elim0_append` 📖	mathematical	—	`append`	—	`append_left_nil`
`eq_insertNth_iff` 📖	mathematical	—	`insertNth` `removeNth`	—	`insertNth_eq_iff`
`eq_self_or_eq_succAbove` 📖	mathematical	—	`succAbove`	—	—
`exists_cons` 📖	mathematical	—	`cons`	—	`cons_self_tail`
`exists_fin_succ_pi` 📖	mathematical	—	`cons`	—	`cons_self_tail`
`exists_fin_zero_pi` 📖	mathematical	—	`finZeroElim`	—	`Unique.instSubsingleton` `isEmpty'`
`exists_iff_castSucc` 📖	—	—	—	—	—
`exists_iff_succ` 📖	—	—	—	—	—
`exists_iff_succAbove` 📖	mathematical	—	`succAbove`	—	—
`find?_decide_eq_dite` 📖	mathematical	—	`find`	—	`find?_eq_dite` `find.congr_simp`
`find?_decide_get_eq_find` 📖	mathematical	—	`find`	—	`find?_decide_eq_dite`
`find?_eq_dite` 📖	mathematical	—	`find`	—	—
`find?_eq_some_find_of_exists` 📖	mathematical	—	`find`	—	`find?_eq_dite`
`find?_eq_some_find_of_isSome` 📖	mathematical	—	`find`	—	`find?_eq_dite`
`find_congr` 📖	mathematical	—	`find` `le_rfl` `PartialOrder.toPreorder` `instPartialOrder`	—	`le_antisymm` `le_rfl` `find_mono_of_le`
`find_congr'` 📖	mathematical	—	`find`	—	`find_congr`
`find_eq_dite` 📖	mathematical	—	`find`	—	—
`find_eq_iff` 📖	mathematical	—	`find`	—	`find_le_of_pos`
`find_eq_zero` 📖	mathematical	—	`find`	—	`instIsEmptyFalse`
`find_le` 📖	mathematical	—	`find`	—	`find_le_iff` `le_refl`
`find_le_iff` 📖	mathematical	—	`find`	—	`LE.le.trans` `find_le_of_pos`
`find_le_of_pos` 📖	mathematical	—	`find`	—	`Function.mtr` `find_min` `lt_of_not_ge`
`find_lt_iff` 📖	mathematical	—	`find`	—	`LE.le.trans_lt` `find_le_of_pos`
`find_mem_find?_decide` 📖	mathematical	—	`find`	—	—
`find_min` 📖	—	`find`	—	—	—
`find_mono` 📖	mathematical	—	`find`	—	`find_mono_of_le`
`find_mono_of_le` 📖	mathematical	—	`find` `le_rfl` `PartialOrder.toPreorder` `instPartialOrder`	—	`find_le_of_pos` `le_rfl` `find_spec`
`find_nat_lt` 📖	mathematical	—	`Nat.find` `find`	—	`val_find` `Nat.find_congr`
`find_of_find_le` 📖	mathematical	`find`	`find`	—	`find_eq_iff` `find_spec` `find_min` `LT.lt.trans_le` `natAdd_lt_natAdd_iff`
`find_of_not_zero` 📖	mathematical	—	`find`	—	`find_spec` `find_min`
`find_pos` 📖	mathematical	—	`find`	—	`Iff.not` `find_eq_zero`
`find_spec` 📖	mathematical	—	`find`	—	—
`forall_fin_add` 📖	—	—	—	—	—
`forall_fin_add_pi` 📖	—	—	—	—	`addCases_castAdd_natAdd`
`forall_fin_succ_pi` 📖	mathematical	—	`cons`	—	—
`forall_fin_zero_pi` 📖	mathematical	—	`finZeroElim`	—	`Unique.instSubsingleton` `isEmpty'`
`forall_iff_castSucc` 📖	—	—	—	—	—
`forall_iff_succ` 📖	—	—	—	—	—
`forall_iff_succAbove` 📖	mathematical	—	`succAbove`	—	—
`get_find?_eq_find_of_eq_true` 📖	mathematical	—	`find`	—	`find?_eq_dite`
`init_def` 📖	mathematical	—	`init`	—	—
`init_snoc` 📖	mathematical	—	`init` `snoc`	—	—
`init_update_castSucc` 📖	mathematical	—	`init` `Function.update`	—	`Function.update_self` `Function.update_of_ne`
`init_update_last` 📖	mathematical	—	`init` `Function.update`	—	`Function.update_of_ne`
`insertNthEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `insertNthEquiv` `insertNth`	—	—
`insertNthEquiv_last` 📖	mathematical	—	`insertNthEquiv` `snocEquiv`	—	`Equiv.ext` `insertNth_last'`
`insertNthEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `insertNthEquiv` `removeNth`	—	—
`insertNthEquiv_zero` 📖	mathematical	—	`insertNthEquiv` `consEquiv`	—	`Function.Bijective.injective` `Equiv.symm_bijective` `Equiv.ext`
`insertNth_apply_above` 📖	mathematical	—	`insertNth` `succAbove` `succAbove_pred_of_lt`	—	`succAbove_pred_of_lt` `insertNth.eq_1` `succAbove_castPred_of_lt` `succAboveCases.eq_1`
`insertNth_apply_below` 📖	mathematical	—	`insertNth` `succAbove` `castPred` `succAbove_castPred_of_lt`	—	`succAbove_castPred_of_lt` `insertNth.eq_1` `succAboveCases.eq_1`
`insertNth_apply_same` 📖	mathematical	—	`insertNth`	—	`succAbove_castPred_of_lt`
`insertNth_apply_succAbove` 📖	mathematical	—	`insertNth` `succAbove`	—	`succAbove_castPred_of_lt` `succAbove_ne` `ne_last_of_lt` `succAbove_lt_iff_castSucc_lt` `castPred_succAbove` `ne_zero_of_lt` `lt_succAbove_iff_le_castSucc` `pred_succAbove`
`insertNth_binop` 📖	mathematical	—	`insertNth` `succAbove`	—	`insertNth_eq_iff` `insertNth_apply_same` `insertNth_apply_succAbove`
`insertNth_comp_rev` 📖	mathematical	—	`insertNth`	—	`insertNth_rev`
`insertNth_comp_succAbove` 📖	mathematical	—	`insertNth` `succAbove`	—	`insertNth_apply_succAbove`
`insertNth_eq_iff` 📖	mathematical	—	`insertNth` `removeNth`	—	`forall_iff_succAbove` `insertNth_apply_same` `insertNth_apply_succAbove`
`insertNth_inj` 📖	mathematical	—	`insertNth`	—	`Function.Injective2.eq_iff` `insertNth_injective2`
`insertNth_injective2` 📖	mathematical	—	`Function.Injective2` `insertNth`	—	`insertNth_apply_same` `insertNth_apply_succAbove`
`insertNth_last` 📖	mathematical	—	`insertNth` `snoc` `succAbove` `succAbove_last_apply`	—	`succAbove_last_apply` `insertNth_eq_iff` `snoc_last` `snoc_castSucc` `congr_arg_heq` `succAbove_last`
`insertNth_last'` 📖	mathematical	—	`insertNth` `snoc`	—	`insertNth_last`
`insertNth_le_iff` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `insertNth` `succAbove`	—	`forall_iff_succAbove` `insertNth_apply_same` `insertNth_apply_succAbove`
`insertNth_left_injective` 📖	mathematical	—	`insertNth`	—	`Function.Injective2.left` `insertNth_injective2`
`insertNth_removeNth` 📖	mathematical	—	`insertNth` `removeNth` `Function.update`	—	`Function.update_self` `removeNth_update`
`insertNth_rev` 📖	mathematical	—	`insertNth`	—	`insertNth_apply_same` `rev_succAbove` `insertNth_apply_succAbove`
`insertNth_right_injective` 📖	mathematical	—	`insertNth`	—	`Function.Injective2.right` `insertNth_injective2`
`insertNth_self_removeNth` 📖	mathematical	—	`insertNth` `removeNth`	—	`insertNth_removeNth` `Function.update_eq_self`
`insertNth_succ_cons` 📖	mathematical	—	`insertNth` `cons`	—	`insertNth_apply_same` `cons_succ` `insertNth_apply_succAbove` `cons_zero` `succAbove_ne_zero_zero` `succ_succAbove_succ`
`insertNth_update` 📖	mathematical	—	`insertNth` `Function.update` `succAbove`	—	`Function.update_of_ne` `insertNth_apply_same` `removeNth_update_succAbove` `removeNth_insertNth`
`insertNth_zero` 📖	mathematical	—	`insertNth` `cons` `succAbove` `succAbove_zero`	—	`succAbove_zero` `insertNth_eq_iff` `cons_zero` `cons_succ`
`insertNth_zero'` 📖	mathematical	—	`insertNth` `cons`	—	`insertNth_zero`
`le_cons` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `cons` `tail`	—	`cons_succ`
`le_find_iff` 📖	mathematical	—	`find`	—	—
`le_insertNth_iff` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `insertNth` `succAbove`	—	`forall_iff_succAbove` `insertNth_apply_same` `insertNth_apply_succAbove`
`lt_find_iff` 📖	mathematical	—	`find`	—	—
`mem_find?_iff` 📖	—	—	—	—	—
`range_cons` 📖	mathematical	—	`Set.range` `cons` `Set` `Set.instInsert`	—	`range_fin_succ` `cons_zero` `tail_cons`
`range_fin_succ` 📖	mathematical	—	`Set.range` `Set` `Set.instInsert` `tail`	—	`Set.ext` `Iff.or`
`range_snoc` 📖	mathematical	—	`Set.range` `snoc` `Set` `Set.instInsert`	—	`Set.ext` `snoc_castSucc` `snoc_last`
`removeNth_apply` 📖	mathematical	—	`removeNth` `succAbove`	—	—
`removeNth_fun_const` 📖	mathematical	—	`removeNth`	—	—
`removeNth_insertNth` 📖	mathematical	—	`removeNth` `insertNth`	—	`insertNth_apply_succAbove`
`removeNth_last` 📖	mathematical	—	`removeNth` `init`	—	`succAbove_last`
`removeNth_removeNth_eq_swap` 📖	mathematical	—	`removeNth` `predAbove` `succAbove`	—	`removeNth_removeNth_heq_swap`
`removeNth_removeNth_heq_swap` 📖	mathematical	—	`removeNth` `succAbove` `predAbove`	—	`Function.hfunext` `congr_arg_heq` `succAbove_succAbove_succAbove_predAbove`
`removeNth_update` 📖	mathematical	—	`removeNth` `Function.update`	—	`Function.update_of_ne`
`removeNth_update_succAbove` 📖	mathematical	—	`removeNth` `Function.update` `succAbove`	—	`eq_or_ne` `Function.update_self` `Function.update_of_ne`
`removeNth_zero` 📖	mathematical	—	`removeNth` `tail`	—	—
`repeat_add` 📖	mathematical	—	`repeat` `append`	—	`Function.Surjective.forall` `rightInverse_cast` `append_left` `append_right`
`repeat_apply` 📖	mathematical	—	`repeat`	—	—
`repeat_comp_rev` 📖	mathematical	—	`repeat`	—	`repeat_rev`
`repeat_one` 📖	mathematical	—	`repeat`	—	`Function.Surjective.forall` `rightInverse_cast`
`repeat_rev` 📖	mathematical	—	`repeat`	—	`modNat_rev`
`repeat_succ` 📖	mathematical	—	`repeat` `append`	—	`Function.Surjective.forall` `rightInverse_cast` `append_left` `append_right`
`repeat_zero` 📖	mathematical	—	`repeat`	—	—
`sigma_eq_iff_eq_comp_cast` 📖	—	—	—	—	`sigma_eq_of_eq_comp_cast`
`sigma_eq_of_eq_comp_cast` 📖	—	—	—	—	—
`snocCases_snoc` 📖	mathematical	—	`snocCases` `snoc`	—	`snocCases.eq_1` `init_snoc` `snoc_last`
`snocEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `snocEquiv` `snoc`	—	—
`snocEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `snocEquiv` `init`	—	—
`snoc_apply_zero` 📖	mathematical	—	`snoc`	—	`snoc_castSucc`
`snoc_castAdd` 📖	mathematical	—	`snoc`	—	—
`snoc_castSucc` 📖	mathematical	—	`snoc`	—	—
`snoc_comp_castAdd` 📖	mathematical	—	`snoc`	—	`snoc_castAdd`
`snoc_comp_castSucc` 📖	mathematical	—	`snoc`	—	`snoc_castSucc`
`snoc_comp_natAdd` 📖	mathematical	—	`snoc`	—	`snoc_last` `snoc_castSucc`
`snoc_comp_rev` 📖	mathematical	—	`snoc` `cons`	—	`snoc_rev`
`snoc_eq_append` 📖	mathematical	—	`snoc` `append` `cons`	—	`append_right_eq_snoc`
`snoc_init_self` 📖	mathematical	—	`snoc` `init`	—	`snoc_last` `snoc_castSucc`
`snoc_inj` 📖	mathematical	—	`snoc`	—	`Function.Injective2.eq_iff` `snoc_injective2`
`snoc_injective2` 📖	mathematical	—	`Function.Injective2` `snoc`	—	`snoc_castSucc` `snoc_last`
`snoc_injective_iff` 📖	mathematical	—	`snoc` `Set` `Set.instMembership` `Set.range`	—	`snoc_comp_castSucc` `castSucc_injective` `ne_last_of_lt` `snoc_castSucc` `snoc_last` `snoc_injective_of_injective`
`snoc_injective_of_injective` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`snoc`	—	`snoc_last` `snoc_castSucc` `Set.mem_range_self`
`snoc_last` 📖	mathematical	—	`snoc`	—	—
`snoc_left_injective` 📖	mathematical	—	`snoc`	—	`Function.Injective2.left` `snoc_injective2`
`snoc_rev` 📖	mathematical	—	`snoc` `cons`	—	`insertNth_last'` `insertNth_zero'` `insertNth_rev`
`snoc_right_injective` 📖	mathematical	—	`snoc`	—	`Function.Injective2.right` `snoc_injective2`
`snoc_update` 📖	mathematical	—	`snoc` `Function.update`	—	`snoc_last` `Function.update_of_ne` `eq_or_ne` `snoc_castSucc` `Function.update_self`
`snoc_zero` 📖	mathematical	—	`snoc`	—	—
`succAbove_cases_eq_insertNth` 📖	mathematical	—	`succAboveCases` `insertNth`	—	—
`tail_cons` 📖	mathematical	—	`tail` `cons`	—	—
`tail_def` 📖	mathematical	—	`tail`	—	—
`tail_init_eq_init_tail` 📖	mathematical	—	`tail` `init`	—	—
`tail_update_succ` 📖	mathematical	—	`tail` `Function.update`	—	`Function.update_self` `Function.update_of_ne` `succ_injective`
`tail_update_zero` 📖	mathematical	—	`tail` `Function.update`	—	`Function.update_of_ne`
`tuple0_le` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE`	—	—
`update_cons_zero` 📖	mathematical	—	`Function.update` `cons`	—	`Function.update_self` `cons_zero` `Function.update_of_ne` `cons_succ`
`update_insertNth` 📖	mathematical	—	`Function.update` `insertNth`	—	`Function.update_self` `removeNth_update` `removeNth_insertNth`
`update_snoc_last` 📖	mathematical	—	`Function.update` `snoc`	—	`Function.update_self` `snoc_last` `Function.update_of_ne` `snoc_castSucc`
`val_find` 📖	mathematical	—	`find` `Nat.find`	—	`Nat.find_eq_iff` `find_spec` `find_min`

(root)

Definitions

Name	Category	Theorems
`piFinTwoEquiv` 📖	CompOp	9 math math: `Function.FromTypes.curry_two_eq_curry`, `Finset.Nat.antidiagonalTuple_two`, `finTwoArrowEquiv_apply`, `Function.FromTypes.uncurry_two_eq_uncurry`, `Nat.image_piFinTwoEquiv_finMulAntidiag`, `piFinTwoEquiv_apply`, `RingEquiv.piFinTwo_symm_apply`, `RingEquiv.piFinTwo_apply`, `piFinTwoEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piFinTwoEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `piFinTwoEquiv`	—	—
`piFinTwoEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `piFinTwoEquiv` `Fin.cons` `finZeroElim`	—	—

---

← Back to Index