-- Mathlib/Order/JordanHolder.lean
theorem smash {s₁ s₂ t₁ t₂ : CompositionSeries X}
    (hs : s₁.last = s₂.head) (ht : t₁.last = t₂.head)
    (h₁ : Equivalent s₁ t₁) (h₂ : Equivalent s₂ t₂) :
    Equivalent (smash s₁ s₂ hs) (smash t₁ t₂ ht) :=
  let e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
    calc
      Fin (s₁.length + s₂.length) ≃ (Fin s₁.length) ⊕ (Fin s₂.length) := finSumFinEquiv.symm
      _ ≃ (Fin t₁.length) ⊕ (Fin t₂.length) := Equiv.sumCongr h₁.choose h₂.choose
      _ ≃ Fin (t₁.length + t₂.length) := finSumFinEquiv
  ⟨e, by
    intro i
    refine Fin.addCases ?_ ?_ i
    · intro i
      simpa [-smash_toFun, e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i
    · intro i
      simpa [-smash_toFun, e, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i⟩

Proof state:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

Tactic:
intro i

Result:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₁.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ Iso ((smash s₁ s₂ hs).toFun i.castSucc, (smash s₁ s₂ hs).toFun i.succ)
    ((smash t₁ t₂ ht).toFun (e i).castSucc, (smash t₁ t₂ ht).toFun (e i).succ)

Tactic:
refine Fin.addCases ?_ ?_ i

Result:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Proof state:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
intro i

Result:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₂.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Proof state:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₂.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
simpa [-smash_toFun, e, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
⊢ ∀ (i : Fin (smash s₁ s₂ hs).length),
    Iso ((smash s₁ s₂ hs).toFun i.castSucc, (smash s₁ s₂ hs).toFun i.succ)
      ((smash t₁ t₂ ht).toFun (e i).castSucc, (smash t₁ t₂ ht).toFun (e i).succ)

Tactic:
intro i

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ Iso ((smash s₁ s₂ hs).toFun i.castSucc, (smash s₁ s₂ hs).toFun i.succ)
    ((smash t₁ t₂ ht).toFun (e i).castSucc, (smash t₁ t₂ ht).toFun (e i).succ)