1 ≤ 1 = true

Stream: maths

[Christopher Hoskin]

This feels like a silly question, but how could I prove the goal:

1 ≤ 1 = true

?

I know that it can be done with simp only [le_refl],, but it feels like it ought to be possible to prove this without having to resort to simp?

[Christopher Hoskin]

( As background, I'm trying to replace the simp in https://github.com/leanprover-community/mathlib/blob/master/src/algebra/order/lattice_group.lean as suggested here: https://github.com/leanprover-community/mathlib4/pull/934#issuecomment-1361463881)

[Kevin Buzzard]

example : 1 ≤ 1 = true := propext dec_trivial

[Kevin Buzzard]

assuming those are natural 1's; you didn't give a mwe (and this won't work for real 1s)

[Ruben Van de Velde]

Maybe

example : 1 ≤ 1 = true := eq_true_intro le_rfl

[Eric Wieser]

How did you end up with this goal in the first place?

[Kevin Buzzard]

There are 21 simps in the file you link to.

[Christopher Hoskin]

I was looking at this simp https://github.com/leanprover-community/mathlib/blob/master/src/algebra/order/lattice_group.lean#L175

I got to:

@[to_additive] -- pos_nonpos_iff
lemma pos_le_one_iff {a : α} : a⁺ ≤ 1 ↔ a ≤ 1 :=
by { rw [m_pos_part_def, sup_le_iff], -- ⊢ a ≤ 1 ∧ 1 ≤ 1 ↔ a ≤ 1
convert and_true (a ≤ 1), -- ⊢ 1 ≤ 1 = true
sorry,
}

[Eric Wieser]

That convert is a bad step; I think there's something like docs#and_iff_left

[Kevin Buzzard]

@[to_additive] -- pos_nonpos_iff
lemma pos_le_one_iff {a : α} : a⁺ ≤ 1 ↔ a ≤ 1 :=
by { rw [m_pos_part_def, sup_le_iff, and_iff_left], exact le_refl _ }

[Christopher Hoskin]

@Kevin Buzzard thanks - that works :)