commit: 1e40623e3e9438444c8844bdf92ae8c7d0b1f548

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Tue Jul 22 10:29:10 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Jul 22 10:31:56 2025 -0700
tree: b5ad764738199a39d34d424d78817105158b60b8
parent: 0cc4c918008d64269460bdba41fbcd3df8445af6 [diff]

fix: `mkCongrSimpCore?`

This PR fixes another issue at the `congr_simp` theorems that was
affecting Mathlib. Many thanks to Johan Commelin for creating the mwe.

3 files changed

tree: b5ad764738199a39d34d424d78817105158b60b8

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.