Help with a weird lambda

Stream: new members

[Brendan Seamas Murphy]

Can someone give me a hand with proving the goal from hAgree?

α : Type u,
_inst_1 : topological_space α,
F : presheaf_of_ab_groups α,
U : opens α,
OC : covering U,
si : Π (i : OC.γ), ⇑(sheafification.pre F) (OC.Uis i),
p : α,
i j : OC.γ,
hp1 : p ∈ OC.Uis i,
hp2 : p ∈ OC.Uis j,
a : ⇑(sheafification.pre F) (OC.Uis i),
b : ⇑(sheafification.pre F) (OC.Uis j),
hAgree :
  (λ (p : α) (h : p ∈ ⟨(OC.Uis i).val ∩ (OC.Uis j).val, _⟩), a.val p _) =
    λ (p : α) (h : p ∈ ⟨(OC.Uis i).val ∩ (OC.Uis j).val, _⟩), b.val p _
⊢ a.val p hp1 = b.val p hp2

The details of what sheafification.pre is shouldn't matter, other than that it's a subtype of Π (p ∈ U), stalk_of_ab_groups F p

[Brendan Seamas Murphy]

I've been trying for like half an hour but nothing has helped

[Brendan Seamas Murphy]

Also p ∈ ⟨(OC.Uis i).val ∩ (OC.Uis j).val, _⟩ is definitionally equal to p ∈ (OC.Uis i).val ∩ (OC.Uis j).val, and those are just sets

[Kevin Buzzard]

Try dsimp at hAgree?

[Kevin Buzzard]

Oh the functions are equal so you can evaluate them both at p maybe

[Mario Carneiro]

yes this is the solution

[Kevin Buzzard]

You could use congr_arg or congr_fun

[Brendan Seamas Murphy]

dsimp doesn't work (neither does simp or dsimp *). Is there a good way to get lean to evaluate both sides of a goal?

[Brendan Seamas Murphy]

ah

[Kevin Buzzard]

I forget which one you want

[Mario Carneiro]

congr_fun (congr_fun hAgree p) hp1 should work

[Kevin Buzzard]

Feed it hAgree

[Kevin Buzzard]

Yeah that

[Kevin Buzzard]

Or something like that

[Mario Carneiro]

the fact that hp1 and hp2 are not defeq seems a bit sketchy

[Mario Carneiro]

Oh I think you need to apply it to a proof that it's in the intersection, so congr_fun (congr_fun hAgree p) <hp1, hp2>

[Mario Carneiro]

then the two underscore proofs applied to this should reduce to hp1 and hp2 respectively

[Brendan Seamas Murphy]

That worked, thanks

[Johan Commelin]

@Brendan Seamas Murphy Did you already know about subtypes before learning about sheafification?

[Johan Commelin]

Otherwise this seems to be a pretty hardcore way of learning Hartshorne (-;

[Brendan Seamas Murphy]

Yes

[Brendan Seamas Murphy]

I have formal verification background, I'm just rusty

[Johan Commelin]

Aha... well it's certainly a nice use of those old skills.

[Brendan Seamas Murphy]

There's so many little details to keep track of with sheaves that I figured I might as well try and have a computer keep track of them

[Kevin Buzzard]

There has been some talk here about how best to implement sheaves in type theory and in some sense we still don't know the answer.