Lean4
/-- Given `ra := a*r` `sb := b*s` `ts := t*s` `tr := t*r` `tsEqa : t*s = a` `trEqb : t*r = b`,
return a proof for `ra = sb`.
We use `a*b` to denote an AC application. That is, `(a*b)*(c*a)` is the term `a*a*b*c`. -/
def mkACSuperposeProof (ra sb a b r s ts tr : ACApps) (tsEqa trEqb : DelayedExpr) : MetaM DelayedExpr := do
let .apps _ _ := tr |
failure
let .apps op _ := ts |
failure
let some tse := ts.toExpr |
failure
let some re := r.toExpr |
failure
let some tre := tr.toExpr |
failure
let some se := s.toExpr |
failure
let some ae := a.toExpr |
failure
let some be := b.toExpr |
failure
let some rae := ra.toExpr |
failure
let some sbe := sb.toExpr |
failure
let tsrEqar := DelayedExpr.congrFun (.congrArg op tsEqa) r
let trsEqbs := DelayedExpr.congrFun (.congrArg op trEqb) s
let tsr := mkApp2 op tse re
let trs := mkApp2 op tre se
let ar := mkApp2 op ae re
let bs := mkApp2 op be se
let tsrEqtrs ← mkACProof tsr trs
let raEqar ← mkACProof rae ar
let bsEqsb ← mkACProof bs sbe
return .eqTrans raEqar (.eqTrans (.eqSymm tsrEqar) (.eqTrans tsrEqtrs (.eqTrans trsEqbs bsEqsb)))
