-- Mathlib/Order/JordanHolder.lean
theorem mem_eraseLast {s : CompositionSeries X} {x : X} (h : 0 < s.length) :
    x ∈ s.eraseLast ↔ x ≠ s.last ∧ x ∈ s

Proof state:
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩

Tactic:
intro h

Result:
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ last s ∧ x ∈ range s.toFun
⊢ x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩

Proof state:
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun

Tactic:
rintro ⟨i, rfl⟩

Result:
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i => s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i => s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < (s.length - Nat.succ 0).succ

Tactic:
exact i.2

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩) ↔ x ≠ last s ∧ x ∈ range s.toFun

Tactic:
constructor

Result:
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun

case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩

Proof state:
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i => s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i => s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun

Tactic:
simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ eraseLast s ↔ x ≠ last s ∧ x ∈ s

Tactic:
simp only [RelSeries.mem_def, eraseLast]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩) ↔ x ≠ last s ∧ x ∈ range s.toFun

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < s.length

Tactic:
conv_rhs => rw [← Nat.add_one_sub_one s.length, Nat.succ_sub h]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < (s.length - Nat.succ 0).succ

Proof state:
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ last s ∧ x ∈ range s.toFun
⊢ x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩

Tactic:
exact mem_eraseLast_of_ne_of_mem h.1 h.2

Result:
no goals

Proof state:
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i => s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i => s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun

Tactic:
have hi : (i : ℕ) < s.length := by
  conv_rhs => rw [← Nat.add_one_sub_one s.length, Nat.succ_sub h]
  exact i.2

Result:
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i => s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i => s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun