Skip to content

Commit 3079fa6

Browse files
wkrozowskiwkrozowski
committed
Further cleanup
1 parent ea94efb commit 3079fa6

File tree

6 files changed

+33
-41
lines changed

6 files changed

+33
-41
lines changed

‎src/Std/Data/DHashMap/Lemmas.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1847,8 +1847,8 @@ theorem Equiv.beq [∀ k, ReflBEq (β k)] (h : m₁ ~m m₂) : m₁ == m₂ :=
18471847
theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h : m₁ == m₂) : m₁ ~m m₂ :=
18481848
⟨Raw₀.equiv_of_beq m₁.2 m₂.2 h⟩
18491849

1850-
theorem Equiv.beq_congr {m₃ m₄ : DHashMap α β} : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) :=
1851-
fun h1 h2 => Raw₀.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 h1.1 h2.1
1850+
theorem Equiv.beq_congr {m₃ m₄ : DHashMap α β} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
1851+
Raw₀.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1
18521852

18531853
end BEq
18541854

@@ -1861,8 +1861,8 @@ theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [ReflBEq β] (h : m₁
18611861
theorem Const.equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : Const.beq m₁ m₂) : m₁ ~m m₂ :=
18621862
⟨Raw₀.Const.equiv_of_beq m₁.2 m₂.2 h⟩
18631863

1864-
theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : DHashMap α (fun _ => β)} : m₁ ~m m₃ → m₂ ~m m₄ → Const.beq m₁ m₂ = Const.beq m₃ m₄ :=
1865-
fun h1 h2 => Raw₀.Const.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 h1.1 h2.1
1864+
theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : DHashMap α (fun _ => β)} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Const.beq m₁ m₂ = Const.beq m₃ m₄ :=
1865+
Raw₀.Const.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1
18661866

18671867
end
18681868

‎src/Std/Data/DHashMap/RawLemmas.lean‎

Lines changed: 13 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3762,39 +3762,32 @@ open Internal.Raw Internal.Raw₀
37623762
section BEq
37633763
variable {m₁ m₂ : Raw α β} [LawfulBEq α] [∀ k, BEq (β k)]
37643764

3765-
theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → m₁ == m₂ := by
3765+
theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ := by
37663766
simp only [BEq.beq]
3767-
simp_to_raw
3768-
intro h
3769-
exact Raw₀.Equiv.beq h₁ h₂ h
3767+
simp_to_raw using Raw₀.Equiv.beq
37703768

3771-
theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := by
3769+
theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true) : m₁ ~m m₂ := by
3770+
revert h
37723771
simp_to_raw using Raw₀.equiv_of_beq
37733772

3774-
theorem Equiv.beq_congr {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
3775-
m₁ ~m m₃ → m₂ ~m m₄ → Raw.beq m₁ m₂ = Raw.beq m₃ m₄ := by
3776-
simp_to_raw
3777-
intro w1 w2
3778-
exact Raw₀.Equiv.beq_congr h₁ h₂ h₃ h₄ w1 w2
3773+
theorem Equiv.beq_congr {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Raw.beq m₁ m₂ = Raw.beq m₃ m₄ := by
3774+
simp_to_raw using Raw₀.Equiv.beq_congr
37793775

37803776
end BEq
37813777

37823778
section
3779+
37833780
variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β)}
37843781

3785-
theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → beq m₁ m₂ := by
3786-
simp_to_raw
3787-
intro h
3788-
exact Raw₀.Const.Equiv.beq h₁ h₂ h
3782+
theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := by
3783+
simp_to_raw using Raw₀.Const.Equiv.beq
37893784

3790-
theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := by
3785+
theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true ) : m₁ ~m m₂ := by
3786+
revert h
37913787
simp_to_raw using Raw₀.Const.equiv_of_beq
37923788

3793-
theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
3794-
m₁ ~m m₃ → m₂ ~m m₄ → Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ := by
3795-
simp_to_raw
3796-
intro w1 w2
3797-
exact Raw₀.Const.Equiv.beq_congr h₁ h₂ h₃ h₄ w1 w2
3789+
theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ := by
3790+
simp_to_raw using Raw₀.Const.Equiv.beq_congr
37983791

37993792
end
38003793

‎src/Std/Data/HashMap/Lemmas.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1355,8 +1355,8 @@ theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [ReflBEq β] (h : m₁ ~m m
13551355
theorem equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : m₁ == m₂) : m₁ ~m m₂ :=
13561356
⟨DHashMap.Const.equiv_of_beq h⟩
13571357

1358-
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashMap α β} : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) := fun h1 h2 =>
1359-
DHashMap.Const.Equiv.beq_congr h1.1 h2.1
1358+
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashMap α β} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
1359+
DHashMap.Const.Equiv.beq_congr w₁.1 w₂.1
13601360

13611361
end
13621362

‎src/Std/Data/HashMap/RawLemmas.lean‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1311,15 +1311,14 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W
13111311
section
13121312
variable {β : Type v} {m₁ m₂ : Raw α β}
13131313

1314-
theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → m₁ == m₂ :=
1315-
fun hyp => DHashMap.Raw.Const.Equiv.beq h₁.1 h₂.1 hyp.1
1314+
theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ :=
1315+
DHashMap.Raw.Const.Equiv.beq h₁.1 h₂.1 h.1
13161316

1317-
theorem equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ == m₂ → m₁ ~m m₂ :=
1318-
fun hyp => ⟨DHashMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 hyp⟩
1317+
theorem equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ :=
1318+
⟨DHashMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 h⟩
13191319

1320-
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) :
1321-
m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) :=
1322-
fun hyp1 hyp2 => DHashMap.Raw.Const.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
1320+
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
1321+
DHashMap.Raw.Const.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1
13231322

13241323
end
13251324

‎src/Std/Data/HashSet/Lemmas.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -791,8 +791,8 @@ theorem Equiv.beq [EquivBEq α] [LawfulHashable α] (h : m₁ ~m m₂) : m₁ ==
791791
theorem equiv_of_beq [LawfulBEq α] (h : m₁ == m₂) : m₁ ~m m₂ :=
792792
⟨HashMap.equiv_of_beq h⟩
793793

794-
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashSet α} : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) :=
795-
fun h1 h2 => HashMap.Equiv.beq_congr h1.1 h2.1
794+
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashSet α} (h₁ : m₁ ~m m₃) (h₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
795+
HashMap.Equiv.beq_congr h₁.1 h₂.1
796796

797797
end
798798

‎src/Std/Data/HashSet/RawLemmas.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -817,14 +817,14 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W
817817
section
818818
variable {m₁ m₂ : Raw α}
819819

820-
theorem Equiv.beq [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → beq m₁ m₂ :=
821-
fun hyp => HashMap.Raw.Equiv.beq h₁.1 h₂.1 hyp.1
820+
theorem Equiv.beq [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ :=
821+
HashMap.Raw.Equiv.beq h₁.1 h₂.1 h.1
822822

823-
theorem equiv_of_beq [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ == m₂ → m₁ ~m m₂ :=
824-
fun hyp => ⟨HashMap.Raw.equiv_of_beq h₁.1 h₂.1 hyp⟩
823+
theorem equiv_of_beq [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ :=
824+
⟨HashMap.Raw.equiv_of_beq h₁.1 h₂.1 h⟩
825825

826-
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) : m₁ ~m m₃ → m₂ ~m m₄ → (m₁ == m₂) = (m₃ == m₄) :=
827-
fun hyp1 hyp2 => HashMap.Raw.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 hyp1.1 hyp2.1
826+
theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) :=
827+
HashMap.Raw.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1
828828

829829
end
830830

0 commit comments

Comments
 (0)