| 1870.lean:12:2-12:35: error: type mismatch | |
| congrArg ?_ (congrArg ?_ ?_) | |
| has type | |
| ?_ (?_ ?_) = ?_ (?_ ?_) : Prop | |
| but is expected to have type | |
| OfNat.ofNat 0 = OfNat.ofNat 1 : Prop | |
| 1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify | |
| ?f ?a₁ = ?f ?a₂ | |
| with | |
| OfNat.ofNat 0 = OfNat.ofNat 1 | |
| ⊢ OfNat.ofNat 0 = OfNat.ofNat 1 | |
| 1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify | |
| ?f ?a₁ = ?f ?a₂ | |
| with | |
| OfNat.ofNat 0 = OfNat.ofNat 1 | |
| ⊢ OfNat.ofNat 0 = OfNat.ofNat 1 |