fix: let use provide last constructor argument, introduce mathlib3-…

…like flattening `use!` (#5350)

Changes:
* `use` now by default discharges with `try with_reducible use_discharger` with a custom discharger tactic rather than `try with_reducible rfl`, which makes it be closer to `exists` and the `use` in mathlib3. It doesn't go so far as to do `try with_reducible trivial` since that involves the `contradiction` tactic.
* this discharger is configurable with `use (discharger := tacticSeq...)`
* the `use` evaluation loop will try refining after constructor failure, so it can be used to fill in all arguments rather than all but the last, like in mathlib3 (closes #5072) but with the caveat that it only works so long as the last argument is not an inductive type (like `Eq`).
* adds `use!`, which is nearly the same as the mathlib3 `use` and fills in constructor arguments along the nodes *and* leaves of the nested constructor expressions. This version tries refining before applying constructors, so it can be used like `exact` for the last argument.

The difference between mathlib3 `use` and this `use!` is that (1) `use!` uses a different tactic to discharge goals (mathlib3 used `trivial'`, which did reducible refl, but also `contradiction`, which we don't emulate) (2) it does not rewrite using `exists_prop`. Regarding 2, this feature seems to be less useful now that bounded existentials encode the bound using a conjunction rather than with nested existentials. We do have `exists_prop` as part of `use_discharger` however.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Archive/MiuLanguage/DecisionSuf.lean

@@ -153,7 +153,7 @@ private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c =
     cases' h with hc hc <;> · rw [hc]; norm_num
   rcases hk with ⟨g, hkg, hgmod⟩
   by_cases hp : c + 3 * (k + 1) ≤ 2 ^ g
-  · use g; exact ⟨hp, hgmod⟩
+  · use g, hp, hgmod
   refine' ⟨g + 2, _, _⟩
   · rw [mul_succ, ← add_assoc, pow_add]
     change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -152,7 +152,7 @@ theorem card_le_two_pow {x k : ℕ} :
     intro m hm
     simp only [M, mem_filter, mem_range, mem_powerset, mem_image, exists_prop] at hm ⊢
     obtain ⟨⟨-, hmp⟩, hms⟩ := hm
-    use ⟨(m + 1).factors, ?_⟩
+    use! (m + 1).factors
     · rwa [Multiset.coe_nodup, ← Nat.squarefree_iff_nodup_factors m.succ_ne_zero]
     refine' ⟨fun p => _, _⟩
     · suffices p ∈ (m + 1).factors → ∃ a : ℕ, a < k ∧ a.succ = p by simpa

Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -133,8 +133,7 @@ theorem exists_rat_eq_of_terminates (terminates : (of v).Terminates) : ∃ q : 
   obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K)
   exact exists_rat_eq_nth_convergent v n
   have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
-  -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5072): was `use`
-  exact ⟨q, this⟩
+  use q, this
 #align generalized_continued_fraction.exists_rat_eq_of_terminates GeneralizedContinuedFraction.exists_rat_eq_of_terminates
 
 end RatOfTerminates
@@ -317,7 +316,7 @@ theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
 theorem exists_nth_stream_eq_none_of_rat (q : ℚ) : ∃ n : ℕ, IntFractPair.stream q n = none := by
   let fract_q_num := (Int.fract q).num; let n := fract_q_num.natAbs + 1
   cases' stream_nth_eq : IntFractPair.stream q n with ifp
-  · use n; exact stream_nth_eq
+  · use n, stream_nth_eq
   · -- arrive at a contradiction since the numerator decreased num + 1 times but every fractional
     -- value is nonnegative.
     have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n :=

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -501,8 +501,6 @@ theorem source_affine_openCover_iff {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y
   · have h := (hP.affine_openCover_TFAE f).out 1 0
     apply h.mp
     use 𝒰
-    use inferInstance
-    exact H
 #align ring_hom.property_is_local.source_affine_open_cover_iff RingHom.PropertyIsLocal.source_affine_openCover_iff
 
 theorem isLocal_sourceAffineLocally : (sourceAffineLocally @P).IsLocal :=

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -116,7 +116,6 @@ instance RepresentablyFlat.id : RepresentablyFlat (𝟭 C) := by
     use StructuredArrow.mk (𝟙 _)
     use StructuredArrow.homMk Y.hom (by erw [Functor.id_map, Category.id_comp])
     use StructuredArrow.homMk Z.hom (by erw [Functor.id_map, Category.id_comp])
-    trivial
   · intro Y Z f g
     use StructuredArrow.mk (𝟙 _)
     use StructuredArrow.homMk Y.hom (by erw [Functor.id_map, Category.id_comp])
@@ -149,7 +148,6 @@ instance RepresentablyFlat.comp (F : C ⥤ D) (G : D ⥤ E) [RepresentablyFlat F
     use StructuredArrow.mk (W.hom ≫ G.map W'.hom)
     use StructuredArrow.homMk Y''.right (by simp [← G.map_comp])
     use StructuredArrow.homMk Z''.right (by simp [← G.map_comp])
-    trivial
   · intro Y Z f g
     let W :=
       @IsCofiltered.eq (StructuredArrow X G) _ _ (StructuredArrow.mk Y.hom)

Mathlib/CategoryTheory/Sites/Coherent.lean

@@ -165,8 +165,6 @@ theorem EffectiveEpiFamily.transitive_of_finite {α : Type} [Fintype α] {Y : α
   apply Coverage.saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
   · apply Coverage.saturate.of
     use α, inferInstance, Y, π
-    simp only [true_and]
-    exact Iff.mp (Sieve.effectiveEpimorphic_family Y π) h'
   · intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
     rw [← hf, Sieve.pullback_comp]
     apply (coherentTopology C).pullback_stable'

Mathlib/Combinatorics/Composition.lean

@@ -859,8 +859,7 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)
         rwa [h₂]
     · intro h
       apply Or.inr
-      use i
-      exact ⟨h, rfl⟩
+      use i, h
 #align composition_as_set_equiv compositionAsSetEquiv
 
 instance compositionAsSetFintype (n : ℕ) : Fintype (CompositionAsSet n) :=

Mathlib/Combinatorics/Hall/Finite.lean

@@ -153,8 +153,7 @@ theorem hall_cond_of_compl {ι : Type u} {t : ι → Finset α} {s : Finset ι}
       exists_imp]
     rintro x (hx | ⟨x', hx', rfl⟩) rat hs
     · exact False.elim <| (hs x) <| And.intro hx rat
-    · use x'
-      exact And.intro hx' (And.intro rat hs)
+    · use x', hx', rat, hs
   · apply biUnion_subset_biUnion_of_subset_left
     apply subset_union_left
 #align hall_marriage_theorem.hall_cond_of_compl HallMarriageTheorem.hall_cond_of_compl

Mathlib/Data/Vector/MapLemmas.lean

@@ -235,8 +235,8 @@ theorem mapAccumr_eq_map {f : α → σ → σ × β} {s₀ : σ} (S : Set σ) (
     (mapAccumr f xs s₀).snd = map (f · s₀ |>.snd) xs := by
   rw[Vector.map_eq_mapAccumr]
   apply mapAccumr_bisim_tail
-  use fun s _ => s ∈ S
-  exact ⟨h₀, @fun s q a h => ⟨closure a s h, out a s s₀ h h₀⟩⟩
+  use fun s _ => s ∈ S, h₀
+  exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
 
 protected theorem map₂_eq_mapAccumr₂ :
     map₂ f xs ys = (mapAccumr₂ (fun x y (_ : Unit) ↦ ((), f x y)) xs ys ()).snd := by
@@ -253,8 +253,8 @@ theorem mapAccumr₂_eq_map₂ {f : α → β → σ → σ × γ} {s₀ : σ} (
     (mapAccumr₂ f xs ys s₀).snd = map₂ (f · · s₀ |>.snd) xs ys := by
   rw[Vector.map₂_eq_mapAccumr₂]
   apply mapAccumr₂_bisim_tail
-  use fun s _ => s ∈ S
-  exact ⟨h₀, @fun s q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩⟩
+  use fun s _ => s ∈ S, h₀
+  exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩
 
 /--
   If an accumulation function `f`, given an initial state `s`, produces `s` as its output state

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -1302,7 +1302,7 @@ theorem finrank_le_one_iff [FiniteDimensional K V] :
     · replace h' := zero_lt_iff.mpr h'
       have : finrank K V = 1 := by linarith
       obtain ⟨v, -, p⟩ := finrank_eq_one_iff'.mp this
-      exact ⟨v, p⟩ -- porting note: was `use`
+      use v, p
   · rintro ⟨v, p⟩
     exact finrank_le_one v p
 #align finrank_le_one_iff finrank_le_one_iff

Mathlib/LinearAlgebra/LinearPMap.lean

@@ -763,8 +763,7 @@ theorem smul_graph (f : E →ₗ.[R] F) (z : M) :
     rw [Submodule.mem_map]
     simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id.def,
       LinearMap.smul_apply, Prod.mk.inj_iff, Prod.exists, exists_exists_and_eq_and]
-    use x_fst, y
-    simp [hy, h]
+    use x_fst, y, hy
   rw [Submodule.mem_map] at h
   rcases h with ⟨x', hx', h⟩
   cases x'
@@ -789,8 +788,7 @@ theorem neg_graph (f : E →ₗ.[R] F) :
     rw [Submodule.mem_map]
     simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id.def,
       LinearMap.neg_apply, Prod.mk.inj_iff, Prod.exists, exists_exists_and_eq_and]
-    use x_fst, y
-    simp [hy, h]
+    use x_fst, y, hy
   rw [Submodule.mem_map] at h
   rcases h with ⟨x', hx', h⟩
   cases x'

Mathlib/NumberTheory/Fermat4.lean

@@ -74,7 +74,6 @@ theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minima
     use Int.natAbs c
     rw [Set.mem_setOf_eq]
     use ⟨a, ⟨b, c⟩⟩
-    tauto
   let m : ℕ := Nat.find S_nonempty
   have m_mem : m ∈ S := Nat.find_spec S_nonempty
   rcases m_mem with ⟨s0, hs0, hs1⟩
@@ -83,7 +82,6 @@ theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minima
   rw [← hs1]
   apply Nat.find_min'
   use ⟨a1, ⟨b1, c1⟩⟩
-  tauto
 #align fermat_42.exists_minimal Fermat42.exists_minimal
 
 /-- a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` must have `a` and `b` coprime. -/
@@ -144,7 +142,6 @@ theorem exists_pos_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) :
   obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h
   rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
   · use a0, b0, c0
-    tauto
   · exfalso
     exact ne_zero hf.1 h1.symm
   · use a0, b0, -c0, neg_of_minimal hf, hc

Mathlib/RingTheory/FiniteType.lean

@@ -143,7 +143,6 @@ theorem iff_quotient_mvPolynomial' : FiniteType R A ↔
   · rw [iff_quotient_mvPolynomial]
     rintro ⟨s, ⟨f, hsur⟩⟩
     use { x : A // x ∈ s }, inferInstance, f
-    exact hsur
   · rintro ⟨ι, ⟨hfintype, ⟨f, hsur⟩⟩⟩
     letI : Fintype ι := hfintype
     exact FiniteType.of_surjective (FiniteType.mvPolynomial R ι) f hsur

Mathlib/RingTheory/Polynomial/Content.lean

@@ -118,7 +118,6 @@ theorem content_X_mul {p : R[X]} : content (X * p) = content p := by
     constructor
     · intro h
       use a
-      simp [h]
     · rintro ⟨b, ⟨h1, h2⟩⟩
       rw [← Nat.succ_injective h2]
       apply h1

Mathlib/RingTheory/Polynomial/GaussLemma.lean

@@ -97,8 +97,7 @@ theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd [IsIntegrallyClosed R] {f : R[X]}
       (integralClosure.mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leadingCoeff_inv g_ne_0)
         g_mul_dvd)
   refine' ⟨map algeq.toAlgHom.toRingHom _, _⟩
-  · -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5072): was `use`
-    exact Classical.choose H
+  · use! Classical.choose H
   · rw [map_map, this]
     exact Classical.choose_spec H
 set_option linter.uppercaseLean3 false in

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1025,16 +1025,12 @@ theorem max_power_factor {a₀ : R} {x : R} (h : a₀ ≠ 0) (hx : Irreducible x
     ∃ n : ℕ, ∃ a : R, ¬x ∣ a ∧ a₀ = x ^ n * a := by
   classical
     let n := (normalizedFactors a₀).count (normalize x)
-    obtain ⟨a, ha1, ha2⟩ :=
-      @exists_eq_pow_mul_and_not_dvd R _ _ x a₀ (ne_top_iff_finite.mp (PartENat.ne_top_iff.mpr _))
+    obtain ⟨a, ha1, ha2⟩ := @exists_eq_pow_mul_and_not_dvd R _ _ x a₀
+      (ne_top_iff_finite.mp (PartENat.ne_top_iff.mpr
+        -- Porting note: this was a hole that was filled at the end of the proof with `use`:
+        ⟨n, multiplicity_eq_count_normalizedFactors hx h⟩))
     simp_rw [← (multiplicity_eq_count_normalizedFactors hx h).symm] at ha1
-    use n
-    use a
-    use ha2
-    rw [ha1]
-    congr
-    use n
-    exact multiplicity_eq_count_normalizedFactors hx h
+    use n, a, ha2, ha1
 #align unique_factorization_monoid.max_power_factor UniqueFactorizationMonoid.max_power_factor