awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
obtain : ∀ (z : (↑s : Type u_1)) (hz : x < z) (hz' : z < y), False
⊢ False

Tactic:
obtain ⟨z, hz, hz'⟩ := exists_between H

Premises used: exists_between
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
⊢ ⊥ < (↑z : WithBot X)

Tactic:
simp [(Subtype.coe_lt_coe.mpr hz).trans_le']

Premises used: Iff.mpr, Subtype.coe_lt_coe, LT.lt.trans_le'
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
⊢ ⊥ < (↑z : WithBot X)

Tactic:
have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
rwa : (↑((↑z : WithBot X).unbot ⋯) : WithBot X) < (↑((↑y : WithBot X).unbot ⋯) : WithBot X)
rwa₁ : (↑z : WithBot X) < (↑((↑y : WithBot X).unbot ⋯) : WithBot X)
rwa₂ rwa₃ rwa₄ rwa₅ : (↑z : WithBot X) < (↑y : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯

Tactic:
rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]

Premises used: WithBot.coe_unbot, WithBot.coe_lt_coe
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz' : z < y
hz0 : ⊥ < (↑z : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯

Tactic:
replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
⊢ False

Tactic:
absurd (this ?_ ?_) hz'.ne

Premises used: absurd, LT.lt.ne
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
refine_1 : (↑z : WithBot X).unbot ⋯ ∈ some ⁻¹' s
refine_2 : (↑y : WithBot X).unbot ⋯ ∈ some ⁻¹' s
⊢ False

Tactic:
refine absurd (this ?_ ?_) hz'.ne

Premises used: absurd, LT.lt.ne
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
⊢ (↑z : WithBot X).unbot ⋯ ∈ some ⁻¹' s

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H_1 : DenselyOrdered.{u_1} (↑s : Type u_1)
this : (some ⁻¹' s).Subsingleton
x y : (↑s : Type u_1)
H : x < y
z : (↑s : Type u_1)
hz : x < z
hz'_1 : z < y
hz0 : ⊥ < (↑z : WithBot X)
hz' : (↑z : WithBot X).unbot ⋯ < (↑y : WithBot X).unbot ⋯
⊢ (↑y : WithBot X).unbot ⋯ ∈ some ⁻¹' s

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
suffices : DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)
⊢ ¬∃ (x : (↑s : Type u_1)) (y : (↑s : Type u_1)), x < y

Tactic:
suffices DenselyOrdered (WithBot.some ⁻¹' s) by
    rintro ⟨x, y, H⟩
    rw [_root_.denselyOrdered_set_iff_subsingleton] at this
    obtain ⟨z, hz, hz'⟩ := exists_between H
    have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
    replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
    refine absurd (this ?_ ?_) hz'.ne <;>
    simp
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
dense : ∀ (a₁ a₂ : (↑(some ⁻¹' s) : Type u_1)), a₁ < a₂ → ∃ (a : (↑(some ⁻¹' s) : Type u_1)), a₁ < a ∧ a < a₂
⊢ DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
dense :
  ∀ (a : X) (b : (↑a : WithBot X) ∈ s) (a_1 : X) (b : (↑a_1 : WithBot X) ∈ s),
    a < a_1 → ∃ (a_3 : X), ((↑a_3 : WithBot X) ∈ s ∧ a < a_3) ∧ a_3 < a_1
⊢ ∀ (a₁ a₂ : (↑(some ⁻¹' s) : Type u_1)), a₁ < a₂ → ∃ (a : (↑(some ⁻¹' s) : Type u_1)), a₁ < a ∧ a < a₂

Tactic:
simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right,
    exists_prop]

Premises used: Subtype.mk_lt_mk, Subtype.exists, Subtype.forall, exists_and_right, exists_prop, Set.mem_preimage
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
⊢ Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy

Tactic:
simp [hxy]
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
⊢ Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy

Tactic:
have : (⟨_, hx⟩ : s) < ⟨_, hy⟩ := by simp [hxy]
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
dense :
  ∀ (z : { x : WithBot X // x ∈ s }) (hz : Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx < z)
    (hz' : z < Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy),
    ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y

Tactic:
obtain ⟨z, hz, hz'⟩ := exists_between this

Premises used: exists_between
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx < z
hz' : z < Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
⊢ (↑x : WithBot X) < (↑z : WithBot X)

Tactic:
simp only [← Subtype.coe_lt_coe] at hz hz'

Premises used: Subtype.coe_lt_coe
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx < z
hz' : z < Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
hz₁ : (↑x : WithBot X) < (↑z : WithBot X)
⊢ (↑z : WithBot X) < (↑y : WithBot X)

Tactic:
simp only [← Subtype.coe_lt_coe] at hz hz'

Premises used: Subtype.coe_lt_coe
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
⊢ ⊥ ≤ (↑x : WithBot X)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
dense : (↑((↑z : WithBot X).unbot ⋯) : WithBot X) ∈ s
dense₁ : x < (↑z : WithBot X).unbot ⋯
dense₂ : (↑z : WithBot X).unbot ⋯ < y
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y

Tactic:
refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
⊢ (↑((↑z : WithBot X).unbot ⋯) : WithBot X) ∈ s

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
dense : (↑x : WithBot X) < (↑((↑z : WithBot X).unbot ⋯) : WithBot X)
⊢ x < (↑z : WithBot X).unbot ⋯

Tactic:
rw [← WithBot.coe_lt_coe]

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
⊢ (↑x : WithBot X) < (↑((↑z : WithBot X).unbot ⋯) : WithBot X)

Tactic:
simp [hz.trans_le]

Premises used: LT.lt.trans_le
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
dense : (↑((↑z : WithBot X).unbot ⋯) : WithBot X) < (↑y : WithBot X)
⊢ (↑z : WithBot X).unbot ⋯ < y

Tactic:
rw [← WithBot.coe_lt_coe]

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
x : X
hx : (↑x : WithBot X) ∈ s
y : X
hy : (↑y : WithBot X) ∈ s
hxy : x < y
this :
  Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑x : WithBot X) hx <
    Subtype.mk (p := fun (x : WithBot X) ↦ x ∈ s) (↑y : WithBot X) hy
z : { x : WithBot X // x ∈ s }
hz : (↑x : WithBot X) < (↑z : WithBot X)
hz' : (↑z : WithBot X) < (↑y : WithBot X)
⊢ (↑((↑z : WithBot X).unbot ⋯) : WithBot X) < (↑y : WithBot X)

Tactic:
simp [hz'.trans_le']

Premises used: LT.lt.trans_le'
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithTop X)
⊢ StrictAnti (α := (↑s : Type u_1)) (β := (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1))
    (⇑(Equiv.image WithTop.toDual s) :
      (a : (↑s : Type u_1)) → (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1))

Tactic:
have he : StrictAnti (WithTop.toDual.image s) :=
    WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)
-- Module: Mathlib.Order.Interval.Finset.DenselyOrdered
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithTop X)
he :
  StrictAnti (α := (↑s : Type u_1)) (β := (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1))
    (⇑(Equiv.image WithTop.toDual s) :
      (a : (↑s : Type u_1)) → (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1))
rw : DenselyOrdered.{u_1} (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1) ↔ s.Subsingleton
rw₁ : Set.Subsingleton (α := WithBot Xᵒᵈ) ((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) ↔ s.Subsingleton
rw₂ rw₃ : s.Subsingleton ↔ s.Subsingleton
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton

Tactic:
rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]

Premises used: WithTop.toDual, Function.Injective.subsingleton_image_iff, Equiv.injective, denselyOrdered_iff_of_strictAnti, WithBot.denselyOrdered_set_iff_subsingleton
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n_1 n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) ((Icc (↑a : ℕ) (↑b : ℕ)).attachFin ⋯) x ↔ a ≤ x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n_1 n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ico (↑a : ℕ) (↑b : ℕ)).attachFin ⋯) x ↔ a ≤ x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n_1 n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ioc (↑a : ℕ) (↑b : ℕ)).attachFin ⋯) x ↔ a < x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n_1 n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ioo (↑a : ℕ) (↑b : ℕ)).attachFin ⋯) x ↔ a < x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ (Icc (↑a : ℕ) (↑b : ℕ)).attachFin ⋯ = Icc a b

Tactic:
rfl

Premises used: Finset.Icc, Finset.attachFin, rfl
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ (Ico (↑a : ℕ) (↑b : ℕ)).attachFin ⋯ = Ico a b

Tactic:
rfl

Premises used: Finset.Ico, Finset.attachFin, rfl
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ (Ioc (↑a : ℕ) (↑b : ℕ)).attachFin ⋯ = Ioc a b

Tactic:
rfl

Premises used: Finset.attachFin, rfl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ (Ioo (↑a : ℕ) (↑b : ℕ)).attachFin ⋯ = Ioo a b

Tactic:
rfl

Premises used: Finset.attachFin, Finset.Ioo, rfl
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ (uIcc (↑a : ℕ) (↑b : ℕ)).attachFin ⋯ = uIcc a b

Tactic:
rfl

Premises used: Finset.Icc, Finset.attachFin, rfl, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ico (↑a : ℕ) n).attachFin ⋯) a_1 ↔ a_1 ∈ Ici a
⊢ (Ico (↑a : ℕ) n).attachFin ⋯ = Ici a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a a_1 : Fin n
⊢ Membership.mem (γ := Finset (Fin n)) ((Ico (↑a : ℕ) n).attachFin ⋯) a_1 ↔ a_1 ∈ Ici a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ioo (↑a : ℕ) n).attachFin ⋯) a_1 ↔ a_1 ∈ Ioi a
⊢ (Ioo (↑a : ℕ) n).attachFin ⋯ = Ioi a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a a_1 : Fin n
⊢ Membership.mem (γ := Finset (Fin n)) ((Ioo (↑a : ℕ) n).attachFin ⋯) a_1 ↔ a_1 ∈ Ioi a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Iic (↑a : ℕ)).attachFin ⋯) a_1 ↔ a_1 ∈ Iic a
⊢ (Iic (↑a : ℕ)).attachFin ⋯ = Iic a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a a_1 : Fin n
⊢ Membership.mem (γ := Finset (Fin n)) ((Iic (↑a : ℕ)).attachFin ⋯) a_1 ↔ a_1 ∈ Iic a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Iio (↑a : ℕ)).attachFin ⋯) a_1 ↔ a_1 ∈ Iio a
⊢ (Iio (↑a : ℕ)).attachFin ⋯ = Iio a

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a a_1 : Fin n
⊢ Membership.mem (γ := Finset (Fin n)) ((Iio (↑a : ℕ)).attachFin ⋯) a_1 ↔ a_1 ∈ Iio a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ image val (Icc a b) = Icc (↑a : ℕ) (↑b : ℕ)

Tactic:
image_val_attachFin _

Premises used: Finset.Icc, Finset.image_val_attachFin, Finset.attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ image val (Ico a b) = Ico (↑a : ℕ) (↑b : ℕ)

Tactic:
image_val_attachFin _

Premises used: Finset.Ico, Finset.image_val_attachFin, Finset.attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ image val (Ioc a b) = Ioc (↑a : ℕ) (↑b : ℕ)

Tactic:
image_val_attachFin _

Premises used: Finset.image_val_attachFin, Finset.attachFin, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ image val (Ioo a b) = Ioo (↑a : ℕ) (↑b : ℕ)

Tactic:
image_val_attachFin _

Premises used: Finset.image_val_attachFin, Finset.attachFin, Finset.Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ image val (uIcc a b) = uIcc (↑a : ℕ) (↑b : ℕ)

Tactic:
finsetImage_val_Icc _ _

Premises used: Fin.finsetImage_val_Icc, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
⊢ image val (Ici a) = Ico (↑a : ℕ) n

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
⊢ image val (Ioi a) = Ioo (↑a : ℕ) n

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
⊢ image val (Iic a) = Iic (↑a : ℕ)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
b : Fin n
⊢ image val (Iio b) = Iio (↑b : ℕ)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Icc a b) = Icc (↑a : ℕ) (↑b : ℕ)

Tactic:
map_valEmbedding_attachFin _

Premises used: Finset.Icc, Finset.map_valEmbedding_attachFin, Finset.attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ico a b) = Ico (↑a : ℕ) (↑b : ℕ)

Tactic:
map_valEmbedding_attachFin _

Premises used: Finset.Ico, Finset.map_valEmbedding_attachFin, Finset.attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioc a b) = Ioc (↑a : ℕ) (↑b : ℕ)

Tactic:
map_valEmbedding_attachFin _

Premises used: Finset.map_valEmbedding_attachFin, Finset.attachFin, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioo a b) = Ioo (↑a : ℕ) (↑b : ℕ)

Tactic:
map_valEmbedding_attachFin _

Premises used: Finset.map_valEmbedding_attachFin, Finset.attachFin, Finset.Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ map valEmbedding (uIcc a b) = uIcc (↑a : ℕ) (↑b : ℕ)

Tactic:
map_valEmbedding_Icc _ _

Premises used: Fin.map_valEmbedding_Icc, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Ico (↑a : ℕ) n).attachFin ⋯) = Ico (↑a : ℕ) n
rw₁ rw₂ : Ico (↑a : ℕ) n = Ico (↑a : ℕ) n
⊢ map valEmbedding (Ici a) = Ico (↑a : ℕ) n

Tactic:
rw [← attachFin_Ico_eq_Ici, map_valEmbedding_attachFin]

Premises used: Fin.attachFin_Ico_eq_Ici, Finset.map_valEmbedding_attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Ioo (↑a : ℕ) n).attachFin ⋯) = Ioo (↑a : ℕ) n
rw₁ rw₂ : Ioo (↑a : ℕ) n = Ioo (↑a : ℕ) n
⊢ map valEmbedding (Ioi a) = Ioo (↑a : ℕ) n

Tactic:
rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]

Premises used: Fin.attachFin_Ioo_eq_Ioi, Finset.map_valEmbedding_attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Iic (↑a : ℕ)).attachFin ⋯) = Iic (↑a : ℕ)
rw₁ rw₂ : Iic (↑a : ℕ) = Iic (↑a : ℕ)
⊢ map valEmbedding (Iic a) = Iic (↑a : ℕ)

Tactic:
rw [← attachFin_Iic, map_valEmbedding_attachFin]

Premises used: Fin.attachFin_Iic, Finset.map_valEmbedding_attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Iio (↑a : ℕ)).attachFin ⋯) = Iio (↑a : ℕ)
rw₁ rw₂ : Iio (↑a : ℕ) = Iio (↑a : ℕ)
⊢ map valEmbedding (Iio a) = Iio (↑a : ℕ)

Tactic:
rw [← attachFin_Iio, map_valEmbedding_attachFin]

Premises used: Fin.attachFin_Iio, Finset.map_valEmbedding_attachFin
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iic a) = Iic (castLE h a)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj