Zulip Chat Archive

Stream: mathlib4

Topic: Analysis.Analytic.Composition !4#4572

Scott Morrison (Jun 13 2023 at 12:21):

If anyone is feeling enthusiastic about wrangling congr, there is a nasty case of not being able to reproduce the behaviour of congr from a mathlib3 proof in this PR. !4#4572

Scott Morrison (Jun 13 2023 at 12:21):

It is now the last sorry in this file.

Scott Morrison (Jun 13 2023 at 12:22):

(Well, I turned the second last sorry into a maxHeartbeats 700000, so perhaps that still counts as a second sorry.)

Johan Commelin (Jun 13 2023 at 12:22):

I'll give it a shot

Mauricio Collares (Jun 13 2023 at 13:35):

@Johan Commelin Sorry for missing your message, but I think I have it working. Do you mind if I push it?

Mauricio Collares (Jun 13 2023 at 13:38):

Ah, just realised you pushed a wip too, so I won't push mine. Here's the diff wrt 22dd58d instead, if it's useful (in particular, feel free to push it, as I won't have Internet access until tomorrow).

diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index e0c3e4b0d..6a411cd14 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -1166,19 +1166,23 @@ def sigmaEquivSigmaPi (n : ℕ) :
       simp [map_ofFn, (· ∘ ·), Composition.blocks_sum, Composition.ofFn_blocksFun]
     rw [sigma_pi_composition_eq_iff]
     dsimp
-    -- Porting FIXME: I can't work out how to reproduce the behaviour of the `congr`
-    -- that appears at this point in mathlib3, and so the proof goes off track here.
-    congr! 2
-    · ext1
+    congr! 1
+    · congr
+      ext1
       dsimp [Composition.gather]
       rwa [splitWrtComposition_join]
       simp only [map_ofFn]
       rfl
-    · congr
-    · ext1
-      dsimp [Composition.gather, sigmaCompositionAux]
-      simp [get_splitWrtComposition]
-      sorry
+    · rw [Fin.heq_fun_iff]
+      · intro i
+        dsimp [Composition.sigmaCompositionAux]
+        rw [get_of_eq (splitWrtComposition_join _ _ _)]
+        · simp only [get_ofFn]
+          rfl
+        · simp only [map_ofFn]
+          congr
+        · simp only [map_ofFn]
+          rfl
 #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi

 end Composition

Adam Topaz (Jun 13 2023 at 15:19):

@Mauricio Collares Johan is unable to post for some reason, but he mentioned to me privately that he likes your version better!

Mauricio Collares (Jun 13 2023 at 15:29):

Pushed, thanks!

Jireh Loreaux (Jun 13 2023 at 16:00):

It has a :check:, did you want to mark it awaiting-review?

Scott Morrison (Jun 13 2023 at 22:07):

I've merged now. Nice work, everyone!

Johan Commelin (Jun 14 2023 at 05:36):

Sorry for disappearing suddenly after pushing the wip commit. I can't access zulip at home atm, because my laptop is bricked. I thought new hardware would arrive yesterday, but it seems like I have to wait one more day.

Johan Commelin (Jun 14 2023 at 05:37):

I'm glad the PR got merged while I was offline :octopus:

Last updated: Dec 20 2023 at 11:08 UTC