chore(Archive,Counterexamples): use Type* not Type _ (leanprover-community#7663)

eric-wieser · eric-wieser · commit 8437cdac90ba · 2023-10-14T06:04:53.000Z
This is an exhaustive replacement.
diff --git a/Archive/Examples/PropEncodable.lean b/Archive/Examples/PropEncodable.lean
@@ -30,7 +30,7 @@ show encodability.
 namespace PropEncodable
 
 /-- Propositional formulas with labels from `α`. -/
-inductive PropForm (α : Type _)
+inductive PropForm (α : Type*)
   | var : α → PropForm α
   | not : PropForm α → PropForm α
   | and : PropForm α → PropForm α → PropForm α
@@ -49,7 +49,7 @@ The next three functions make it easier to construct functions from a small
 
 namespace PropForm
 
-private def Constructors (α : Type _) :=
+private def Constructors (α : Type*) :=
   α ⊕ (Unit ⊕ (Unit ⊕ Unit))
 
 local notation "cvar " a => Sum.inl a
@@ -61,13 +61,13 @@ local notation "cand" => Sum.inr (Sum.inr (Sum.inr Unit.unit))
 local notation "cor" => Sum.inr (Sum.inr (Sum.inl Unit.unit))
 
 @[simp]
-private def arity (α : Type _) : Constructors α → Nat
+private def arity (α : Type*) : Constructors α → Nat
   | cvar _ => 0
   | cnot => 1
   | cand => 2
   | cor => 2
 
-variable {α : Type _}
+variable {α : Type*}
 
 instance : ∀ c : Unit ⊕ (Unit ⊕ Unit), NeZero (arity α (.inr c))
   | .inl () => ⟨one_ne_zero⟩
diff --git a/Archive/Imo/Imo1962Q4.lean b/Archive/Imo/Imo1962Q4.lean
@@ -106,7 +106,7 @@ We now present a second solution.  The key to this solution is that, when the id
 converted to an identity which is polynomial in `a` := `cos x`, it can be rewritten as a product of
 terms, `a ^ 2 * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3)`, being equal to zero.
 -/
-theorem formula {R : Type _} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
+theorem formula {R : Type*} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
     a ^ 2 + ((2 : R) * a ^ 2 - (1 : R)) ^ 2 + ((4 : R) * a ^ 3 - 3 * a) ^ 2 = 1 ↔
       ((2 : R) * a ^ 2 - (1 : R)) * ((4 : R) * a ^ 3 - 3 * a) = 0 := by
   constructor <;> intro h
diff --git a/Archive/Imo/Imo1987Q1.lean b/Archive/Imo/Imo1987Q1.lean
@@ -25,7 +25,7 @@ holds true for `n = 0` as well, so we first prove it, then deduce the original v
 `n ≥ 1`. -/
 
 
-variable (α : Type _) [Fintype α] [DecidableEq α]
+variable (α : Type*) [Fintype α] [DecidableEq α]
 
 open scoped BigOperators Nat
 
@@ -54,7 +54,7 @@ theorem card_fixed_points :
     Finset.filter_eq', Finset.card_univ]
 #align imo1987_q1.card_fixed_points Imo1987Q1.card_fixed_points
 
-/-- Given `α : Type _` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
+/-- Given `α : Type*` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
 fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
@@ -91,7 +91,7 @@ def fixedPointsEquiv' :
   right_inv := fun ⟨⟨x, σ⟩, h⟩ => rfl
 #align imo1987_q1.fixed_points_equiv' Imo1987Q1.fixedPointsEquiv'
 
-/-- Main statement for any `(α : Type _) [Fintype α]`. -/
+/-- Main statement for any `(α : Type*) [Fintype α]`. -/
 theorem main_fintype : ∑ k in range (card α + 1), k * p α k = card α * (card α - 1)! := by
   have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
   simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,
diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
@@ -45,19 +45,19 @@ set_option linter.uppercaseLean3 false
 
 open scoped Classical
 
-variable {C J : Type _} (r : C → J → Prop)
+variable {C J : Type*} (r : C → J → Prop)
 
 namespace Imo1998Q2
 
 noncomputable section
 
 /-- An ordered pair of judges. -/
-abbrev JudgePair (J : Type _) :=
+abbrev JudgePair (J : Type*) :=
   J × J
 #align imo1998_q2.judge_pair Imo1998Q2.JudgePair
 
 /-- A triple consisting of contestant together with an ordered pair of judges. -/
-abbrev AgreedTriple (C J : Type _) :=
+abbrev AgreedTriple (C J : Type*) :=
   C × JudgePair J
 #align imo1998_q2.agreed_triple Imo1998Q2.AgreedTriple
 
@@ -168,7 +168,7 @@ theorem A_card_upper_bound {k : ℕ}
 
 end
 
-theorem add_sq_add_sq_sub {α : Type _} [Ring α] (x y : α) :
+theorem add_sq_add_sq_sub {α : Type*} [Ring α] (x y : α) :
     (x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y := by noncomm_ring
 #align imo1998_q2.add_sq_add_sq_sub Imo1998Q2.add_sq_add_sq_sub
 
diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -67,7 +67,7 @@ set_option linter.uppercaseLean3 false
 
 attribute [local instance] FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two
 
-variable (V : Type _) (Pt : Type _)
+variable (V : Type*) (Pt : Type*)
 
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
 
diff --git a/Archive/OxfordInvariants/Summer2021/Week3P1.lean b/Archive/OxfordInvariants/Summer2021/Week3P1.lean
@@ -71,7 +71,7 @@ natural.
 
 open scoped BigOperators
 
-variable {α : Type _} [LinearOrderedField α]
+variable {α : Type*} [LinearOrderedField α]
 
 theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤ n, 0 < a i)
     (ha : ∀ i, i + 2 ≤ n → a (i + 1) ∣ a i + a (i + 2)) :
diff --git a/Archive/Wiedijk100Theorems/AbelRuffini.lean b/Archive/Wiedijk100Theorems/AbelRuffini.lean
@@ -39,7 +39,7 @@ open scoped Polynomial
 
 attribute [local instance] splits_ℚ_ℂ
 
-variable (R : Type _) [CommRing R] (a b : ℕ)
+variable (R : Type*) [CommRing R] (a b : ℕ)
 
 /-- A quintic polynomial that we will show is irreducible -/
 noncomputable def Φ : R[X] :=
@@ -49,7 +49,7 @@ noncomputable def Φ : R[X] :=
 variable {R}
 
 @[simp]
-theorem map_Phi {S : Type _} [CommRing S] (f : R →+* S) : (Φ R a b).map f = Φ S a b := by simp [Φ]
+theorem map_Phi {S : Type*} [CommRing S] (f : R →+* S) : (Φ R a b).map f = Φ S a b := by simp [Φ]
 #align abel_ruffini.map_Phi AbelRuffini.map_Phi
 
 @[simp]
diff --git a/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean b/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean
@@ -24,7 +24,7 @@ sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Er
 -/
 
 
-variable {α : Type _} [LinearOrder α] {β : Type _}
+variable {α : Type*} [LinearOrder α] {β : Type*}
 
 open Function Finset
 
diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -252,7 +252,7 @@ theorem first_vote_pos :
     · simp
 #align ballot.first_vote_pos Ballot.first_vote_pos
 
-theorem headI_mem_of_nonempty {α : Type _} [Inhabited α] : ∀ {l : List α} (_ : l ≠ []), l.headI ∈ l
+theorem headI_mem_of_nonempty {α : Type*} [Inhabited α] : ∀ {l : List α} (_ : l ≠ []), l.headI ∈ l
   | [], h => (h rfl).elim
   | x::l, _ => List.mem_cons_self x l
 #align ballot.head_mem_of_nonempty Ballot.headI_mem_of_nonempty
diff --git a/Archive/Wiedijk100Theorems/HeronsFormula.lean b/Archive/Wiedijk100Theorems/HeronsFormula.lean
@@ -31,7 +31,7 @@ namespace Theorems100
 
 local notation "√" => Real.sqrt
 
-variable {V : Type _} {P : Type _} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
   [NormedAddTorsor V P]
 
 /-- **Heron's formula**: The area of a triangle with side lengths `a`, `b`, and `c` is
diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean
@@ -60,7 +60,7 @@ namespace Theorems100
 
 noncomputable section
 
-variable {α : Type _}
+variable {α : Type*}
 
 open Finset
 
@@ -97,14 +97,14 @@ Every function in here is finitely supported, and the support is a subset of `s`
 This should be thought of as a generalisation of `Finset.Nat.antidiagonalTuple` where
 `antidiagonalTuple k n` is the same thing as `cut (s : Finset.univ (Fin k)) n`.
 -/
-def cut {ι : Type _} (s : Finset ι) (n : ℕ) : Finset (ι → ℕ) :=
+def cut {ι : Type*} (s : Finset ι) (n : ℕ) : Finset (ι → ℕ) :=
   Finset.filter (fun f => s.sum f = n)
     ((s.pi fun _ => range (n + 1)).map
       ⟨fun f i => if h : i ∈ s then f i h else 0, fun f g h => by
         ext i hi; simpa [dif_pos hi] using congr_fun h i⟩)
 #align theorems_100.cut Theorems100.cut
 
-theorem mem_cut {ι : Type _} (s : Finset ι) (n : ℕ) (f : ι → ℕ) :
+theorem mem_cut {ι : Type*} (s : Finset ι) (n : ℕ) (f : ι → ℕ) :
     f ∈ cut s n ↔ s.sum f = n ∧ ∀ i, i ∉ s → f i = 0 := by
   rw [cut, mem_filter, and_comm, and_congr_right]
   intro h
@@ -136,7 +136,7 @@ theorem cut_univ_fin_eq_antidiagonalTuple (n : ℕ) (k : ℕ) :
 
 /-- There is only one `cut` of 0. -/
 @[simp]
-theorem cut_zero {ι : Type _} (s : Finset ι) : cut s 0 = {0} := by
+theorem cut_zero {ι : Type*} (s : Finset ι) : cut s 0 = {0} := by
   -- In general it's nice to prove things using `mem_cut` but in this case it's easier to just
   -- use the definition.
   rw [cut, range_one, pi_const_singleton, map_singleton, Function.Embedding.coeFn_mk,
@@ -148,14 +148,14 @@ theorem cut_zero {ι : Type _} (s : Finset ι) : cut s 0 = {0} := by
 #align theorems_100.cut_zero Theorems100.cut_zero
 
 @[simp]
-theorem cut_empty_succ {ι : Type _} (n : ℕ) : cut (∅ : Finset ι) (n + 1) = ∅ := by
+theorem cut_empty_succ {ι : Type*} (n : ℕ) : cut (∅ : Finset ι) (n + 1) = ∅ := by
   apply eq_empty_of_forall_not_mem
   intro x hx
   rw [mem_cut, sum_empty] at hx
   cases hx.1
 #align theorems_100.cut_empty_succ Theorems100.cut_empty_succ
 
-theorem cut_insert {ι : Type _} (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s) :
+theorem cut_insert {ι : Type*} (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s) :
     cut (insert a s) n =
       (Nat.antidiagonal n).biUnion fun p : ℕ × ℕ =>
         (cut s p.snd).map
@@ -192,7 +192,7 @@ theorem cut_insert {ι : Type _} (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s
       simp [if_neg h₁, hg₂ _ h₂]
 #align theorems_100.cut_insert Theorems100.cut_insert
 
-theorem coeff_prod_range [CommSemiring α] {ι : Type _} (s : Finset ι) (f : ι → PowerSeries α)
+theorem coeff_prod_range [CommSemiring α] {ι : Type*} (s : Finset ι) (f : ι → PowerSeries α)
     (n : ℕ) : coeff α n (∏ j in s, f j) = ∑ l in cut s n, ∏ i in s, coeff α (l i) (f i) := by
   revert n
   induction s using Finset.induction_on with
@@ -227,7 +227,7 @@ theorem coeff_prod_range [CommSemiring α] {ι : Type _} (s : Finset ι) (f : ι
 #align theorems_100.coeff_prod_range Theorems100.coeff_prod_range
 
 /-- A convenience constructor for the power series whose coefficients indicate a subset. -/
-def indicatorSeries (α : Type _) [Semiring α] (s : Set ℕ) : PowerSeries α :=
+def indicatorSeries (α : Type*) [Semiring α] (s : Set ℕ) : PowerSeries α :=
   PowerSeries.mk fun n => if n ∈ s then 1 else 0
 #align theorems_100.indicator_series Theorems100.indicatorSeries
 
@@ -309,7 +309,7 @@ def mkOdd : ℕ ↪ ℕ :=
 #align theorems_100.mk_odd Theorems100.mkOdd
 
 -- The main workhorse of the partition theorem proof.
-theorem partialGF_prop (α : Type _) [CommSemiring α] (n : ℕ) (s : Finset ℕ) (hs : ∀ i ∈ s, 0 < i)
+theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ) (hs : ∀ i ∈ s, 0 < i)
     (c : ℕ → Set ℕ) (hc : ∀ i, i ∉ s → 0 ∈ c i) :
     (Finset.card
           ((univ : Finset (Nat.Partition n)).filter fun p =>
diff --git a/Archive/Wiedijk100Theorems/SolutionOfCubic.lean b/Archive/Wiedijk100Theorems/SolutionOfCubic.lean
@@ -43,7 +43,7 @@ section Field
 
 open Polynomial
 
-variable {K : Type _} [Field K]
+variable {K : Type*} [Field K]
 
 variable [Invertible (2 : K)] [Invertible (3 : K)]
 
diff --git a/Counterexamples/HomogeneousPrimeNotPrime.lean b/Counterexamples/HomogeneousPrimeNotPrime.lean
@@ -58,7 +58,7 @@ instance : LinearOrderedAddCommMonoid Two :=
       delta Two WithZero; decide }
 section
 
-variable (R : Type _) [CommRing R]
+variable (R : Type*) [CommRing R]
 
 /-- The grade 0 part of `R²` is `{(a, a) | a ∈ R}`. -/
 def submoduleZ : Submodule R (R × R) where
diff --git a/Counterexamples/QuadraticForm.lean b/Counterexamples/QuadraticForm.lean
@@ -18,7 +18,7 @@ The counterexample we use is $B (x, y) (x', y') ↦ xy' + x'y$ where `x y x' y'
 -/
 
 
-variable (F : Type _) [Nontrivial F] [CommRing F] [CharP F 2]
+variable (F : Type*) [Nontrivial F] [CommRing F] [CharP F 2]
 
 open BilinForm
 
