From 62ac547f1438fea1b2ee544aee1b965416b1d600 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 1 Aug 2024 12:33:56 -0400
Subject: [PATCH] Delete `ToMathlib/Logic/Basic`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We no longer need `forall₂_and_distrib`, `forall_and` works.
---
 SphereEversion.lean                       | 1 -
 SphereEversion/Global/Gromov.lean         | 5 ++---
 SphereEversion/ToMathlib/Logic/Basic.lean | 6 ------
 3 files changed, 2 insertions(+), 10 deletions(-)
 delete mode 100644 SphereEversion/ToMathlib/Logic/Basic.lean

diff --git a/SphereEversion.lean b/SphereEversion.lean
index dfa89056..657df270 100644
--- a/SphereEversion.lean
+++ b/SphereEversion.lean
@@ -53,7 +53,6 @@ import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
 import SphereEversion.ToMathlib.LinearAlgebra.Basic
 import SphereEversion.ToMathlib.LinearAlgebra.Basis
 import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional
-import SphereEversion.ToMathlib.Logic.Basic
 import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
 import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
 import SphereEversion.ToMathlib.Order.Filter.Basic
diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index ea3d42a1..e5c42bfb 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -1,7 +1,6 @@
 import SphereEversion.Global.LocalisationData
 import SphereEversion.Global.LocalizedConstruction
 import SphereEversion.Global.ParametricityForFree
-import SphereEversion.ToMathlib.Logic.Basic
 import SphereEversion.ToMathlib.Geometry.Manifold.Metrizable
 
 /-!
@@ -170,7 +169,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
     · apply hF'₁.mono fun x hx ↦ ?_
       rw [hx]
   rcases inductive_htpy_construction' P₀ P₁ P₂ hP₂ hP₂' init ind with ⟨F, hF₀, hFP₀, hFP₁, hFP₂⟩
-  simp only [P₀, forall₂_and_distrib] at hFP₀
+  simp only [P₀, forall_and] at hFP₀
   rcases hFP₀ with ⟨hF_sec, hF_sol, _hF_smooth, hF_A, hF_dist⟩
   refine ⟨mkHtpyFormalSol F hF_sec hF_sol hFP₂, ?_, hFP₁, ?_, ?_⟩
   · intro x
@@ -326,7 +325,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
   rcases inductive_htpy_construction P₀ P₁ P₂ hP₂ L.lf_φ K_cover init (𝓕₀.smooth.comp contMDiff_snd)
       ind with
     ⟨F, hF₀, hFP₀, hFP₁, hFP₂⟩
-  simp only [P₀, forall₂_and_distrib] at hFP₀
+  simp only [P₀, forall_and] at hFP₀
   rcases hFP₀ with ⟨hF_sec, hF_sol, _hF_smooth, hF_A, hF_dist⟩
   refine ⟨mkHtpyFormalSol F hF_sec hF_sol hFP₂, ?_, hFP₁, ?_, ?_⟩
   · intro x
diff --git a/SphereEversion/ToMathlib/Logic/Basic.lean b/SphereEversion/ToMathlib/Logic/Basic.lean
deleted file mode 100644
index d9ee5816..00000000
--- a/SphereEversion/ToMathlib/Logic/Basic.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import Mathlib.Tactic.TypeStar
-
--- `by simp [forall_and]` works in Lean 4
-theorem forall₂_and_distrib {α β : Sort*} {p q : α → β → Prop} :
-    (∀ x y, p x y ∧ q x y) ↔ (∀ x y, p x y) ∧ ∀ x y, q x y :=
-  (forall_congr' fun x : α ↦ @forall_and _ (p x) (q x)).trans forall_and