awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
this :
  @IsMaximal _ inst _
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1, ⋯⟩ :
        Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1)))
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      ⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1, ⋯⟩)
⊢ (↑(Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}))) :
      ℕ) =
    s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1

Tactic:
(tsub_add_cancel_of_le h).symm

Premises used: tsub_add_cancel_of_le, Eq.symm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
this :
  @IsMaximal _ inst _
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1, ⋯⟩ :
        Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1)))
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      ⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1, ⋯⟩)
⊢ (↑(Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}))) :
      ℕ) =
    s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1

Tactic:
exact (tsub_add_cancel_of_le h).symm

Premises used: tsub_add_cancel_of_le, Eq.symm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
h₁ :
  ∀ (x : X),
    x ∈ s ↔
      x ∈
        (eraseLast (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s).snoc
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          (last (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s)
          ⋯
⊢ s =
    (eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).snoc
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s)
      ⋯

Tactic:
ext x
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
x : X
h₁ :
  x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
⊢ x ∈ s ↔
    x ∈
      (eraseLast (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s).snoc
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s)
        ⋯

Tactic:
simp only [mem_snoc, mem_eraseLast h, ne_eq]

Premises used: ne_eq, CompositionSeries.mem_eraseLast, RelSeries.mem_snoc
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
x : X
pos :
  ∀
    (h :
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s),
    x ∈ s ↔
      ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
        x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
neg :
  ∀
    (h :
      ¬x =
          last (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s),
    x ∈ s ↔
      ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
        x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
⊢ x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s

Tactic:
by_cases h : x = s.last

Premises used: RelSeries.last
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h_1 :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
x : X
h :
  x =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
⊢ x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s

Tactic:
simp [*, s.last_mem]

Premises used: RelSeries.last_mem
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h_1 :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
x : X
h :
  ¬x =
      last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s
⊢ x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s

Tactic:
simp [*, s.last_mem]

Premises used: RelSeries.last_mem
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  @IsMaximal _ inst _
    ((eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
hs :
  s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s =
    (eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
simp [last, Fin.ext_iff, hs]

Premises used: Fin.ext_iff, RelSeries.last
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ s.Equivalent s

Tactic:
⟨Equiv.refl _, fun _ => (s.step _).iso_refl⟩

Premises used: Exists.intro, JordanHolderLattice.IsMaximal.iso_refl, RelSeries.step, Equiv.refl, CompositionSeries.Equivalent
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ s₃ : CompositionSeries X
h₁ : s₁.Equivalent s₂
h₂ : s₂.Equivalent s₃
⊢ s₁.Equivalent s₃

Tactic:
⟨h₁.choose.trans h₂.choose,
    fun i => iso_trans (h₁.choose_spec i) (h₂.choose_spec (h₁.choose i))⟩

Premises used: Exists.choose_spec, Equiv.trans, JordanHolderLattice.iso_trans, Exists.intro, Exists.choose, DFunLike.coe, CompositionSeries.Equivalent
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
⊢ s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    s₂.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
simpa using Fintype.card_congr h.choose

Premises used: Fintype.card_congr, Exists.choose
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
    x₁
hsat₂ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
    x₂
hsaty₁ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₁ hsat₁).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₁
hsaty₂ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₂ hsat₂).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₂
hr₁ :
  @Iso _ inst _
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s,
      x₁)
    (x₂, y₂)
hr₂ :
  @Iso _ inst _ (x₁, y₁)
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s,
      x₂)
e : Fin
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1 +
      1) ≃
  Fin
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1 +
      1) :=
  Equiv.swap
    (Fin.last
      (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
    (Fin.castSucc
      (Fin.last
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))))
⊢ ∀
    {i :
      Fin
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))},
    i.castSucc.castSucc ≠
      Fin.castSucc
        (Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})))

Tactic:
simp
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
    x₁
hsat₂ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
    x₂
hsaty₁ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₁ hsat₁).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₁
hsaty₂ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₂ hsat₂).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₂
hr₁ :
  @Iso _ inst _
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s,
      x₁)
    (x₂, y₂)
hr₂ :
  @Iso _ inst _ (x₁, y₁)
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s,
      x₂)
e : Fin
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1 +
      1) ≃
  Fin
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1 +
      1) :=
  Equiv.swap
    (Fin.last
      (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
    (Fin.castSucc
      (Fin.last
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))))
h1 :
  ∀
    {i :
      Fin
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))},
    i.castSucc.castSucc ≠
      Fin.castSucc
        (Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})))
⊢ ∀
    {i :
      Fin
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))},
    i.castSucc.castSucc ≠
      Fin.last
        (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}) +
          1)

Tactic:
simp
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁ :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ (↑0 : ℕ) =
    (↑(Fin.last
          (s₁.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}))) :
      ℕ)

Tactic:
simp [hs₁]
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁ :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ Eq (α :=
    Fin
      (s₂.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
    (Fin.last
      (s₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})))
    0

Tactic:
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁ :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
this :
  Eq (α :=
    Fin
      (s₂.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
    (Fin.last
      (s₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})))
    0
⊢ s₂.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0

Tactic:
simpa [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
⊢ ¬0 <
        s₂.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) →
    ¬0 <
        s₁.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
simpa only [pos_iff_ne_zero, ne_eq, Decidable.not_not] using
        length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb.symm ht.symm

Premises used: ne_eq, Decidable.not_not, Eq.symm, pos_iff_ne_zero, CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ ∀ (x : X),
    x ∈ s₁ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁

Tactic:
have : ∀ x, x ∈ s₁ ↔ x = s₁.last := fun x =>
    ⟨fun hx =>  subsingleton_of_length_eq_zero hs₁0 hx s₁.last_mem, fun hx => hx.symm ▸ s₁.last_mem⟩
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
this :
  ∀ (x : X),
    x ∈ s₁ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁
⊢ ∀ (x : X),
    x ∈ s₂ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₂

Tactic:
have : ∀ x, x ∈ s₂ ↔ x = s₂.last := fun x =>
    ⟨fun hx =>
      subsingleton_of_length_eq_zero
        (length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht
          hs₁0) hx s₂.last_mem,
      fun hx => hx.symm ▸ s₂.last_mem⟩
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
this_1 :
  ∀ (x : X),
    x ∈ s₁ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁
this :
  ∀ (x : X),
    x ∈ s₂ ↔
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₂
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂

Tactic:
ext