Equality of structure with single constructor

Stream: new members

[Tobias Grosser]

I try to complete this simple proof:

ll: { field := a }.1 = { field := b }.1
⊢ a = b

Is there a lean tactic that allows me to complete this proof? I would hope that there is a way to get rid of the storing a value in a struct and directly extracting it again, in case of single-element structures.

[Eric Wieser]

exact ll

[Eric Wieser]

dsimp only at ll would clean things up in the more general case

[Tobias Grosser]

Nice.

[Tobias Grosser]

In my proof I also have a ↑v1.1 = ↑v2.1 (cooersion Fin to Nat) from which I want to derive that v1.1 = v2.1.

[Eric Wieser]

have := Fin.coe_injective h

[Eric Wieser]

Though if that second term is your goal, your could also use ext

[Tobias Grosser]

I guess that can be written more concise.

[Tobias Grosser]

I am particularly unhappy with having to use cases which unfolds things quite a bit.

[Tobias Grosser]

I could not really use the ext

[Tobias Grosser]

I am particularly unhappy with having to use cases which unfolds things quite a bit.

[Tobias Grosser]

I guess that can be written more concise.

[Tobias Grosser]

But I came up with the following:

theorem test {n : Nat} {v1 v2 : Fin n} {h : (↑v1 : Nat) = (↑v2 : Nat)} : v1 = v2 := by
  cases v1
  cases v2
  simp [*]
  dsimp only at h
  exact h

[Tobias Grosser]

OK, I got it:

theorem test {n : Nat} {v1 v2 : Fin n} {h : (↑v1 : Nat) = (↑v2 : Nat)} : v1 = v2 :=
  Fin.val_injective h