Commit 2026-05-29 12:25 154ede8c

View on Github →

fix(Tactic/FunProp): detect Continuous.subtype_mk as compositional (#35683) This PR changes fun_prop to detect some theorems involving dependent types, such as Continuous.subtype_mk to be in compositional form. This lets fun_prop solve goals such as Continuous fun x => (⟨x, trivial⟩ : {x : ℝ // True}).

Estimated changes

Modified Mathlib/Tactic/FunProp/Core.lean

Modified Mathlib/Tactic/FunProp/FunctionData.lean

added inductive Mathlib.Meta.FunProp.DecompositionResult

added def Mathlib.Meta.FunProp.FunctionData.decomposition

deleted def Mathlib.Meta.FunProp.FunctionData.nontrivialDecomposition

modified def Mathlib.Meta.FunProp.FunctionData.peeloffArgDecomposition

Modified Mathlib/Tactic/FunProp/Theorems.lean

added def Mathlib.Meta.FunProp.DecompositionResult.toTheoremForm

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified MathlibTest/FunPropMinimal.lean

added theorem Con_imp

added theorem Con_subtype_mk