Single issue in !4##2565 Combinatorics.SimpleGraph.Prod

Stream: mathlib4

[Arien Malec]

I again have a file down to a single issue, this time what appears to be a missing type inference at Finset.univ in boxProd_neighborFinset. There are a limited set of types it could be but I haven't managed to type annotate correctly yet. Would appreciate extra eyes on...

[Rémi Bottinelli]

  obtain ⟨xa,xb⟩ := x
  ext ⟨a,b⟩
  aesop

seems to close the goal, but I don't know if that's allowed? Oh, but I think it poisons some instance?

Edit with that proof above, the next theorem fails, but you can dumbly make it work again with

theorem boxProd_degree (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)]
    [Fintype ((G □ H).neighborSet x)] : (G □ H).degree x = G.degree x.1 + H.degree x.2 := by
  rw [degree, degree, degree, boxProd_neighborFinset, Finset.card_disjUnion]
  simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]
  exact x
  exact y

I don't understand why it needs those two new exacts.

[Rémi Bottinelli]

theorem boxProd_neighborFinset (x : α × β) [Fintype (G.neighborSet x.1)]
    [Fintype (H.neighborSet x.2)] [Fintype ((G □ H).neighborSet x)] :
    (G □ H).neighborFinset x =
      -- porting note: was `×ˢ`
      (G.neighborFinset x.1 ×ᶠ {x.2}).disjUnion ({x.1} ×ᶠ H.neighborFinset x.2)
        (Finset.disjoint_product.mpr <| Or.inl <| neighborFinset_disjoint_singleton _ _) := by
  obtain ⟨_, _⟩ := x
  ext ⟨_, _⟩
  aesop
#align simple_graph.box_prod_neighbor_finset SimpleGraph.boxProd_neighborFinset

theorem boxProd_degree (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)]
    [Fintype ((G □ H).neighborSet x)] : (G □ H).degree x = G.degree x.1 + H.degree x.2 := by
  rw [degree, degree, degree, boxProd_neighborFinset, Finset.card_disjUnion]
  simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]
  exact x
  exact y
#align simple_graph.box_prod_degree SimpleGraph.boxProd_degree

So, if I use aesop in the first theorem, it decides to catch two implicit variables, not sure why.
Seems to me this is a case where omit would have been useful.

[Kyle Miller]

The aesop thing is a gotcha when you're coming from Lean 3. Now every variable is available in theorems and there's no way for a smart tactic to know that it shouldn't do cases on something in the local context.

A solution to this is to be more careful with what you put in your variables. I went ahead and did that

[Kyle Miller]

But I also fixed the proof of boxProd_neighborFinset, which is now slightly more careful about how it replaces the Fintype instance.

[Rémi Bottinelli]

The aesop thing is a gotcha when you're coming from Lean 3. Now every variable is available in theorems and there's no way for a smart tactic to know that it shouldn't do cases on something in the local context.

That seems like a footgun. Is there a way/plan to remedy this?
I mean, the "no need for omit/include anymore" pitch doesn't mean much if you can actually get got by unwanted use of variables…

[Kyle Miller]

Another place to be careful is with induction since it generalizes all variables that depend on variables involved in the induction.

[Kyle Miller]

I'm not sure there's a good solution beyond relying more on autoimplicits and mimicking omit/include by carefully crafting your variables.

[Rémi Bottinelli]

ah, autoimplicits mean we don't have as much of an incentive to keep variables around, good point!