refactor: Lint
This commit is contained in:
jstoobysmith
parent
2490535569
commit
c7bd59c981
10 changed files with 120 additions and 90 deletions
|
|
@ -123,8 +123,9 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c
|
|||
rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply, Finset.disjoint_map]
|
||||
exact c.2.2 a' ha' b' hb'
|
||||
|
||||
lemma insertAndContractNat_of_isSome (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted)
|
||||
(hj : j.isSome) : (insertAndContractNat c i j).1 = Insert.insert {i, i.succAbove (j.get hj)}
|
||||
lemma insertAndContractNat_of_isSome (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Option c.uncontracted) (hj : j.isSome) :
|
||||
(insertAndContractNat c i j).1 = Insert.insert {i, i.succAbove (j.get hj)}
|
||||
(Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding c.1) := by
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset]
|
||||
rw [@Option.isSome_iff_exists] at hj
|
||||
|
|
@ -153,12 +154,14 @@ lemma self_mem_uncontracted_of_insertAndContractNat_none (c : WickContraction n)
|
|||
· exact Fin.ne_succAbove i y
|
||||
|
||||
@[simp]
|
||||
lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) : i ∉ (insertAndContractNat c i (some j)).uncontracted := by
|
||||
lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContraction n)
|
||||
(i : Fin n.succ) (j : c.uncontracted) :
|
||||
i ∉ (insertAndContractNat c i (some j)).uncontracted := by
|
||||
rw [mem_uncontracted_iff_not_contracted]
|
||||
simp [insertAndContractNat]
|
||||
|
||||
lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) :
|
||||
lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Fin n) :
|
||||
(i.succAbove j) ∈ (insertAndContractNat c i none).uncontracted ↔ j ∈ c.uncontracted := by
|
||||
rw [mem_uncontracted_iff_not_contracted, mem_uncontracted_iff_not_contracted]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map,
|
||||
|
|
@ -191,8 +194,8 @@ lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n
|
|||
(fun a => hp'.2 (i.succAbove_right_injective a))
|
||||
|
||||
@[simp]
|
||||
lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) :
|
||||
k ∈ (insertAndContractNat c i none).uncontracted ↔
|
||||
lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ)
|
||||
(k : Fin n.succ) : k ∈ (insertAndContractNat c i none).uncontracted ↔
|
||||
k = i ∨ ∃ j, k = i.succAbove j ∧ j ∈ c.uncontracted := by
|
||||
by_cases hi : k = i
|
||||
· subst hi
|
||||
|
|
@ -201,7 +204,8 @@ lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i
|
|||
obtain ⟨z, hk⟩ := hi
|
||||
subst hk
|
||||
have hn : ¬ i.succAbove z = i := Fin.succAbove_ne i z
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat_succAbove_mem_uncontracted_iff, hn, false_or]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat_succAbove_mem_uncontracted_iff, hn,
|
||||
false_or]
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
exact ⟨z, rfl, h⟩
|
||||
|
|
@ -212,7 +216,8 @@ lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i
|
|||
exact hk.2
|
||||
|
||||
lemma insertAndContractNat_none_uncontracted (c : WickContraction n) (i : Fin n.succ) :
|
||||
(insertAndContractNat c i none).uncontracted = Insert.insert i (c.uncontracted.map i.succAboveEmb) := by
|
||||
(insertAndContractNat c i none).uncontracted =
|
||||
Insert.insert i (c.uncontracted.map i.succAboveEmb) := by
|
||||
ext a
|
||||
simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_none_iff, Finset.mem_insert,
|
||||
Finset.mem_map, Fin.succAboveEmb_apply]
|
||||
|
|
@ -255,8 +260,8 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i
|
|||
∃ z, k = i.succAbove z ∧ z ∈ c.uncontracted ∧ z ≠ j := by
|
||||
by_cases hki : k = i
|
||||
· subst hki
|
||||
simp only [Nat.succ_eq_add_one, self_not_mem_uncontracted_of_insertAndContractNat_some, ne_eq, false_iff,
|
||||
not_exists, not_and, Decidable.not_not]
|
||||
simp only [Nat.succ_eq_add_one, self_not_mem_uncontracted_of_insertAndContractNat_some, ne_eq,
|
||||
false_iff, not_exists, not_and, Decidable.not_not]
|
||||
exact fun x hx => False.elim (Fin.ne_succAbove k x hx)
|
||||
· simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hki
|
||||
obtain ⟨z, hk⟩ := hki
|
||||
|
|
@ -279,9 +284,9 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i
|
|||
rw [mem_uncontracted_iff_not_contracted]
|
||||
intro p hp
|
||||
rw [mem_uncontracted_iff_not_contracted] at h
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert,
|
||||
Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton,
|
||||
not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset,
|
||||
Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp,
|
||||
Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
|
||||
have hc := h.2 p hp
|
||||
rw [Finset.mapEmbedding_apply] at hc
|
||||
exact (Finset.mem_map' (i.succAboveEmb)).mpr.mt hc
|
||||
|
|
@ -290,20 +295,22 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i
|
|||
rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz'1
|
||||
subst hz'1
|
||||
rw [mem_uncontracted_iff_not_contracted]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert,
|
||||
Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton,
|
||||
not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset,
|
||||
Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp,
|
||||
Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
|
||||
apply And.intro
|
||||
· rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)]
|
||||
exact And.intro (Fin.succAbove_ne i z) (fun a => hjz a.symm)
|
||||
· rw [mem_uncontracted_iff_not_contracted] at hz'
|
||||
exact fun a ha hc => hz'.1 a ha ((Finset.mem_map' (i.succAboveEmb)).mp hc)
|
||||
|
||||
lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) :
|
||||
(insertAndContractNat c i (some j)).uncontracted = (c.uncontracted.erase j).map i.succAboveEmb := by
|
||||
lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) :
|
||||
(insertAndContractNat c i (some j)).uncontracted =
|
||||
(c.uncontracted.erase j).map i.succAboveEmb := by
|
||||
ext a
|
||||
simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq, Finset.map_erase,
|
||||
Fin.succAboveEmb_apply, Finset.mem_erase, Finset.mem_map]
|
||||
simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq,
|
||||
Finset.map_erase, Fin.succAboveEmb_apply, Finset.mem_erase, Finset.mem_map]
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
obtain ⟨z, h1, h2, h3⟩ := h
|
||||
|
|
@ -338,20 +345,22 @@ lemma insertAndContractNat_none_getDual?_isNone (c : WickContraction n) (i : Fin
|
|||
simp
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) :
|
||||
lemma insertAndContractNat_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Fin n) :
|
||||
(insertAndContractNat c i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none := by
|
||||
have h1 := insertAndContractNat_succAbove_mem_uncontracted_iff c i j
|
||||
simpa [uncontracted] using h1
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) :
|
||||
lemma insertAndContractNat_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Fin n) :
|
||||
((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome ↔ (c.getDual? j).isSome := by
|
||||
rw [← not_iff_not]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ) (j : Fin n)
|
||||
(h : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome) :
|
||||
lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Fin n) (h : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome) :
|
||||
((insertAndContractNat c i none).getDual? (i.succAbove j)).get h =
|
||||
i.succAbove ((c.getDual? j).get (by simpa using h)) := by
|
||||
have h1 : (insertAndContractNat c i none).getDual? (i.succAbove j) = some
|
||||
|
|
@ -366,14 +375,15 @@ lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : F
|
|||
exact Option.get_of_mem h h1
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) :
|
||||
lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) :
|
||||
(insertAndContractNat c i (some j)).getDual? i = some (i.succAbove j) := by
|
||||
rw [getDual?_eq_some_iff_mem]
|
||||
simp [insertAndContractNat]
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_some_getDual?_neq_none (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted)
|
||||
(k : Fin n) (hkj : k ≠ j.1) :
|
||||
lemma insertAndContractNat_some_getDual?_neq_none (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) :
|
||||
(insertAndContractNat c i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
|
|
@ -394,9 +404,10 @@ lemma insertAndContractNat_some_getDual?_neq_none (c : WickContraction n) (i : F
|
|||
simpa [uncontracted, -mem_uncontracted_insertAndContractNat_some_iff, ne_eq] using hk
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_some_getDual?_neq_isSome (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted)
|
||||
(k : Fin n) (hkj : k ≠ j.1) :
|
||||
((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome ↔ (c.getDual? k).isSome := by
|
||||
lemma insertAndContractNat_some_getDual?_neq_isSome (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) :
|
||||
((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome ↔
|
||||
(c.getDual? k).isSome := by
|
||||
rw [← not_iff_not]
|
||||
simp [hkj]
|
||||
|
||||
|
|
@ -409,8 +420,8 @@ lemma insertAndContractNat_some_getDual?_neq_isSome_get (c : WickContraction n)
|
|||
have h1 : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k))
|
||||
= some (i.succAbove ((c.getDual? k).get (by simpa [hkj] using h))) := by
|
||||
rw [getDual?_eq_some_iff_mem]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map,
|
||||
RelEmbedding.coe_toEmbedding]
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert,
|
||||
Finset.mem_map, RelEmbedding.coe_toEmbedding]
|
||||
apply Or.inr
|
||||
use { k, ((c.getDual? k).get (by simpa [hkj] using h))}
|
||||
simp only [self_getDual?_get_mem, true_and]
|
||||
|
|
@ -419,8 +430,8 @@ lemma insertAndContractNat_some_getDual?_neq_isSome_get (c : WickContraction n)
|
|||
exact Option.get_of_mem h h1
|
||||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted)
|
||||
(k : Fin n) (hkj : k ≠ j.1) :
|
||||
lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) :
|
||||
(insertAndContractNat c i (some j)).getDual? (i.succAbove k) =
|
||||
Option.map i.succAbove (c.getDual? k) := by
|
||||
by_cases h : (c.getDual? k).isSome
|
||||
|
|
@ -444,8 +455,8 @@ lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin
|
|||
|
||||
-/
|
||||
@[simp]
|
||||
lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) :
|
||||
erase (insertAndContractNat c i j) i = c := by
|
||||
lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Option c.uncontracted) : erase (insertAndContractNat c i j) i = c := by
|
||||
refine Subtype.eq ?_
|
||||
simp only [erase, Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset]
|
||||
conv_rhs => rw [c.eq_filter_mem_self]
|
||||
|
|
@ -489,12 +500,13 @@ lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ) (j : O
|
|||
simp only [ha, true_and]
|
||||
rw [Finset.mapEmbedding_apply]
|
||||
|
||||
lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) :
|
||||
(insertAndContractNat c i j).getDualErase i =
|
||||
lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Option c.uncontracted) : (insertAndContractNat c i j).getDualErase i =
|
||||
uncontractedCongr (c := c) (c' := (c.insertAndContractNat i j).erase i) (by simp) j := by
|
||||
match n with
|
||||
| 0 =>
|
||||
simp only [insertAndContractNat, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.le_eq_subset, getDualErase]
|
||||
simp only [insertAndContractNat, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.le_eq_subset,
|
||||
getDualErase]
|
||||
fin_cases j
|
||||
simp
|
||||
| Nat.succ n =>
|
||||
|
|
@ -503,8 +515,9 @@ lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ)
|
|||
have hi := insertAndContractNat_none_getDual?_isNone c i
|
||||
simp [getDualErase, hi]
|
||||
| some j =>
|
||||
simp only [Nat.succ_eq_add_one, getDualErase, insertAndContractNat_some_getDual?_eq, Option.isSome_some,
|
||||
↓reduceDIte, Option.get_some, predAboveI_succAbove, uncontractedCongr_some, Option.some.injEq]
|
||||
simp only [Nat.succ_eq_add_one, getDualErase, insertAndContractNat_some_getDual?_eq,
|
||||
Option.isSome_some, ↓reduceDIte, Option.get_some, predAboveI_succAbove,
|
||||
uncontractedCongr_some, Option.some.injEq]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
|
|
@ -513,7 +526,8 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) :
|
|||
match n with
|
||||
| 0 =>
|
||||
apply Subtype.eq
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insertAndContractNat, getDualErase, Finset.le_eq_subset]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insertAndContractNat, getDualErase,
|
||||
Finset.le_eq_subset]
|
||||
ext a
|
||||
simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding]
|
||||
apply Iff.intro
|
||||
|
|
@ -565,8 +579,8 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) :
|
|||
rfl
|
||||
simp only [Nat.succ_eq_add_one, ne_eq, self_neq_getDual?_get, not_false_eq_true]
|
||||
exact (getDualErase_isSome_iff_getDual?_isSome c i).mpr hi
|
||||
· simp only [Nat.succ_eq_add_one, insertAndContractNat, getDualErase, hi, Bool.false_eq_true, ↓reduceDIte,
|
||||
Finset.le_eq_subset]
|
||||
· simp only [Nat.succ_eq_add_one, insertAndContractNat, getDualErase, hi, Bool.false_eq_true,
|
||||
↓reduceDIte, Finset.le_eq_subset]
|
||||
ext a
|
||||
simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding]
|
||||
apply Iff.intro
|
||||
|
|
@ -626,7 +640,8 @@ lemma insertLift_none_bijective {c : WickContraction n} (i : Fin n.succ) :
|
|||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) =
|
||||
(j : Option (c.uncontracted)) (a : c.1) :
|
||||
(c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) =
|
||||
i.succAbove (c.fstFieldOfContract a) := by
|
||||
refine (c.insertAndContractNat i j).eq_fstFieldOfContract_of_mem (a := (insertLift i j a))
|
||||
(i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_
|
||||
|
|
@ -641,7 +656,8 @@ lemma insertAndContractNat_fstFieldOfContract (c : WickContraction n) (i : Fin n
|
|||
|
||||
@[simp]
|
||||
lemma insertAndContractNat_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ)
|
||||
(j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) =
|
||||
(j : Option (c.uncontracted)) (a : c.1) :
|
||||
(c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) =
|
||||
i.succAbove (c.sndFieldOfContract a) := by
|
||||
refine (c.insertAndContractNat i j).eq_sndFieldOfContract_of_mem (a := (insertLift i j a))
|
||||
(i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_
|
||||
|
|
@ -701,8 +717,8 @@ lemma insertLiftSome_surjective {c : WickContraction n} (i : Fin n.succ) (j : c.
|
|||
Function.Surjective (insertLiftSome i j) := by
|
||||
intro a
|
||||
have ha := a.2
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map,
|
||||
RelEmbedding.coe_toEmbedding] at ha
|
||||
simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert,
|
||||
Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha
|
||||
rcases ha with ha | ha
|
||||
· use Sum.inl ()
|
||||
exact Subtype.eq ha.symm
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue