From 3e385c3cac6b4df0a97961e6f2473a59efdb4ec1 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 17 Jan 2024 20:03:10 +0000 Subject: [PATCH] Bump mathlib Signed-off-by: zeramorphic --- ConNF/Counting/Spec.lean | 2 +- ConNF/Counting/StrongSupport.lean | 2 +- ConNF/FOA/Action/FillAtomRange.lean | 8 +++---- ConNF/FOA/Action/NearLitterAction.lean | 2 +- ConNF/FOA/Basic/Constrains.lean | 10 ++++----- ConNF/FOA/Basic/Flexible.lean | 2 +- ConNF/FOA/Properties/Injective.lean | 6 +++--- ConNF/NewTangle/Cloud.lean | 8 +++---- ConNF/NewTangle/CodeEquiv.lean | 30 +++++++++++++------------- ConNF/NewTangle/NewAllowable.lean | 4 ++-- ConNF/NewTangle/NewTangle.lean | 4 ++-- lake-manifest.json | 23 ++++++++++++++------ 12 files changed, 55 insertions(+), 46 deletions(-) diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean index c57094a638..9af6762136 100644 --- a/ConNF/Counting/Spec.lean +++ b/ConNF/Counting/Spec.lean @@ -529,7 +529,7 @@ theorem specifies_iff (σ : Spec β) (S : Support β) : σ.Specifies S ↔ σ.max = S.max ∧ ∀ (i : κ) (hσ : i < σ.max) (hS : i < S.max), SpecifiesCondition S (σ.f i hσ) (S.f i hS) := by - rw [Specifies, Specifies'_iff] + rw [Specifies, specifies'_iff] rfl theorem Specifies.max_eq_max {σ : Spec β} {S : Support β} (h : σ.Specifies S) : diff --git a/ConNF/Counting/StrongSupport.lean b/ConNF/Counting/StrongSupport.lean index 53ba7bae3d..bf01bda9b9 100644 --- a/ConNF/Counting/StrongSupport.lean +++ b/ConNF/Counting/StrongSupport.lean @@ -191,7 +191,7 @@ def bannedLitters (T : Support β) (A : ExtendedIndex β) : Set Litter := theorem bannedLitter_iff_mem_bannedLitters (T : Support β) (A : ExtendedIndex β) (L : Litter) : BannedLitter T A L ↔ L ∈ bannedLitters T A := by - simp only [BannedLitter_iff, bannedLitters, + simp only [bannedLitter_iff, bannedLitters, mem_union, mem_iUnion, Set.mem_singleton_iff, exists_prop] constructor · rintro (h | ⟨a, N, ha, hN, rfl⟩) diff --git a/ConNF/FOA/Action/FillAtomRange.lean b/ConNF/FOA/Action/FillAtomRange.lean index 6a9009779f..5f1819b980 100644 --- a/ConNF/FOA/Action/FillAtomRange.lean +++ b/ConNF/FOA/Action/FillAtomRange.lean @@ -36,7 +36,7 @@ structure WithoutPreimage (a : Atom) : Prop where not_mem_ran : a ∉ φ.atomMap.ran theorem withoutPreimage_small : Small {a | φ.WithoutPreimage a} := by - simp only [WithoutPreimage_iff, setOf_and] + simp only [withoutPreimage_iff, setOf_and] rw [← inter_assoc] refine' Small.mono (inter_subset_left _ _) _ suffices @@ -90,7 +90,7 @@ structure MappedOutside (L : Litter) (hL : (φ.litterMap L).Dom) (a : Atom) : Pr and that are not already in the domain. -/ theorem mappedOutside_small (L : Litter) (hL : (φ.litterMap L).Dom) : Small {a | φ.MappedOutside L hL a} := by - simp only [MappedOutside_iff, setOf_and] + simp only [mappedOutside_iff, setOf_and] rw [← inter_assoc] refine' Small.mono (inter_subset_left _ _) _ refine' Small.mono _ ((φ.litterMap L).get hL).2.prop @@ -203,7 +203,7 @@ theorem supportedAction_eq_of_mem_preimageLitterSubset {a : Atom} rw [Or.elim'_right, Or.elim'_left] intro h' have := φ.preimageLitter_not_banned - rw [BannedLitter_iff] at this + rw [bannedLitter_iff] at this push_neg at this exact this.1 a h' (φ.preimageLitterSubset_subset ha).symm @@ -225,7 +225,7 @@ theorem supportedAction_eq_of_mem_mappedOutsideSubset {a : Atom} (φ.preimageLitterSubset_subset h) cases this have := φ.preimageLitter_not_banned - rw [BannedLitter_iff] at this + rw [bannedLitter_iff] at this push_neg at this cases this.2.1 hL · exact ((mappedOutsideSubset_spec _ _ hL).1 ha).2 diff --git a/ConNF/FOA/Action/NearLitterAction.lean b/ConNF/FOA/Action/NearLitterAction.lean index 2f6574be8f..de2ece420e 100644 --- a/ConNF/FOA/Action/NearLitterAction.lean +++ b/ConNF/FOA/Action/NearLitterAction.lean @@ -74,7 +74,7 @@ theorem BannedLitter.memMap (a : Atom) (L : Litter) (hL) /-- There are only a small amount of banned litters. -/ theorem bannedLitter_small : Small {L | φ.BannedLitter L} := by - simp only [BannedLitter_iff, mem_diff, SetLike.mem_coe, mem_litterSet] + simp only [bannedLitter_iff, mem_diff, SetLike.mem_coe, mem_litterSet] refine' Small.union _ (Small.union _ (Small.union _ (Small.union _ _))) · refine' lt_of_le_of_lt _ φ.atomMap_dom_small refine' ⟨⟨fun a => ⟨_, a.prop.choose_spec.1⟩, fun a₁ a₂ h => _⟩⟩ diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index c8f605d6a2..ed52c4c68b 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -74,7 +74,7 @@ inductive HasPosition : Litter → μ → Prop theorem hasPosition_subsingleton {L : Litter} {ν₁ ν₂ : μ} (h₁ : HasPosition L ν₁) (h₂ : HasPosition L ν₂) : ν₁ = ν₂ := by - rw [HasPosition_iff] at h₁ h₂ + rw [hasPosition_iff] at h₁ h₂ cases h₁ with | inl h₁ => obtain ⟨δ, _, ε, _, hδε, t, rfl, rfl⟩ := h₁ @@ -110,7 +110,7 @@ theorem hasPosition_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrai theorem hasPosition_lt_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrains L₁ L₂) {ν₁ ν₂ : μ} (h₁ : HasPosition L₁ ν₁) (h₂ : HasPosition L₂ ν₂) : ν₁ < ν₂ := by - rw [HasPosition_iff] at h₁ h₂ + rw [hasPosition_iff] at h₁ h₂ cases h with | fuzz_atom hδε t ht => cases h₂ with @@ -198,7 +198,7 @@ theorem constrains_nearLitter {c : SupportCondition β} {A : ExtendedIndex β} ∃ a ∈ litterSet N.fst ∆ N.snd, c = ⟨A, inl a⟩ := by constructor · intro h - rw [Constrains_iff] at h + rw [constrains_iff] at h obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ | ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, _, rfl, hc'⟩ | ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := h @@ -258,7 +258,7 @@ theorem constrains_wf (β : Λ) : WellFounded ((· ≺ ·) : SupportCondition β intro L ih A constructor intro c hc - rw [Constrains_iff] at hc + rw [constrains_iff] at hc obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ | ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, hc, rfl, hc'⟩ | ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := hc @@ -374,7 +374,7 @@ theorem lt_nearLitter' {β : Λ} {N : NearLitter} {B : ExtendedIndex β} theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺ c} := by obtain ⟨A, a | N⟩ := c · simp only [constrains_atom, setOf_eq_eq_singleton, small_singleton] - simp_rw [Constrains_iff] + simp_rw [constrains_iff] refine Small.union ?_ (Small.union ?_ (Small.union ?_ (Small.union ?_ ?_))) <;> rw [small_setOf] · change Small {c | ∃ b B, _ ∧ _ = _} diff --git a/ConNF/FOA/Basic/Flexible.lean b/ConNF/FOA/Basic/Flexible.lean index 61df4dbb7d..aaaae057f1 100644 --- a/ConNF/FOA/Basic/Flexible.lean +++ b/ConNF/FOA/Basic/Flexible.lean @@ -50,7 +50,7 @@ theorem mk_flexible (A : ExtendedIndex β) : #{L | Flexible A L} = #μ := by refine le_antisymm ((Cardinal.mk_subtype_le _).trans mk_litter.le) ?_ refine ⟨⟨fun ν => ⟨⟨ν, ⊥, α, bot_ne_coe⟩, ?_⟩, ?_⟩⟩ · intro h - rw [Inflexible_iff] at h + rw [inflexible_iff] at h obtain ⟨γ, _, δ, _, ε, _, _, hε, hδε, A, t, rfl, h⟩ | ⟨γ, _, ε, _, hε, A, t, rfl, h⟩ := h all_goals apply_fun Litter.γ at h diff --git a/ConNF/FOA/Properties/Injective.lean b/ConNF/FOA/Properties/Injective.lean index 9d174863d2..1b48c8854c 100644 --- a/ConNF/FOA/Properties/Injective.lean +++ b/ConNF/FOA/Properties/Injective.lean @@ -23,7 +23,7 @@ theorem atom_injective_extends {c d : SupportCondition β} (hcd : (ihsAction π exact (π A).atomPerm.injOn ha hb h · rw [completeAtomMap_eq_of_mem_domain ha, completeAtomMap_eq_of_not_mem_domain hb] at h cases - (π A).not_mem_domain_of_mem_largestSublitter (Subtype.coe_eq_iff.mp h.symm).choose + (π A).notr_mem_domain_of_mem_largestSublitter (Subtype.coe_eq_iff.mp h.symm).choose ((π A).atomPerm.map_domain ha) · rw [completeAtomMap_eq_of_not_mem_domain ha, completeAtomMap_eq_of_mem_domain hb] at h cases @@ -286,7 +286,7 @@ theorem constrainedAction_comp_mapFlexible (hπf : π.Free) {γ : Λ} {s : Set ( obtain ⟨⟨δ, ε, hε, C, hC⟩, a, rfl⟩ := hL₃ contrapose hL₂ rw [not_flexible_iff] at hL₂ ⊢ - rw [Inflexible_iff] at hL₂ + rw [inflexible_iff] at hL₂ obtain ⟨δ', _, ε', _, ζ', _, _, hζ', hεζ', C', t', rfl, h'⟩ | ⟨δ', _, ε', _, hε', C', a', rfl, h'⟩ := hL₂ · have := congr_arg Litter.β h' @@ -303,7 +303,7 @@ theorem constrainedAction_comp_mapFlexible (hπf : π.Free) {γ : Λ} {s : Set ( obtain ⟨⟨δ, ε, ζ, hε, hζ, hεζ, C, hC⟩, t, rfl⟩ := hL₃ contrapose hL₂ rw [not_flexible_iff] at hL₂ ⊢ - rw [Inflexible_iff] at hL₂ + rw [inflexible_iff] at hL₂ obtain ⟨δ', _, ε', _, ζ', _, hε', hζ', hεζ', C', t', rfl, h'⟩ | ⟨δ', _, ε', _, hε', C', a', rfl, h'⟩ := hL₂ · rw [Path.comp_cons, Path.comp_cons] at hC diff --git a/ConNF/NewTangle/Cloud.lean b/ConNF/NewTangle/Cloud.lean index c53d4fc99b..e61788d96e 100644 --- a/ConNF/NewTangle/Cloud.lean +++ b/ConNF/NewTangle/Cloud.lean @@ -270,7 +270,7 @@ infixl:62 " ↝₀ " => CloudRel theorem cloudRel_subsingleton (hc : c.members.Nonempty) : {d : Code | d ↝₀ c}.Subsingleton := by intro d hd e he - simp only [CloudRel_iff] at hd he + simp only [cloudRel_iff] at hd he obtain ⟨β, hβ, hdβ, rfl⟩ := hd obtain ⟨γ, hγ, heγ, h⟩ := he have := ((Code.ext_iff _ _).1 h).1 @@ -292,7 +292,7 @@ theorem CloudRel.nonempty_iff : c ↝₀ d → (c.members.Nonempty ↔ d.members exact cloudCode_nonempty.symm theorem cloudRelEmptyEmpty (hγβ : γ ≠ β) : mk γ ∅ ↝₀ mk β ∅ := - (CloudRel_iff _ _).2 + (cloudRel_iff _ _).2 ⟨β, inferInstance, hγβ, by ext : 1 · rfl @@ -317,7 +317,7 @@ infixl:62 " ↝ " => CloudRel' @[simp] theorem cloudRel_coe_coe {c d : NonemptyCode} : (c : Code) ↝₀ d ↔ c ↝ d := by - rw [CloudRel_iff, CloudRel'_iff] + rw [cloudRel_iff, cloudRel'_iff] aesop theorem cloud_subrelation : Subrelation (· ↝ ·) (InvImage (· < ·) (codeMinMap : NonemptyCode → μ)) @@ -335,7 +335,7 @@ only one code which is related (on the left) to any given code under the `cloud` theorem cloudRel'_subsingleton (c : NonemptyCode) : {d : NonemptyCode | d ↝ c}.Subsingleton := by intro d hd e he - simp only [Ne.def, CloudRel'_iff, mem_setOf_eq] at hd he + simp only [Ne.def, cloudRel'_iff, mem_setOf_eq] at hd he obtain ⟨β, hβ, hdβ, rfl⟩ := hd obtain ⟨γ, hγ, heγ, h⟩ := he rw [Subtype.ext_iff] at h diff --git a/ConNF/NewTangle/CodeEquiv.lean b/ConNF/NewTangle/CodeEquiv.lean index 85523abe8f..74f728f505 100644 --- a/ConNF/NewTangle/CodeEquiv.lean +++ b/ConNF/NewTangle/CodeEquiv.lean @@ -66,7 +66,7 @@ mutual end theorem isEven_of_forall_not (h : ∀ d, ¬d ↝₀ c) : IsEven c := - (IsEven_iff c).2 fun _ hd => (h _ hd).elim + (isEven_iff c).2 fun _ hd => (h _ hd).elim @[simp] theorem isEven_of_eq_bot (c : Code) (hc : c.1 = ⊥) : c.IsEven := @@ -77,7 +77,7 @@ theorem isEven_bot (s : Set Atom) : IsEven (mk ⊥ s : Code) := isEven_of_eq_bot _ rfl theorem not_isOdd_bot (s : Set Atom) : ¬IsOdd (mk ⊥ s : Code) := by - simp_rw [IsOdd_iff, CloudRel_iff] + simp_rw [isOdd_iff, cloudRel_iff] rintro ⟨d, ⟨γ, _, h⟩, _⟩ exact bot_ne_coe (congr_arg Code.β h.2) @@ -90,7 +90,7 @@ theorem IsEmpty.isEven_iff (hc : c.IsEmpty) : IsEven c ↔ (c.1 : TypeIndex) = · rfl · simp [Code.IsEmpty] at hc cases hc - have := not_isOdd_bot ∅ ((IsEven_iff _).1 h ⟨⊥, ∅⟩ ?_) + have := not_isOdd_bot ∅ ((isEven_iff _).1 h ⟨⊥, ∅⟩ ?_) · cases this convert CloudRel.intro β _ · aesop @@ -99,11 +99,11 @@ theorem IsEmpty.isEven_iff (hc : c.IsEmpty) : IsEven c ↔ (c.1 : TypeIndex) = @[simp] theorem IsEmpty.isOdd_iff (hc : c.IsEmpty) : IsOdd c ↔ (c.1 : TypeIndex) ≠ ⊥ := by obtain ⟨β, s⟩ := c - refine' ⟨_, fun h => (IsOdd_iff _).2 ⟨mk ⊥ ∅, _, isEven_bot _⟩⟩ + refine' ⟨_, fun h => (isOdd_iff _).2 ⟨mk ⊥ ∅, _, isEven_bot _⟩⟩ · rintro h (rfl : β = _) exact not_isOdd_bot _ h · lift β to Λ using h - refine (CloudRel_iff _ _).2 ⟨β, inferInstance, ?_⟩ + refine (cloudRel_iff _ _).2 ⟨β, inferInstance, ?_⟩ simp only [ne_eq, bot_ne_coe, not_false_eq_true, cloudCode_mk_ne, cloud_empty, mk.injEq, heq_eq_eq, true_and] exact hc @@ -118,7 +118,7 @@ theorem isOdd_empty_iff : IsOdd (mk β ∅) ↔ (β : TypeIndex) ≠ ⊥ := private theorem not_isOdd_nonempty : ∀ c : NonemptyCode, ¬c.1.IsOdd ↔ c.1.IsEven | c => by - rw [IsOdd_iff, IsEven_iff] + rw [isOdd_iff, isEven_iff] push_neg apply forall_congr' _ intro d @@ -153,14 +153,14 @@ theorem isEven_or_isOdd (c : Code) : c.IsEven ∨ c.IsOdd := by exact em _ protected theorem _root_.ConNF.CloudRel.isOdd (hc : c.IsEven) (h : c ↝₀ d) : d.IsOdd := - (IsOdd_iff d).2 ⟨_, h, hc⟩ + (isOdd_iff d).2 ⟨_, h, hc⟩ protected theorem IsEven.cloudCode (hc : c.IsEven) (hcγ : c.1 ≠ γ) : (cloudCode γ c).IsOdd := (CloudRel.intro _ hcγ).isOdd hc protected theorem IsOdd.cloudCode (hc : c.IsOdd) (hc' : c.members.Nonempty) (hcγ : c.1 ≠ γ) : (cloudCode γ c).IsEven := - (IsEven_iff _).2 fun d hd => by rwa [(cloudRel_cloudCode _ hc' hcγ).1 hd] + (isEven_iff _).2 fun d hd => by rwa [(cloudRel_cloudCode _ hc' hcγ).1 hd] protected theorem IsEven.cloudCode_ne (hc : c.IsEven) (hd : d.IsEven) (hcγ : c.1 ≠ γ) : cloudCode γ c ≠ d := by rintro rfl; exact hd.not_isOdd (hc.cloudCode hcγ) @@ -185,7 +185,7 @@ theorem cloudCode_ne_singleton {t} (hcβ : c.1 ≠ β) : cloudCode γ c ≠ mk @[simp] theorem isEven_singleton (t) : (mk β {t}).IsEven := by refine' isEven_of_forall_not fun c hc => _ - obtain ⟨γ, _, h⟩ := (CloudRel_iff _ _).1 hc + obtain ⟨γ, _, h⟩ := (cloudRel_iff _ _).1 hc have := congr_arg Code.β h.2 cases this exact cloudCode_ne_singleton h.1 h.2.symm @@ -251,9 +251,9 @@ protected theorem _root_.ConNF.Code.IsEmpty.equiv (hc : c.IsEmpty) (hd : d.IsEmp /-- Code equivalence is transitive. -/ theorem trans {c d e : Code} : c ≡ d → d ≡ e → c ≡ e := by - rw [Equiv_iff, Equiv_iff] + rw [equiv_iff, equiv_iff] rintro (rfl | ⟨hc, β, _, hcβ, rfl⟩ | ⟨hc, β, _, hcβ, rfl⟩ | ⟨d, hd, γ, _, hdγ, ε, _, hdε, rfl, rfl⟩) - · exact (Equiv_iff _ _).2 + · exact (equiv_iff _ _).2 · rintro (rfl | ⟨hc', γ, _, hcγ, rfl⟩ | ⟨-, γ, _, hcγ, rfl⟩ | ⟨_, hc', γ, _, hcγ, ε, _, _, rfl, rfl⟩) · exact cloud_left _ hc β hcβ · cases (hc'.cloudCode hcγ).not_isEven hc @@ -310,13 +310,13 @@ theorem ext : ∀ {c d : Code}, c ≡ d → c.1 = d.1 → c = d @[simp] theorem bot_left_iff {s} : mk ⊥ s ≡ c ↔ mk ⊥ s = c ∨ ∃ β : Λ, ∃ _ : LtLevel β, c = mk β (cloud bot_ne_coe s) := by - simp [Equiv_iff, cloudCode_ne_bot.symm] + simp [equiv_iff, cloudCode_ne_bot.symm] rw [eq_comm] @[simp] theorem bot_right_iff {s} : c ≡ mk ⊥ s ↔ c = mk ⊥ s ∨ ∃ β : Λ, ∃ _ : LtLevel β, c = mk β (cloud bot_ne_coe s) := by - simp [Equiv_iff, cloudCode_ne_bot.symm] + simp [equiv_iff, cloudCode_ne_bot.symm] rw [eq_comm] @[simp] @@ -341,7 +341,7 @@ theorem singleton_iff {g} : (c.1 : TypeIndex) = (γ : Λ) ∧ β ≠ γ ∧ c = cloudCode γ (mk β {g}) := by classical refine ⟨fun h => ?_, ?_⟩ - · rw [Equiv_iff] at h + · rw [equiv_iff] at h simp only [isEven_singleton, ne_eq, exists_and_left, true_and] at h obtain rfl | ⟨γ, hβγ, _, _, rfl⟩ | ⟨_, γ, γne, _, h⟩ | ⟨d, -, γ, _, _, δ, δne, _, _, h⟩ := h @@ -382,7 +382,7 @@ theorem exists_even_equiv : ∀ c : Code, ∃ d : Code, d ≡ c ∧ d.IsEven := · exact ⟨_, Equiv.empty_empty _ _, isEven_bot _⟩ obtain heven | hodd := isEven_or_isOdd ⟨β, s⟩ · exact ⟨_, Equiv.rfl, heven⟩ - simp_rw [IsOdd_iff, CloudRel_iff] at hodd + simp_rw [isOdd_iff, cloudRel_iff] at hodd obtain ⟨d, ⟨γ, _, hdγ, hc⟩, hd⟩ := id hodd exact ⟨d, (Equiv.cloud_right _ hd _ hdγ).trans (Equiv.of_eq hc.symm), hd⟩ diff --git a/ConNF/NewTangle/NewAllowable.lean b/ConNF/NewTangle/NewAllowable.lean index d8de43e894..394151ca2c 100644 --- a/ConNF/NewTangle/NewAllowable.lean +++ b/ConNF/NewTangle/NewAllowable.lean @@ -392,7 +392,7 @@ end NewAllowable theorem CloudRel.smul : c ↝₀ d → ρ • c ↝₀ ρ • d := by rintro ⟨γ, hγ⟩ - exact (CloudRel_iff _ _).2 ⟨_, inferInstance, hγ, ρ.smul_cloudCode hγ⟩ + exact (cloudRel_iff _ _).2 ⟨_, inferInstance, hγ, ρ.smul_cloudCode hγ⟩ @[simp] theorem smul_cloudRel : ρ • c ↝₀ ρ • d ↔ c ↝₀ d := by @@ -404,7 +404,7 @@ namespace Code theorem isEven_smul_nonempty : ∀ c : NonemptyCode, (ρ • c.val).IsEven ↔ c.val.IsEven | ⟨c, hc⟩ => by - simp_rw [Code.IsEven_iff] + simp_rw [Code.isEven_iff] constructor <;> intro h d hd · have := hd.nonempty_iff.2 hc have _ : ⟨d, this⟩ ↝ ⟨c, hc⟩ := cloudRel_coe_coe.1 hd diff --git a/ConNF/NewTangle/NewTangle.lean b/ConNF/NewTangle/NewTangle.lean index 962082b709..9004f24f20 100644 --- a/ConNF/NewTangle/NewTangle.lean +++ b/ConNF/NewTangle/NewTangle.lean @@ -164,7 +164,7 @@ theorem ext_code : ∀ {t₁ t₂ : Semitangle}, reprCode t₁ ≡ reprCode t₂ cases even₁.not_isOdd ((isEven_bot _).cloudCode bot_ne_coe) | ⟨e₁, Preference.proper γ even₁ hA₁⟩, ⟨e₂, Preference.proper δ even₂ hA₂⟩, h => by dsimp at h - simp only [Equiv_iff, WithBot.coe_ne_bot, ne_eq, Subtype.mk.injEq, coe_inj, Subtype.coe_inj, + simp only [equiv_iff, WithBot.coe_ne_bot, ne_eq, Subtype.mk.injEq, coe_inj, Subtype.coe_inj, Subtype.exists, mem_Iio] at h obtain h | ⟨_, γ, _, hδγ, h⟩ | ⟨_, δ, _, hγδ, h⟩ | ⟨c, hc, γ, hcγ, hc', δ, hcδ, h⟩ := h @@ -467,7 +467,7 @@ def newTypedNearLitter (N : NearLitter) : NewTangle := congr 1 simp only [Support.singleton_enum, Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left, NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr, - Sum.inr.injEq] at h + Sum.inr.injEq] at h apply_fun SetLike.coe at h refine Eq.trans ?_ h rw [NearLitterPerm.smul_nearLitter_coe] diff --git a/lake-manifest.json b/lake-manifest.json index ea3fe4c597..38279feff4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "ee49cf8fada1bf5a15592c399a925c401848227f", + "rev": "1d85fd7db28700b28043d6370dd1ebc426de4d5d", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c", + "rev": "1c88406514a636d241903e2e288d21dc6d861e01", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a", + "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f", + "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.24", + "inputRev": "v0.0.25", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -46,10 +46,19 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph.git", + "type": "git", + "subDir": null, + "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "dd0886f429862c93eec21ba4740b222a96f4f23d", + "rev": "1dfae4b262932b0e74ebd9f36214546e38543ba6", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1", + "rev": "b7fad51b87a5f8fb3a238dc820ec40ebfa2a636e", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main",