awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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 : (↑s : Type u_1)) (y : (↑s : Type u_1)), x < y
have suffices : DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)
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
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
⊢ DenselyOrdered.{u_1} (↑(some ⁻¹' s) : Type u_1)
have dense : ∀ (a₁ a₂ : (↑(some ⁻¹' s) : Type u_1)), a₁ < a₂ → ∃ (a : (↑(some ⁻¹' s) : Type u_1)), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered.{u_1} (↑s : Type u_1)
⊢ ∀ (a₁ a₂ : (↑(some ⁻¹' s) : Type u_1)), a₁ < a₂ → ∃ (a : (↑(some ⁻¹' s) : Type u_1)), a₁ < a ∧ a < a₂
have 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
Tactic: simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right,
    exists_prop]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
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
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have 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
Tactic: have : (⟨_, hx⟩ : s) < ⟨_, hy⟩ := by simp [hxy]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have 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
Tactic: obtain ⟨z, hz, hz'⟩ := exists_between this
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
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
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have hz₁ : (↑x : WithBot X) < (↑z : WithBot X)
Tactic: simp only [← Subtype.coe_lt_coe] at hz hz'
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
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)
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have hz'₁ : (↑z : WithBot X) < (↑y : WithBot X)
Tactic: simp only [← Subtype.coe_lt_coe] at hz hz'
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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)
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have dense : (↑((↑z : WithBot X).unbot sorry) : WithBot X) ∈ s
Tactic: refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have dense₁ : x < (↑z : WithBot X).unbot sorry
Tactic: refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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 ⋯
⊢ ∃ (a : X), ((↑a : WithBot X) ∈ s ∧ x < a) ∧ a < y
have dense₂ : (↑z : WithBot X).unbot sorry < y
Tactic: refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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 < (↑z : WithBot X).unbot ⋯
have dense : (↑x : WithBot X) < (↑((↑z : WithBot X).unbot sorry) : WithBot X)
Tactic: rw [← WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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 ⋯ < y
have dense : (↑((↑z : WithBot X).unbot sorry) : WithBot X) < (↑y : WithBot X)
Tactic: rw [← WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithTop X)
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton
have 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))
Tactic: have he : StrictAnti (WithTop.toDual.image s) :=
    WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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))
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton
have rw : DenselyOrdered.{u_1} (↑((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) : Type u_1) ↔ s.Subsingleton
Tactic: rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton
have rw₁ : Set.Subsingleton (α := WithBot Xᵒᵈ) ((⇑WithTop.toDual : (a : WithTop X) → WithBot Xᵒᵈ) '' s) ↔ s.Subsingleton
Tactic: rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.DenselyOrdered (goal)
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
⊢ DenselyOrdered.{u_1} (↑s : Type u_1) ↔ s.Subsingleton
have rw₂ : s.Subsingleton ↔ s.Subsingleton
Tactic: rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ (Ico (↑a : ℕ) n).attachFin ⋯ = Ici a
have h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ico (↑a : ℕ) n).attachFin sorry) a_1 ↔ a_1 ∈ Ici a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ (Ioo (↑a : ℕ) n).attachFin ⋯ = Ioi a
have h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Ioo (↑a : ℕ) n).attachFin sorry) a_1 ↔ a_1 ∈ Ioi a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ (Iic (↑a : ℕ)).attachFin ⋯ = Iic a
have h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Iic (↑a : ℕ)).attachFin sorry) a_1 ↔ a_1 ∈ Iic a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ (Iio (↑a : ℕ)).attachFin ⋯ = Iio a
have h : ∀ (a_1 : Fin n), Membership.mem (γ := Finset (Fin n)) ((Iio (↑a : ℕ)).attachFin sorry) a_1 ↔ a_1 ∈ Iio a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Ico (↑a : ℕ) n
have rw : map (α := Fin n) valEmbedding ((Ico (↑a : ℕ) n).attachFin sorry) = Ico (↑a : ℕ) n
Tactic: rw [← attachFin_Ico_eq_Ici, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Ico (↑a : ℕ) n).attachFin ⋯) = Ico (↑a : ℕ) n
⊢ map valEmbedding (Ici a) = Ico (↑a : ℕ) n
have rw₁ : Ico (↑a : ℕ) n = Ico (↑a : ℕ) n
Tactic: rw [← attachFin_Ico_eq_Ici, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioo (↑a : ℕ) n
have rw : map (α := Fin n) valEmbedding ((Ioo (↑a : ℕ) n).attachFin sorry) = Ioo (↑a : ℕ) n
Tactic: rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Ioo (↑a : ℕ) n).attachFin ⋯) = Ioo (↑a : ℕ) n
⊢ map valEmbedding (Ioi a) = Ioo (↑a : ℕ) n
have rw₁ : Ioo (↑a : ℕ) n = Ioo (↑a : ℕ) n
Tactic: rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ map valEmbedding (Iic a) = Iic (↑a : ℕ)
have rw : map (α := Fin n) valEmbedding ((Iic (↑a : ℕ)).attachFin sorry) = Iic (↑a : ℕ)
Tactic: rw [← attachFin_Iic, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Iic (↑a : ℕ)).attachFin ⋯) = Iic (↑a : ℕ)
⊢ map valEmbedding (Iic a) = Iic (↑a : ℕ)
have rw₁ : Iic (↑a : ℕ) = Iic (↑a : ℕ)
Tactic: rw [← attachFin_Iic, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ map valEmbedding (Iio a) = Iio (↑a : ℕ)
have rw : map (α := Fin n) valEmbedding ((Iio (↑a : ℕ)).attachFin sorry) = Iio (↑a : ℕ)
Tactic: rw [← attachFin_Iio, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : map (α := Fin n) valEmbedding ((Iio (↑a : ℕ)).attachFin ⋯) = Iio (↑a : ℕ)
⊢ map valEmbedding (Iio a) = Iio (↑a : ℕ)
have rw₁ : Iio (↑a : ℕ) = Iio (↑a : ℕ)
Tactic: rw [← attachFin_Iio, map_valEmbedding_attachFin]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw₁ : #(Icc a b) = #(map valEmbedding (Icc a b))
Tactic: rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Icc a b) = #(map valEmbedding (Icc a b))
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)
have rw₂ : #(Icc a b) = #(Icc a b)
Tactic: rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ico a b) = #(map valEmbedding (Ico a b))
Tactic: rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ico a b) = #(map valEmbedding (Ico a b))
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₂ : #(Ico a b) = #(Ico a b)
Tactic: rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₁ : #(Ioc a b) = #(map valEmbedding (Ioc a b))
Tactic: rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioc a b) = #(map valEmbedding (Ioc a b))
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)
have rw₂ : #(Ioc a b) = #(Ioc a b)
Tactic: rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
⊢ #(Ioo a b) = (↑b : ℕ) - (↑a : ℕ) - 1
have rw : #(Ioo a b) = #(Ioo (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ioo a b) = #(Ioo (↑a : ℕ) (↑b : ℕ))
⊢ #(Ioo a b) = (↑b : ℕ) - (↑a : ℕ) - 1
have rw₁ : #(Ioo a b) = #(map valEmbedding (Ioo a b))
Tactic: rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(Ioo a b) = #(Ioo (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioo a b) = #(map valEmbedding (Ioo a b))
⊢ #(Ioo a b) = (↑b : ℕ) - (↑a : ℕ) - 1
have rw₂ : #(Ioo a b) = #(Ioo a b)
Tactic: rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
Tactic: rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw₁ : #(uIcc a b) = #(map valEmbedding (uIcc a b))
Tactic: rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a b : Fin n
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(uIcc a b) = #(map valEmbedding (uIcc a b))
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1
have rw₂ : #(uIcc a b) = #(uIcc a b)
Tactic: rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ #(Ici a) = n - (↑a : ℕ)
have rw : card (α := Fin n) ((Ico (↑a : ℕ) n).attachFin sorry) = n - (↑a : ℕ)
Tactic: rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : card (α := Fin n) ((Ico (↑a : ℕ) n).attachFin ⋯) = n - (↑a : ℕ)
⊢ #(Ici a) = n - (↑a : ℕ)
have rw₁ : #(Ico (↑a : ℕ) n) = n - (↑a : ℕ)
Tactic: rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : card (α := Fin n) ((Ico (↑a : ℕ) n).attachFin ⋯) = n - (↑a : ℕ)
rw₁ : #(Ico (↑a : ℕ) n) = n - (↑a : ℕ)
⊢ #(Ici a) = n - (↑a : ℕ)
have rw₂ : n - (↑a : ℕ) = n - (↑a : ℕ)
Tactic: rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw₁ : Fin n ↪ ℕ
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
rw₁ : Fin n ↪ ℕ
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw₂ : Type
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
rw₁ : Fin n ↪ ℕ
rw₂ : Type
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw₃ : #(Ioo (↑a : ℕ) n) = n - 1 - (↑a : ℕ)
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
rw₁ : Fin n ↪ ℕ
rw₂ : Type
rw₃ : #(Ioo (↑a : ℕ) n) = n - 1 - (↑a : ℕ)
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw₄ : n - (↑a : ℕ) - 1 = n - 1 - (↑a : ℕ)
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
rw₁ : Fin n ↪ ℕ
rw₂ : Type
rw₃ : #(Ioo (↑a : ℕ) n) = n - 1 - (↑a : ℕ)
rw₄ : n - (↑a : ℕ) - 1 = n - 1 - (↑a : ℕ)
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)
have rw₅ : n - 1 - (↑a : ℕ) = n - 1 - (↑a : ℕ)
Tactic: rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
⊢ #(Iic b) = (↑b : ℕ) + 1
have rw : #(Iic b) = #(Iic (↑b : ℕ))
Tactic: rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
rw : #(Iic b) = #(Iic (↑b : ℕ))
⊢ #(Iic b) = (↑b : ℕ) + 1
have rw₁ : #(Iic b) = #(map valEmbedding (Iic b))
Tactic: rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
rw : #(Iic b) = #(Iic (↑b : ℕ))
rw₁ : #(Iic b) = #(map valEmbedding (Iic b))
⊢ #(Iic b) = (↑b : ℕ) + 1
have rw₂ : #(Iic b) = #(Iic b)
Tactic: rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
⊢ #(Iio b) = (↑b : ℕ)
have rw : #(Iio b) = #(Iio (↑b : ℕ))
Tactic: rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
rw : #(Iio b) = #(Iio (↑b : ℕ))
⊢ #(Iio b) = (↑b : ℕ)
have rw₁ : #(Iio b) = #(map valEmbedding (Iio b))
Tactic: rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Fin (goal)
Goal:
n : ℕ
b : Fin n
rw : #(Iio b) = #(Iio (↑b : ℕ))
rw₁ : #(Iio b) = #(map valEmbedding (Iio b))
⊢ #(Iio b) = (↑b : ℕ)
have rw₂ : #(Iio b) = #(Iio b)
Tactic: rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (goal)
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (↑j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ
have h₁ : (↑(↑j.succ : Fin (k + 1)) : ℕ) = (↑(⟨j, hj⟩ : Fin k).succ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Gaps (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).2
have this : (↑j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ
Tactic: have : (j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ := by ext; simp [hj]