From dedd9275ec162e181bbbd11ce65ba3bdfbf38e02 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 22 Jul 2025 11:09:24 -0700
Subject: [PATCH] fix: `mkCongrSimpCore?` (#9472)

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

closes #9466
---
 src/Lean/Meta/CongrTheorems.lean          | 100 ++-
 tests/lean/run/congrSimpBug.lean          |  12 +
 tests/lean/run/congrSimpMathlibIssue.lean | 757 ++++++++++++++++++++++
 3 files changed, 835 insertions(+), 34 deletions(-)
 create mode 100644 tests/lean/run/congrSimpMathlibIssue.lean

diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index 5d56b9371d..406507b074 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -5,10 +5,13 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.AddDecl
+import Lean.Class
 import Lean.ReservedNameAction
 import Lean.ResolveName
 import Lean.Meta.AppBuilder
-import Lean.Class
+import Lean.Meta.Tactic.Subst
+import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Assert
 
 namespace Lean.Meta
 
@@ -133,32 +136,6 @@ private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind
           break
   return kinds
 
-/--
-(Tries to) cast expression `e` to the given type using the equations `eqs`.
-`deps` contains the indices of the relevant equalities.
-Remark: deps is sorted.
--/
-private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do
-  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
-     if i < deps.size then
-       match eqs[deps[i]!]! with
-       | none => go (i+1) type
-       | some major =>
-         let some (_, lhs, rhs) := (← inferType major).eq? | unreachable!
-         if (← pure major.isFVar <&&> dependsOn type major.fvarId!) then
-           let motive ← mkLambdaFVars #[rhs, major] type
-           let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs)
-           let minor ← go (i+1) typeNew
-           mkEqRec motive minor major
-         else
-           let motive ← mkLambdaFVars #[rhs] type
-           let typeNew := type.replaceFVar rhs lhs
-           let minor ← go (i+1) typeNew
-           mkEqNDRec motive minor major
-     else
-       return e
-  go 0 type
-
 /-- Returns `true` if `kinds` contains `.cast` or `.subsingletonInst` -/
 private def hasCastLike (kinds : Array CongrArgKind) : Bool :=
   kinds.any fun kind => kind matches .cast | .subsingletonInst
@@ -260,6 +237,63 @@ def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) :=
       result := result.push .fixed
   return fixKindsForDependencies info result
 
+/--
+Auxiliary type for applying `mkCast` at `mkCongrSimpCore?`
+-/
+private inductive EqInfo where
+  | /-- `fvarId` is an equality for "type casting." -/
+    hyp (fvarId : FVarId)
+  | /--
+    `lhs` and `rhs` are `Decidable` instances which should have the same type after
+    we have applied other type casting operations. We use the helper theorem `Decidable.eq`
+    to perform the type cast operation.
+    -/
+    decSubsingleton (lhs rhs : FVarId)
+
+/--
+Helper function for applying the substitution `s`.
+It assumes that all entries in `s` map free variables to free variables.
+-/
+private def getFVarId (s : FVarSubst) (fvarId : FVarId) : FVarId :=
+  if let some h := s.find? fvarId then h.fvarId! else fvarId
+
+/--
+(Tries to) cast free variable `fvarId` to the given type using the equations `eqs`.
+`deps` contains the indices of the relevant equalities.
+Remark: deps is sorted.
+-/
+private partial def mkCast (fvarId : FVarId) (type : Expr) (deps : Array Nat) (eqs : Array (Option EqInfo)) : MetaM Expr := do
+  -- Remark: we use the `subst` tactic to avoid re-implementing the `revert`/`intro` logic used there.
+  let eqs := deps.filterMap fun idx => eqs[idx]!
+  if eqs.isEmpty then return mkFVar fvarId
+  let mvar ← mkFreshExprMVar type
+  let mut mvarId := mvar.mvarId!
+  let mut s : FVarSubst := {}
+  for eq in eqs do
+    match eq with
+    | .hyp fvarId =>
+      let fvarId := getFVarId s fvarId
+      let (s', mvarId') ← substCore mvarId fvarId (symm := true) s
+      s := s'
+      mvarId := mvarId'
+    | .decSubsingleton lhsFVarId rhsFVarId =>
+      let lhsFVarId := getFVarId s lhsFVarId
+      let rhsFVarId := getFVarId s rhsFVarId
+      let lhs := mkFVar lhsFVarId
+      let rhs := mkFVar rhsFVarId
+      let eq ← mvarId.withContext <| mkEq lhs rhs
+      let h ← mvarId.withContext <| mkAppM ``Subsingleton.elim #[lhs, rhs]
+      mvarId ← mvarId.assert `h eq h
+      let (fvarId', mvarId') ← mvarId.intro1
+      let (s', mvarId') ← substCore mvarId' fvarId' (symm := true) s
+      s := s'
+      mvarId := mvarId'
+  let fvarId := getFVarId s fvarId
+  mvarId.assign (mkFVar fvarId)
+  let r ← instantiateMVars mvar
+  trace[Meta.debug] "{r} : {← inferType r}"
+  return r
+
 /--
 Creates a congruence theorem that is useful for the simplifier and `congr` tactic.
 -/
@@ -277,7 +311,7 @@ where
     Create a congruence theorem that is useful for the simplifier.
     In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem
     contains an input `a_i` representing the i-th argument in the left-hand-side, and
-    it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side.
+    it appears with a cast (e.g., `Eq.rec ... a_i ...`) in the right-hand-side.
     The idea is that the right-hand-side of this theorem "tells" the simplifier
     how the resulting term looks like. -/
   mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
@@ -285,7 +319,7 @@ where
       let fType ← inferType f
       forallBoundedTelescope fType kinds.size (cleanupAnnotations := true) fun lhss _ => do
         if lhss.size != kinds.size then return none
-        let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
+        let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option EqInfo)) (hyps : Array Expr) : MetaM CongrTheorem := do
           if i == kinds.size then
             let lhs := mkAppN f lhss
             let rhs := mkAppN f rhss
@@ -300,11 +334,11 @@ where
               let localDecl ← lhss[i]!.fvarId!.getDecl
               withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do
               withLocalDeclD (localDecl.userName.appendBefore "e_") (← mkEq lhss[i]! rhs) fun eq => do
-                go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq)
+                go (i+1) (rhss.push rhs) (eqs.push <| some <| .hyp eq.fvarId!) (hyps.push rhs |>.push eq)
             | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps
             | .cast =>
               let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[*...rhss.size]) rhss
-              let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs
+              let rhs ← mkCast lhss[i]!.fvarId! rhsType info.paramInfo[i]!.backDeps eqs
               go (i+1) (rhss.push rhs) (eqs.push none) hyps
             | .subsingletonInst =>
               -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
@@ -314,9 +348,7 @@ where
                 let rhsType := lhsType.replaceFVars (lhss[*...rhss.size]) rhss
                 let rhsBi   := if subsingletonInstImplicitRhs then .instImplicit else .implicit
                 withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs => do
-                  let lhs' ← mkCast lhs rhsType info.paramInfo[i]!.backDeps eqs
-                  let heq ← mkAppM ``Subsingleton.elim #[lhs', rhs]
-                  go (i+1) (rhss.push rhs) (eqs.push heq) (hyps.push rhs)
+                  go (i+1) (rhss.push rhs) (eqs.push <| some <| .decSubsingleton lhs.fvarId! rhs.fvarId!) (hyps.push rhs)
         return some (← go 0 #[] #[] #[])
     catch _ =>
       return none
diff --git a/tests/lean/run/congrSimpBug.lean b/tests/lean/run/congrSimpBug.lean
index 17b0714cfa..38d941abb9 100644
--- a/tests/lean/run/congrSimpBug.lean
+++ b/tests/lean/run/congrSimpBug.lean
@@ -59,3 +59,15 @@ info: test7.congr_simp.{u} {α : Type u} {i : DecidableEq α} [i✝ : DecidableE
 -/
 #guard_msgs in
 #check test7.congr_simp
+
+def test8 (p : Prop) [Decidable p] (_ : decide p = true) : Nat := 3
+
+/--
+info: test8.congr_simp (p p✝ : Prop) (e_p : p = p✝) {inst✝ : Decidable p} [Decidable p✝] (x✝ : decide p = true) :
+  test8 p x✝ =
+    test8 p✝
+      (Eq.ndrec (motive := fun p => ∀ [inst : Decidable p], decide p = true)
+        (fun [inst : Decidable p] => Subsingleton.elim inst✝ inst ▸ x✝) e_p)
+-/
+#guard_msgs in
+#check test8.congr_simp
diff --git a/tests/lean/run/congrSimpMathlibIssue.lean b/tests/lean/run/congrSimpMathlibIssue.lean
new file mode 100644
index 0000000000..dab087d3e6
--- /dev/null
+++ b/tests/lean/run/congrSimpMathlibIssue.lean
@@ -0,0 +1,757 @@
+import Lean.Elab.Term
+
+/-!
+# Turán's theorem
+-/
+
+set_option warn.sorry false
+
+section Mathlib.Tactic.TypeStar
+
+open Lean
+
+elab "Sort*" : term => do
+  let u ← Lean.Meta.mkFreshLevelMVar
+  Elab.Term.levelMVarToParam (.sort u)
+
+elab "Type*" : term => do
+  let u ← Lean.Meta.mkFreshLevelMVar
+  Elab.Term.levelMVarToParam (.sort (.succ u))
+
+end Mathlib.Tactic.TypeStar
+
+section Mathlib.Data.Set.Defs
+
+universe u
+variable {α : Type u}
+
+/-- A set is a collection of elements of some type `α`.
+
+Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
+relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
+and predicates.
+-/
+def Set (α : Type u) := α → Prop
+
+/-- Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}` -/
+def setOf {α : Type u} (p : α → Prop) : Set α :=
+  p
+
+namespace Set
+
+/-- Membership in a set -/
+protected def Mem (s : Set α) (a : α) : Prop :=
+  s a
+
+instance : Membership α (Set α) :=
+  ⟨Set.Mem⟩
+
+end Set
+
+end Mathlib.Data.Set.Defs
+
+section Mathlib.Order.Defs.Unbundled
+
+variable {α : Sort*} (r : α → α → Prop)
+
+/-- `IsSymm` as a definition, suitable for use in proofs. -/
+def Symmetric := ∀ ⦃x y⦄, r x y → r y x
+
+end Mathlib.Order.Defs.Unbundled
+
+section Mathlib.Data.List.Defs
+
+namespace List
+
+variable {α : Type*}
+
+section Choose
+
+variable (p : α → Prop) [DecidablePred p] (l : List α)
+
+/-- Given a decidable predicate `p` and a proof of existence of `a ∈ l` such that `p a`,
+choose the first element with this property. This version returns both `a` and proofs
+of `a ∈ l` and `p a`. -/
+def chooseX : ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }
+  | [], hp => False.elim (Exists.elim hp fun _ h => not_mem_nil h.left)
+  | l :: ls, hp =>
+    if pl : p l then ⟨l, ⟨mem_cons.mpr <| Or.inl rfl, pl⟩⟩
+    else
+      -- pattern matching on `hx` too makes this not reducible!
+      let ⟨a, ha⟩ :=
+        chooseX ls
+          (hp.imp fun _ ⟨o, h₂⟩ => ⟨(mem_cons.mp o).resolve_left fun e => pl <| e ▸ h₂, h₂⟩)
+      ⟨a, mem_cons.mpr <| Or.inr ha.1, ha.2⟩
+
+end Choose
+
+end List
+
+end Mathlib.Data.List.Defs
+
+section Mathlib.Data.Set.CoeSort
+
+namespace Set
+
+universe u v w
+
+variable {α : Type u} {β : Type v} {γ : Type w}
+
+/-- Given the set `s`, `Elem s` is the `Type` of element of `s`.
+
+It is currently an abbreviation so that instance coming from `Subtype` are available.
+If you're interested in making it a `def`, as it probably should be,
+you'll then need to create additional instances (and possibly prove lemmas about them).
+See e.g. `Mathlib/Data/Set/Order.lean`.
+-/
+@[coe, reducible] def Elem (s : Set α) : Type u := {x // x ∈ s}
+
+/-- Coercion from a set to the corresponding subtype. -/
+instance : CoeSort (Set α) (Type u) := ⟨Elem⟩
+
+end Set
+
+end Mathlib.Data.Set.CoeSort
+
+section Mathlib.Data.Multiset.Defs
+
+universe v
+
+open List Subtype Nat Function
+
+variable {α : Type*} {β : Type v} {γ : Type*}
+
+/-- `Multiset α` is the quotient of `List α` by list permutation. The result
+  is a type of finite sets with duplicates allowed. -/
+def Multiset.{u} (α : Type u) : Type u :=
+  Quotient (List.isSetoid α)
+
+namespace Multiset
+
+/-- The quotient map from `List α` to `Multiset α`. -/
+def ofList : List α → Multiset α :=
+  Quot.mk _
+
+section Mem
+
+/-- `a ∈ s` means that `a` has nonzero multiplicity in `s`. -/
+def Mem (s : Multiset α) (a : α) : Prop :=
+  Quot.liftOn s (fun l => a ∈ l) fun l₁ l₂ (e : l₁ ~ l₂) => propext <| e.mem_iff
+
+instance : Membership α (Multiset α) :=
+  ⟨Mem⟩
+
+instance decidableMem [DecidableEq α] (a : α) (s : Multiset α) : Decidable (a ∈ s) :=
+  Quot.recOnSubsingleton s fun l ↦ inferInstanceAs (Decidable (a ∈ l))
+
+end Mem
+
+/-- The cardinality of a multiset is the sum of the multiplicities
+  of all its elements, or simply the length of the underlying list. -/
+def card : Multiset α → Nat := Quot.lift length sorry
+
+/-- Lift of the list `pmap` operation. Map a partial function `f` over a multiset
+  `s` whose elements are all in the domain of `f`. -/
+nonrec def pmap {p : α → Prop} (f : ∀ a, p a → β) (s : Multiset α) : (∀ a ∈ s, p a) → Multiset β :=
+  Quot.recOn s (fun l H => ofList (pmap f l H)) sorry
+
+end Multiset
+
+end Mathlib.Data.Multiset.Defs
+
+section Mathlib.Data.Multiset.ZeroCons
+
+universe v
+
+open List Subtype Nat Function
+
+variable {α : Type*} {β : Type v} {γ : Type*}
+
+namespace Multiset
+
+/-- `0 : Multiset α` is the empty set -/
+protected def zero : Multiset α :=
+  ofList (@nil α)
+
+instance : Zero (Multiset α) :=
+  ⟨Multiset.zero⟩
+
+end Multiset
+
+end Mathlib.Data.Multiset.ZeroCons
+
+section Mathlib.Data.Multiset.Basic
+
+universe v
+
+open List Subtype Nat Function
+
+variable {α : Type*} {β : Type v} {γ : Type*}
+
+namespace Multiset
+
+section Choose
+
+variable (p : α → Prop) [DecidablePred p] (l : Multiset α)
+
+/-- Given a proof `hp` that there exists a unique `a ∈ l` such that `p a`, `chooseX p l hp` returns
+that `a` together with proofs of `a ∈ l` and `p a`. -/
+def chooseX : ∀ _hp : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a } :=
+  Quotient.recOn l (fun l' h => List.chooseX p l' h) sorry
+
+end Choose
+
+end Multiset
+
+end Mathlib.Data.Multiset.Basic
+
+section Mathlib.Data.Multiset.MapFold
+
+variable {α β : Type*}
+
+namespace Multiset
+
+/-- `map f s` is the lift of the list `map` operation. The multiplicity
+  of `b` in `map f s` is the number of `a ∈ s` (counting multiplicity)
+  such that `f a = b`. -/
+def map (f : α → β) (s : Multiset α) : Multiset β :=
+  Quot.liftOn s (fun l : List α => ofList <| l.map f) sorry
+
+end Multiset
+
+end Mathlib.Data.Multiset.MapFold
+
+section Mathlib.Data.Multiset.Filter
+
+variable {α : Type*}
+
+namespace Multiset
+
+variable (p : α → Prop) [DecidablePred p]
+
+/-- `Filter p s` returns the elements in `s` (with the same multiplicities)
+  which satisfy `p`, and removes the rest. -/
+def filter (s : Multiset α) : Multiset α :=
+  Quot.liftOn s (fun l => ofList <| List.filter p l) sorry
+
+end Multiset
+
+end Mathlib.Data.Multiset.Filter
+
+section Mathlib.Data.Finset.Defs
+
+universe u
+
+variable {α : Type*} {β : Type*} {γ : Type*}
+
+/-- `Finset α` is the type of finite sets of elements of `α`. It is implemented
+  as a multiset (a list up to permutation) which has no duplicate elements. -/
+structure Finset (α : Type*) where
+  /-- The underlying multiset -/
+  val : Multiset α
+
+namespace Finset
+
+theorem val_inj {s t : Finset α} : s.1 = t.1 ↔ s = t := sorry
+
+instance : Membership α (Finset α) :=
+  ⟨fun s a => a ∈ s.1⟩
+
+instance decidableMem [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ s) :=
+  Multiset.decidableMem _ _
+
+end Finset
+
+end Mathlib.Data.Finset.Defs
+
+section Mathlib.Data.Finset.Dedup
+
+universe u
+
+variable {α : Type*} {β : Type*} {γ : Type*}
+
+namespace Finset
+
+end Finset
+
+/-! ### dedup on list and multiset -/
+
+namespace Multiset
+
+variable [DecidableEq α] {s t : Multiset α}
+
+/-- `toFinset s` removes duplicates from the multiset `s` to produce a finset. -/
+def toFinset (s : Multiset α) : Finset α := ⟨s⟩
+
+end Multiset
+
+end Mathlib.Data.Finset.Dedup
+
+section Mathlib.Data.Finset.Empty
+
+universe u
+
+variable {α : Type*} {β : Type*} {γ : Type*}
+
+namespace Finset
+
+section Empty
+
+variable {s : Finset α}
+
+/-- The empty finset -/
+protected def empty : Finset α := ⟨0⟩
+
+end Empty
+end Finset
+
+end Mathlib.Data.Finset.Empty
+
+section Mathlib.Data.Finset.Filter
+
+variable {α : Type*}
+
+namespace Finset
+
+section Filter
+
+variable (p : α → Prop) [DecidablePred p]
+
+/-- `Finset.filter p s` is the set of elements of `s` that satisfy `p`.
+For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α`
+as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available). -/
+def filter (s : Finset α) : Finset α :=
+  ⟨s.1.filter p⟩
+
+end Finset.Filter
+
+end Mathlib.Data.Finset.Filter
+
+section Mathlib.Data.Finset.Basic
+
+variable {α : Type*}
+
+namespace Finset
+
+section Choose
+
+variable (p : α → Prop) [DecidablePred p] (l : Finset α)
+
+/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
+`l` satisfying `p` this unique element, as an element of the corresponding subtype. -/
+def chooseX (hp : ∃ a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a } :=
+  Multiset.chooseX p l.val hp
+
+/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
+`l` satisfying `p` this unique element, as an element of the ambient type. -/
+def choose (hp : ∃ a, a ∈ l ∧ p a) : α :=
+  chooseX p l hp
+
+end Choose
+
+end Finset
+
+end Mathlib.Data.Finset.Basic
+
+section Mathlib.Data.Finset.Image
+
+variable {α β γ : Type*}
+
+namespace Finset
+
+section Map
+
+/-- When `f` is an embedding of `α` in `β` and `s` is a finset in `α`, then `s.map f` is the image
+finset in `β`. The embedding condition guarantees that there are no duplicates in the image. -/
+def map (f : α → β) (s : Finset α) : Finset β := ⟨s.1.map f⟩
+
+end Map
+
+section Image
+
+variable [DecidableEq β]
+
+/-- `image f s` is the forward image of `s` under `f`. -/
+def image (f : α → β) (s : Finset α) : Finset β :=
+  (s.1.map f).toFinset
+
+end Image
+
+end Finset
+
+end Mathlib.Data.Finset.Image
+
+section Mathlib.Data.Finset.Card
+
+variable {α β R : Type*}
+
+namespace Finset
+
+variable {s t : Finset α} {a b : α}
+
+/-- `s.card` is the number of elements of `s`, aka its cardinality.
+The notation `#s` can be accessed in the `Finset` locale. -/
+def card (s : Finset α) : Nat :=
+  Multiset.card s.1
+
+end Finset
+
+end Mathlib.Data.Finset.Card
+
+section Mathlib.Data.Fintype.Defs
+
+variable {α β γ : Type*}
+
+/-- `Fintype α` means that `α` is finite, i.e. there are only
+  finitely many distinct elements of type `α`. The evidence of this
+  is a finset `elems` (a list up to permutation without duplicates),
+  together with a proof that everything of type `α` is in the list. -/
+class Fintype (α : Type*) where
+  /-- The `Finset` containing all elements of a `Fintype` -/
+  elems : Finset α
+
+namespace Finset
+
+variable [Fintype α] {s t : Finset α}
+
+/-- `univ` is the universal finite set of type `Finset α` implied from
+  the assumption `Fintype α`. -/
+def univ : Finset α := @Fintype.elems α _
+
+end Finset
+
+namespace Fintype
+
+/-- Given a predicate that can be represented by a finset, the subtype
+associated to the predicate is a fintype. -/
+protected def subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) :
+    Fintype { x // p x } :=
+  ⟨⟨s.1.pmap Subtype.mk fun x => (H x).1⟩⟩
+
+end Fintype
+
+end Mathlib.Data.Fintype.Defs
+
+section Mathlib.Data.Fintype.Sets
+
+variable {α β γ : Type*}
+
+open Finset
+
+namespace Set
+
+variable {s t : Set α}
+
+/-- Construct a finset enumerating a set `s`, given a `Fintype` instance. -/
+def toFinset (s : Set α) [Fintype s] : Finset α :=
+  (@Finset.univ s _).map <| Subtype.val
+
+end Set
+
+instance Subtype.fintype (p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x // p x } :=
+  Fintype.subtype (univ.filter p) sorry
+
+end Mathlib.Data.Fintype.Sets
+
+section Mathlib.Data.Sym.Sym2
+
+open Function
+
+universe u
+
+variable {α β γ : Type*}
+
+namespace Sym2
+
+/-- This is the relation capturing the notion of pairs equivalent up to permutations. -/
+inductive Rel (α : Type u) : α × α → α × α → Prop
+  | refl (x y : α) : Rel _ (x, y) (x, y)
+  | swap (x y : α) : Rel _ (x, y) (y, x)
+
+end Sym2
+
+/-- `Sym2 α` is the symmetric square of `α`, which, in other words, is the
+type of unordered pairs. -/
+abbrev Sym2 (α : Type u) := Quot (Sym2.Rel α)
+
+/-- Constructor for `Sym2`. This is the quotient map `α × α → Sym2 α`. -/
+protected abbrev Sym2.mk {α : Type*} (p : α × α) : Sym2 α := Quot.mk (Sym2.Rel α) p
+
+namespace Sym2
+
+/-- The universal property of `Sym2`; symmetric functions of two arguments are equivalent to
+functions from `Sym2`. Note that when `β` is `Prop`, it can sometimes be more convenient to use
+`Sym2.fromRel` instead. -/
+def lift : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ } → (Sym2 α → β) :=
+  fun f => Quot.lift (uncurry f) <| by sorry
+
+section Relations
+
+variable {r : α → α → Prop}
+
+/-- Symmetric relations define a set on `Sym2 α` by taking all those pairs
+of elements that are related.
+-/
+def fromRel (sym : Symmetric r) : Set (Sym2 α) :=
+  setOf (lift ⟨r, fun _ _ => propext ⟨(sym ·), (sym ·)⟩⟩)
+
+instance fromRel.decidablePred (sym : Symmetric r) [h : DecidableRel r] :
+    DecidablePred (· ∈ Sym2.fromRel sym) := fun z => z.recOnSubsingleton fun _ => h _ _
+
+end Relations
+
+end Sym2
+
+end Mathlib.Data.Sym.Sym2
+
+section Mathlib.Data.List.Sym
+
+namespace List
+
+variable {α β : Type*}
+
+section Sym2
+
+/-- `xs.sym2` is a list of all unordered pairs of elements from `xs`.
+If `xs` has no duplicates then neither does `xs.sym2`. -/
+protected def sym2 : List α → List (Sym2 α)
+  | [] => []
+  | x :: xs => (x :: xs).map (fun y => .mk (x, y)) ++ xs.sym2
+
+end Sym2
+
+end List
+
+end Mathlib.Data.List.Sym
+
+section Mathlib.Data.Multiset.Sym
+
+namespace Multiset
+
+variable {α β : Type*}
+
+section Sym2
+
+/-- `m.sym2` is the multiset of all unordered pairs of elements from `m`, with multiplicity.
+If `m` has no duplicates then neither does `m.sym2`. -/
+protected def sym2 (m : Multiset α) : Multiset (Sym2 α) :=
+  m.liftOn (fun xs => ofList xs.sym2) fun _ _ h => sorry
+
+end Sym2
+
+end Multiset
+
+end Mathlib.Data.Multiset.Sym
+
+section Mathlib.Data.Finset.Sym
+
+namespace Finset
+
+variable {α β : Type*}
+
+protected def sym2 (s : Finset α) : Finset (Sym2 α) := ⟨s.1.sym2⟩
+
+section
+variable {s t : Finset α} {a b : α}
+
+instance _root_.Sym2.instFintype [Fintype α] : Fintype (Sym2 α) where
+  elems := Finset.univ.sym2
+
+end
+
+end Finset
+
+end Mathlib.Data.Finset.Sym
+
+section Mathlib.Combinatorics.SimpleGraph.Basic
+
+open Function
+
+universe u v w
+
+/-- A simple graph is an irreflexive symmetric relation `Adj` on a vertex type `V`.
+The relation describes which pairs of vertices are adjacent.
+There is exactly one edge for every pair of adjacent vertices;
+see `SimpleGraph.edgeSet` for the corresponding edge set.
+-/
+structure SimpleGraph (V : Type u) where
+  /-- The adjacency relation of a simple graph. -/
+  Adj : V → V → Prop
+
+namespace SimpleGraph
+
+variable {ι : Sort*} {V : Type u} (G : SimpleGraph V) {a b c u v w : V} {e : Sym2 V}
+
+section EdgeSet
+
+variable {G₁ G₂ : SimpleGraph V}
+
+/-- The edges of G consist of the unordered pairs of vertices related by
+`G.Adj`. This is the order embedding; for the edge set of a particular graph, see
+`SimpleGraph.edgeSet`.
+
+The way `edgeSet` is defined is such that `mem_edgeSet` is proved by `Iff.rfl`.
+(That is, `s(v, w) ∈ G.edgeSet` is definitionally equal to `G.Adj v w`.)
+-/
+-- Porting note: We need a separate definition so that dot notation works.
+def edgeSetEmbedding (V : Type*) : SimpleGraph V → Set (Sym2 V) :=
+  fun G => Sym2.fromRel (r := G.1) sorry
+
+/-- `G.edgeSet` is the edge set for `G`.
+This is an abbreviation for `edgeSetEmbedding G` that permits dot notation. -/
+abbrev edgeSet (G : SimpleGraph V) : Set (Sym2 V) := edgeSetEmbedding V G
+
+variable (G₁ G₂)
+
+instance decidableMemEdgeSet [DecidableRel G.Adj] : DecidablePred (· ∈ G.edgeSet) :=
+  Sym2.fromRel.decidablePred sorry
+
+end EdgeSet
+
+end SimpleGraph
+
+end Mathlib.Combinatorics.SimpleGraph.Basic
+
+section Mathlib.Combinatorics.SimpleGraph.Finite
+namespace SimpleGraph
+
+variable {V : Type*} (G : SimpleGraph V) {e : Sym2 V}
+variable {G₁ G₂ : SimpleGraph V} [Fintype G.edgeSet] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet]
+
+/-- The `edgeSet` of the graph as a `Finset`. -/
+abbrev edgeFinset : Finset (Sym2 V) := Set.toFinset G.edgeSet
+
+end SimpleGraph
+end Mathlib.Combinatorics.SimpleGraph.Finite
+
+section Mathlib.Combinatorics.SimpleGraph.Clique
+
+namespace SimpleGraph
+
+variable {α β : Type*} (G H : SimpleGraph α)
+
+/-! ### `n`-cliques -/
+
+section NClique
+
+variable {n : Nat} {s : Finset α}
+
+/-- An `n`-clique in a graph is a set of `n` vertices which are pairwise connected. -/
+structure IsNClique (G : SimpleGraph α) (n : Nat) (s : Finset α) : Prop where
+
+end NClique
+
+/-! ### Graphs without cliques -/
+
+
+section CliqueFree
+
+variable {m n : Nat}
+
+/-- `G.CliqueFree n` means that `G` has no `n`-cliques. -/
+def CliqueFree (n : Nat) : Prop :=
+  ∀ t, ¬G.IsNClique n t
+
+end CliqueFree
+
+end SimpleGraph
+end Mathlib.Combinatorics.SimpleGraph.Clique
+
+section Mathlib.Order.Partition.Finpartition
+open Finset
+
+variable {α : Type*}
+
+/-- A finite partition of `a : α` is a pairwise disjoint finite set of elements whose supremum is
+`a`. We forbid `⊥` as a part. -/
+structure Finpartition (a : α) where
+  /-- The elements of the finite partition of `a` -/
+  parts : Finset α
+
+/-! ### Finite partitions of finsets -/
+
+namespace Finpartition
+
+variable [DecidableEq α] {s t u : Finset α} (P : Finpartition s) {a : α}
+
+theorem existsUnique_mem (ha : a ∈ s) : ∃ t, t ∈ P.parts ∧ a ∈ t := by sorry
+
+/-- The part of the finpartition that `a` lies in. -/
+def part (a : α) : Finset α := if ha : a ∈ s then choose (hp := P.existsUnique_mem ha) else .empty
+
+section SetSetoid
+
+/-- A setoid over a finite type induces a finpartition of the type's elements,
+where the parts are the setoid's equivalence classes. -/
+def ofSetSetoid (s : Setoid α) (x : Finset α) [DecidableRel s.r] : Finpartition x where
+  parts := x.image fun a ↦ x.filter (s.r a ·)
+
+end SetSetoid
+
+section Setoid
+
+variable [Fintype α]
+
+/-- A setoid over a finite type induces a finpartition of the type's elements,
+where the parts are the setoid's equivalence classes. -/
+def ofSetoid (s : Setoid α) [DecidableRel s.r] : Finpartition (univ : Finset α) :=
+  ofSetSetoid s univ
+
+end Setoid
+
+end Finpartition
+
+end Mathlib.Order.Partition.Finpartition
+
+open Finset
+
+namespace SimpleGraph
+
+variable {V : Type*} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n r : Nat}
+
+variable (G) in
+/-- An `r + 1`-cliquefree graph is `r`-Turán-maximal if any other `r + 1`-cliquefree graph on
+the same vertex set has the same or fewer number of edges. -/
+def IsTuranMaximal (r : Nat) : Prop :=
+  G.CliqueFree (r + 1) ∧ ∀ (H : SimpleGraph V) [DecidableRel H.Adj],
+    H.CliqueFree (r + 1) → H.edgeFinset.card ≤ G.edgeFinset.card
+
+namespace IsTuranMaximal
+
+variable {s t u : V}
+
+variable (h : G.IsTuranMaximal r)
+include h
+
+/-- In a Turán-maximal graph, non-adjacency is an equivalence relation. -/
+theorem equivalence_not_adj : Equivalence (¬G.Adj · ·) where
+  refl := sorry
+  symm := sorry
+  trans := sorry
+
+/-- The non-adjacency setoid over the vertices of a Turán-maximal graph
+induced by `equivalence_not_adj`. -/
+def setoid : Setoid V := ⟨_, h.equivalence_not_adj⟩
+
+instance : DecidableRel h.setoid.r :=
+  inferInstanceAs <| DecidableRel (¬G.Adj · ·)
+
+/-- The finpartition derived from `h.setoid`. -/
+def finpartition [DecidableEq V] : Finpartition (univ : Finset V) := Finpartition.ofSetoid h.setoid
+
+theorem not_adj_iff_part_eq [DecidableEq V] :
+    ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t := by sorry
+
+theorem card_parts_extracted_1_11 [DecidableEq V] :
+  let fp := h.finpartition;
+  fp.parts.card < (Finset.univ (α := V)).card ∧ fp.parts.card < r →
+    ∀ (x y : V),
+      x ≠ y → fp.part x = fp.part y →
+      ∀ ⦃z : Finset V⦄, z.card = r → ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y := by
+  intro fp l x y hn he z zc
+  simp [h.not_adj_iff_part_eq] ---- should work
+  sorry
+
+end IsTuranMaximal
+
+end SimpleGraph