Proved QHat.rat_meet_zHat and QHat.rat_join_zHat.

[DjangoPeeters]

Proved QHat.rat_meet_zHat and QHat.rat_join_zHat.

[Ruben-VandeVelde]

This is great, but since you asked for feedback, here's some things I might change. Please don't let the wall of text demotivate you; I'm just hoping you might find my suggestions interesting.

[Ruben-VandeVelde]

We avoid using simp without only in the middle of a proof:

Suggested change

	simp at hl hr; rcases lowestTerms x with ⟨⟨N, z, hNz, hx⟩, unique⟩
	simp only [AddMonoidHom.coe_coe, Algebra.TensorProduct.includeLeft_apply,
	Algebra.TensorProduct.includeRight_apply] at hl hr
	rcases lowestTerms x with ⟨⟨N, z, hNz, hx⟩, unique⟩

[Ruben-VandeVelde]

If you add

lemma ZMod.isUnit_natAbs {z : ℤ} {N : ℕ} : IsUnit (z.natAbs : ZMod N) ↔ IsUnit (z : ZMod N) := by
  cases z.natAbs_eq with
  | inl h | inr h => rw [h]; simp [-Int.natCast_natAbs]

then you can rewrite this as

Suggested change

	have : PNat.val l.den.toPNat' = l.den := by simp [l.den_pos]
	simp [IsCoprime]; rw [this]
	have hlp := (ZMod.isUnit_iff_coprime l.num.natAbs l.den).2 l.reduced
	let m := l.num; have hm : l.num = m := by rfl
	rcases m with m | m
	· simp [hm] at *; exact hlp
	· simp [hm] at *; rw [← neg_add, add_comm]; exact IsUnit.neg hlp
	simp_rw [IsCoprime, ZHat.intCast_val, ← ZMod.isUnit_natAbs, ZMod.isUnit_iff_coprime,
	PNat.toPNat'_coe l.den_pos]
	exact l.reduced

That's a lot of changes at one. I:

1. Replaced the simp [IsCoprime] by the output of simp? [IsCoprime]

2. Noted that the cases split didn't use anything specific about l.num, and tried to extract the general statement into the lemma above. That left me with rw [ZMod.isUnit_natAbs] at hlp; exact hlp to finish the proof.

3. Looked at hlp and noticed that I could move the ZMod.isUnit_iff_coprime application out: have hlp := l.reduced; rw [← ZMod.isUnit_iff_coprime, ZMod.isUnit_natAbs] at hlp; exact hlp

4. Rather than working on hlp until it matched the goal, I worked on the goal until it matched hlp: rw [← ZMod.isUnit_natAbs, ZMod.isUnit_iff_coprime]; have hlp := l.reduced; exact hlp

5. Suspect that this should be provable with a single lemma, and found it by searching loogle for Nat.toPNat'

6. This got me to

      simp only [IsCoprime, ZHat.intCast_val]
      rw [PNat.toPNat'_coe l.den_pos]
      rw [← ZMod.isUnit_natAbs, ZMod.isUnit_iff_coprime]
      exact l.reduced

at which point I collapsed everything into a single simp_rw, though I had to move PNat.toPNat'_coe l.den_pos to the end for a reason I didn't investigate.

[Ruben-VandeVelde]

I think it's best to avoid using instance names explicitly. This could be:

Suggested change

	have cop2 : IsCoprime 1 r := ⟨default, by simp [ZMod.instUnique.uniq]⟩
	have cop2 : IsCoprime 1 r := ⟨default, by simp only [PNat.val_ofNat]; exact Subsingleton.elim _ _⟩

or also

Suggested change

	have cop2 : IsCoprime 1 r := ⟨default, by simp [ZMod.instUnique.uniq]⟩
	have cop2 : IsCoprime 1 r := by
	simp only [IsCoprime, PNat.val_ofNat]
	exact isUnit_of_subsingleton _

[Ruben-VandeVelde]

You can write the messy cast like this:

Suggested change

	have : 1 = 1/(@Nat.cast ℚ Rat.instNatCast (PNat.val 1 : ℕ) : ℚ) := by rfl
	have : 1 = 1 / (((1 : ℕ+) : ℕ) : ℚ) := by simp

and it's somehow an accident that rfl works, so I used simp instead

[Ruben-VandeVelde]

A trick: since the result of unique is two equalities of variables, you can substitute them out with

Suggested change

	have h := unique _ _ _ _ ⟨hNz, cop1, hcanon⟩
	obtain ⟨rfl, rfl⟩ := unique _ _ _ _ ⟨hNz, cop1, hcanon⟩

(and then a bit of work below)

[Ruben-VandeVelde]

norm_num isn't the greatest tactic to use here; I'd suggest instead

Suggested change

	use l.num; rw [hx, h.2, (unique N 1 z r ⟨hNz, cop2, hcanon.symm⟩).1]; norm_num
	use l.num; rw [hx, h.2, (unique N 1 z r ⟨hNz, cop2, hcanon.symm⟩).1]
	simp only [AddMonoidHom.coe_coe, eq_intCast, PNat.val_ofNat, Nat.cast_one, ne_eq, one_ne_zero,
	not_false_eq_true, div_self]

[Ruben-VandeVelde]

Again the fact that rfl works is somewhat of an accident, but you could use this instead:

Suggested change

	calc
	↑l.num = i₂ ↑l.num := by simp
	_ = 1 ⊗ₜ[ℤ] ↑l.num:= by rfl
	calc
	↑l.num = i₂ ↑l.num := by simp
	_ = 1 ⊗ₜ[ℤ] ↑l.num:= by simp only [i₂, Algebra.TensorProduct.includeRight_apply]

You could also use

Suggested change

	calc
	↑l.num = i₂ ↑l.num := by simp
	_ = 1 ⊗ₜ[ℤ] ↑l.num:= by rfl
	rw [← map_intCast i₂, i₂, Algebra.TensorProduct.includeRight_apply]

or even

Suggested change

	calc
	↑l.num = i₂ ↑l.num := by simp
	_ = 1 ⊗ₜ[ℤ] ↑l.num:= by rfl
	rw [← map_intCast Algebra.TensorProduct.includeRight, Algebra.TensorProduct.includeRight_apply]

But then you could also add a lemma

@[simp]
lemma one_tmul_intCast {z : ℤ} : (1 : ℚ) ⊗ₜ[ℤ] (z : ZHat) = z := by
  rw [← map_intCast Algebra.TensorProduct.includeRight, Algebra.TensorProduct.includeRight_apply]

and you could replace the norm_num; calc entirely by simp.

Or you could even notice the lemma holds more generally:

@[simp]
lemma _root_.Algebra.TensorProduct.one_tmul_intCast {R : Type*} {A : Type*} {B : Type*}
    [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] {z : ℤ} :
    (1 : A) ⊗ₜ[R] (z : B) = (z : TensorProduct R A B) := by
  rw [← map_intCast Algebra.TensorProduct.includeRight, Algebra.TensorProduct.includeRight_apply]

[DjangoPeeters]

Why is the rfl an accident here? I found it funny and very useful when writing the proof lol.

[kbuzzard]

Sometimes things are "accidentally true by definition". And then if the definition changes, they're no longer accidentally true by definition and the proof breaks. It's better to have a more robust proof.

[Ruben-VandeVelde]

There's a dedicated lemma for this:

Suggested change

	apply le_antisymm
	simp; intro x _
	rw [eq_top_iff]
	intro x _

[Ruben-VandeVelde]

Also possible, not necessarily better:

Suggested change

	have h : z - r = N * q := by simp [hz]
	have h : z - r = N * q := sub_eq_of_eq_add hz

[Ruben-VandeVelde]

We prefer focusing dots to make it clear what goal you're working on:

Suggested change

	use ((r : ℤ) / N : ℚ) ⊗ₜ[ℤ] 1
	constructor; simp; use 1 ⊗ₜ[ℤ] q
	constructor; simp; nth_rw 1 [← mul_one ((r : ℤ) / N : ℚ), div_mul_comm,
	mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]
	use ((r : ℤ) / N : ℚ) ⊗ₜ[ℤ] 1
	constructor
	· simp
	use 1 ⊗ₜ[ℤ] q
	constructor
	· simp
	nth_rw 1 [← mul_one ((r : ℤ) / N : ℚ), div_mul_comm,
	mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]

or you could use:

Suggested change

	use ((r : ℤ) / N : ℚ) ⊗ₜ[ℤ] 1
	constructor; simp; use 1 ⊗ₜ[ℤ] q
	constructor; simp; nth_rw 1 [← mul_one ((r : ℤ) / N : ℚ), div_mul_comm,
	mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]
	refine ⟨((r : ℤ) / N : ℚ) ⊗ₜ[ℤ] 1, by simp, 1 ⊗ₜ[ℤ] q, by simp, ?_⟩
	nth_rw 1 [← mul_one ((r : ℤ) / N : ℚ), div_mul_comm,
	mul_comm, ← zsmul_eq_mul, TensorProduct.smul_tmul, zsmul_eq_mul, mul_one]

[Ruben-VandeVelde]

And please also add \leanok after \begin{proof} for both lemmas in blueprint/src/chapter/ch05automorphicformexample.tex

[DjangoPeeters]

Done.

[DjangoPeeters]

Ruben, I think your 2nd lemma gave an error...

[kbuzzard]

Thanks a lot for your work on this! Can you resolve the issues which have been dealt with so I can see what's going on? Sorry, I've been dealing with real life for most of this week but now I've got more time for FLT.