chore: use inferInstanceAs (#2074)

Drop

* `by delta mydef; infer_instance`. This generates `id _` in the proof.

* `show _, by infer_instance`. This generates `let` in `let`; not sure if it's bad for defeq but a reducible `inferInstanceAs` should not be worse.

Mathlib/Algebra/DirectSum/Basic.lean

@@ -44,14 +44,14 @@ def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
 
 -- Porting note: Added inhabited instance manually
 instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
-  by delta DirectSum; infer_instance
+  inferInstanceAs (Inhabited (Π₀ i, β i))
 
 -- Porting note: Added addCommMonoid instance manually
 instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
-  by delta DirectSum; infer_instance
+  inferInstanceAs (AddCommMonoid (Π₀ i, β i))
 
 instance [∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i :=
-  by delta DirectSum; infer_instance
+  inferInstanceAs (CoeFun (Π₀ i, β i) fun _ => ∀ i : ι, β i)
 
 -- Porting note: scoped does not work with notation3; TODO rewrite as lean4 notation?
 -- scoped[DirectSum]
@@ -79,7 +79,7 @@ section AddCommGroup
 variable [∀ i, AddCommGroup (β i)]
 
 instance : AddCommGroup (DirectSum ι β) :=
-  by delta DirectSum; infer_instance
+  inferInstanceAs (AddCommGroup (Π₀ i, β i))
 variable {β}
 
 @[simp]

Mathlib/Algebra/Group/ConjFinite.lean

@@ -27,9 +27,8 @@ instance [Fintype α] [DecidableRel (IsConj : α → α → Prop)] : Fintype (Co
 instance [Finite α] : Finite (ConjClasses α) :=
   Quotient.finite _
 
-instance [DecidableEq α] [Fintype α] : DecidableRel (IsConj : α → α → Prop) := fun a b => by
-  delta IsConj SemiconjBy
-  infer_instance
+instance [DecidableEq α] [Fintype α] : DecidableRel (IsConj : α → α → Prop) := fun a b =>
+  inferInstanceAs (Decidable (∃ c : αˣ, c.1 * a = b * c.1))
 
 instance conjugatesOf.fintype [Fintype α] [DecidableRel (IsConj : α → α → Prop)] {a : α} :
   Fintype (conjugatesOf a) :=

Mathlib/Algebra/GroupRingAction/Subobjects.lean

@@ -30,8 +30,7 @@ variable [Monoid M] [Group G] [Semiring R]
 /-- A stronger version of `Submonoid.distribMulAction`. -/
 instance Submonoid.mulSemiringAction [MulSemiringAction M R] (H : Submonoid M) :
     MulSemiringAction H R :=
-  { show MulDistribMulAction H R by infer_instance,
-    show DistribMulAction H R by infer_instance
+  { inferInstanceAs (DistribMulAction H R), inferInstanceAs (MulDistribMulAction H R)
     with smul := (· • ·) }
 #align submonoid.mul_semiring_action Submonoid.mulSemiringAction
 

Mathlib/Algebra/Star/Basic.lean

@@ -456,8 +456,8 @@ namespace StarOrderedRing
 -- see note [lower instance priority]
 instance (priority := 100) [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R] :
     OrderedAddCommGroup R :=
-  { show NonUnitalRing R by infer_instance, show PartialOrder R by infer_instance,
-    show StarOrderedRing R by infer_instance with }
+  { inferInstanceAs (NonUnitalRing R), inferInstanceAs (PartialOrder R),
+    inferInstanceAs (StarOrderedRing R) with }
 
 end StarOrderedRing
 

Mathlib/Algebra/Star/Prod.lean

@@ -51,8 +51,8 @@ instance [AddMonoid R] [AddMonoid S] [StarAddMonoid R] [StarAddMonoid S] : StarA
     where star_add _ _ := Prod.ext (star_add _ _) (star_add _ _)
 
 instance [NonUnitalSemiring R] [NonUnitalSemiring S] [StarRing R] [StarRing S] : StarRing (R × S) :=
-  { (show StarAddMonoid (R × S) by infer_instance),
-    (show StarSemigroup (R × S) by infer_instance) with }
+  { inferInstanceAs (StarAddMonoid (R × S)),
+    inferInstanceAs (StarSemigroup (R × S)) with }
 
 instance {α : Type w} [SMul α R] [SMul α S] [Star α] [Star R] [Star S]
     [StarModule α R] [StarModule α S] : StarModule α (R × S)

Mathlib/Algebra/Star/Unitary.lean

@@ -155,7 +155,7 @@ section CommMonoid
 variable [CommMonoid R] [StarSemigroup R]
 
 instance : CommGroup (unitary R) :=
-  { show Group (unitary R) by infer_instance, Submonoid.toCommMonoid _ with }
+  { inferInstanceAs (Group (unitary R)), Submonoid.toCommMonoid _ with }
 
 theorem mem_iff_star_mul_self {U : R} : U ∈ unitary R ↔ star U * U = 1 :=
   mem_iff.trans <| and_iff_left_of_imp fun h => mul_comm (star U) U ▸ h

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -89,7 +89,7 @@ theorem mem_mk (c : ℕ × ℕ) (cells) (isLowerSet) :
 #align young_diagram.mem_mk YoungDiagram.mem_mk
 
 instance decidableMem (μ : YoungDiagram) : DecidablePred (· ∈ μ) :=
-  show DecidablePred (· ∈ μ.cells) by infer_instance
+  inferInstanceAs (DecidablePred (· ∈ μ.cells))
 #align young_diagram.decidable_mem YoungDiagram.decidableMem
 
 /-- In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2)

Mathlib/Data/ENat/Basic.lean

@@ -43,10 +43,10 @@ instance : Coe ℕ ℕ∞ := ⟨ofNat⟩
 --Porting note: instances that derive failed to find
 instance : OrderBot ℕ∞ := WithTop.orderBot
 instance : OrderTop ℕ∞ := WithTop.orderTop
-instance : OrderedSub ℕ∞ := by delta ENat; infer_instance
-instance : SuccOrder ℕ∞ := by delta ENat; infer_instance
-instance : WellFoundedLT ℕ∞ := by delta ENat; infer_instance
-instance : CharZero ℕ∞ := by delta ENat; infer_instance
+instance : OrderedSub ℕ∞ := inferInstanceAs (OrderedSub (WithTop ℕ))
+instance : SuccOrder ℕ∞ := inferInstanceAs (SuccOrder (WithTop ℕ))
+instance : WellFoundedLT ℕ∞ := inferInstanceAs (WellFoundedLT (WithTop ℕ))
+instance : CharZero ℕ∞ := inferInstanceAs (CharZero (WithTop ℕ))
 instance : IsWellOrder ℕ∞ (· < ·) where
 
 variable {m n : ℕ∞}

Mathlib/Data/ENat/Lattice.lean

@@ -19,4 +19,5 @@ This instance is not in `Data.ENat.Basic` to avoid dependency on `Finset`s.
 
 -- porting notes: was `deriving instance` but "default handlers have not been implemented yet"
 -- porting notes: `noncomputable` through 'Nat.instConditionallyCompleteLinearOrderBotNat'
-noncomputable instance : CompleteLinearOrder ENat := by delta ENat; infer_instance
+noncomputable instance : CompleteLinearOrder ENat :=
+  inferInstanceAs (CompleteLinearOrder (WithTop ℕ))

Mathlib/Data/Fintype/Basic.lean

@@ -129,7 +129,7 @@ theorem subset_univ (s : Finset α) : s ⊆ univ := fun a _ => mem_univ a
 #align finset.subset_univ Finset.subset_univ
 
 instance : BoundedOrder (Finset α) :=
-  { (show OrderBot (Finset α) by infer_instance) with
+  { inferInstanceAs (OrderBot (Finset α)) with
     top := univ
     le_top := subset_univ }
 

Mathlib/Data/Nat/GCD/Basic.lean

@@ -107,7 +107,7 @@ theorem lcm_dvd_iff {m n k : ℕ} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
 See also `Nat.coprime_of_dvd` and `Nat.coprime_of_dvd'` to prove `Nat.coprime m n`.
 -/
 
-instance (m n : ℕ) : Decidable (coprime m n) := by unfold coprime ;infer_instance
+instance (m n : ℕ) : Decidable (coprime m n) := inferInstanceAs (Decidable (gcd m n = 1))
 
 theorem coprime.lcm_eq_mul {m n : ℕ} (h : coprime m n) : lcm m n = m * n := by
   rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]

Mathlib/Data/Vector.lean

@@ -30,9 +30,8 @@ variable {α : Type u} {β : Type v} {φ : Type w}
 
 variable {n : ℕ}
 
-instance [DecidableEq α] : DecidableEq (Vector α n) := by
-  unfold Vector
-  infer_instance
+instance [DecidableEq α] : DecidableEq (Vector α n) :=
+  inferInstanceAs (DecidableEq {l : List α // l.length = n})
 
 /-- The empty vector with elements of type `α` -/
 @[match_pattern]

Mathlib/Data/ZMod/Defs.lean

@@ -89,8 +89,8 @@ def ZMod : ℕ → Type
 #align zmod ZMod
 
 instance ZMod.decidableEq : ∀ n : ℕ, DecidableEq (ZMod n)
-  | 0 => by dsimp [ZMod]; infer_instance
-  | n + 1 => by dsimp [ZMod]; infer_instance
+  | 0 => inferInstanceAs (DecidableEq ℤ)
+  | n + 1 => inferInstanceAs (DecidableEq (Fin (n + 1)))
 #align zmod.decidable_eq ZMod.decidableEq
 
 instance ZMod.repr : ∀ n : ℕ, Repr (ZMod n)

Mathlib/GroupTheory/Subgroup/Actions.lean

@@ -30,7 +30,7 @@ variable {α β : Type _}
 /-- The action by a subgroup is the action by the underlying group. -/
 @[to_additive "The additive action by an add_subgroup is the action by the underlying `AddGroup`. "]
 instance [MulAction G α] (S : Subgroup G) : MulAction S α :=
-  show MulAction S.toSubmonoid α by infer_instance
+  inferInstanceAs (MulAction S.toSubmonoid α)
 
 @[to_additive]
 theorem smul_def [MulAction G α] {S : Subgroup G} (g : S) (m : α) : g • m = (g : G) • m :=
@@ -55,18 +55,18 @@ instance smulCommClass_right [SMul α β] [MulAction G β] [SMulCommClass α G 
 /-- Note that this provides `IsScalarTower S G G` which is needed by `smul_mul_assoc`. -/
 instance [SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) :
     IsScalarTower S α β :=
-  show IsScalarTower S.toSubmonoid α β by infer_instance
+  inferInstanceAs (IsScalarTower S.toSubmonoid α β)
 
 instance [MulAction G α] [FaithfulSMul G α] (S : Subgroup G) : FaithfulSMul S α :=
-  show FaithfulSMul S.toSubmonoid α by infer_instance
+  inferInstanceAs (FaithfulSMul S.toSubmonoid α)
 
 /-- The action by a subgroup is the action by the underlying group. -/
 instance [AddMonoid α] [DistribMulAction G α] (S : Subgroup G) : DistribMulAction S α :=
-  show DistribMulAction S.toSubmonoid α by infer_instance
+  inferInstanceAs (DistribMulAction S.toSubmonoid α)
 
 /-- The action by a subgroup is the action by the underlying group. -/
 instance [Monoid α] [MulDistribMulAction G α] (S : Subgroup G) : MulDistribMulAction S α :=
-  show MulDistribMulAction S.toSubmonoid α by infer_instance
+  inferInstanceAs (MulDistribMulAction S.toSubmonoid α)
 
 /-- The center of a group acts commutatively on that group. -/
 instance center.smulCommClass_left : SMulCommClass (center G) G G :=

Mathlib/GroupTheory/Submonoid/Inverses.lean

@@ -44,8 +44,8 @@ noncomputable instance [Monoid M] : Group (IsUnit.submonoid M) :=
 
 @[to_additive]
 noncomputable instance [CommMonoid M] : CommGroup (IsUnit.submonoid M) :=
-  { show Group (IsUnit.submonoid M) by infer_instance
-      with mul_comm := fun a b ↦ by convert mul_comm a b }
+  { inferInstanceAs (Group (IsUnit.submonoid M)) with
+    mul_comm := fun a b ↦ by convert mul_comm a b }
 
 @[to_additive]
 theorem IsUnit.Submonoid.coe_inv [Monoid M] (x : IsUnit.submonoid M) :

Mathlib/Order/Atoms.lean

@@ -579,8 +579,7 @@ def orderIsoBool : α ≃o Bool :=
 /-- A simple `BoundedOrder` is also a `BooleanAlgebra`. -/
 protected def booleanAlgebra {α} [DecidableEq α] [Lattice α] [BoundedOrder α] [IsSimpleOrder α] :
     BooleanAlgebra α :=
-  { show BoundedOrder α by infer_instance,
-    IsSimpleOrder.distribLattice with
+  { inferInstanceAs (BoundedOrder α), IsSimpleOrder.distribLattice with
     compl := fun x => if x = ⊥ then ⊤ else ⊥
     sdiff := fun x y => if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥
     sdiff_eq := fun x y => by

Mathlib/RingTheory/Congruence.lean

@@ -190,16 +190,14 @@ section add_mul
 
 variable [Add R] [Mul R] (c : RingCon R)
 
-instance : Add c.Quotient :=
-  show Add c.toAddCon.Quotient by infer_instance
+instance : Add c.Quotient := inferInstanceAs (Add c.toAddCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_add (x y : R) : (↑(x + y) : c.Quotient) = ↑x + ↑y :=
   rfl
 #align ring_con.coe_add RingCon.coe_add
 
-instance : Mul c.Quotient :=
-  show Mul c.toCon.Quotient by infer_instance
+instance : Mul c.Quotient := inferInstanceAs (Mul c.toCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_mul (x y : R) : (↑(x * y) : c.Quotient) = ↑x * ↑y :=
@@ -212,8 +210,7 @@ section Zero
 
 variable [AddZeroClass R] [Mul R] (c : RingCon R)
 
-instance : Zero c.Quotient :=
-  show Zero c.toAddCon.Quotient by infer_instance
+instance : Zero c.Quotient := inferInstanceAs (Zero c.toAddCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_zero : (↑(0 : R) : c.Quotient) = 0 :=
@@ -226,8 +223,7 @@ section One
 
 variable [Add R] [MulOneClass R] (c : RingCon R)
 
-instance : One c.Quotient :=
-  show One c.toCon.Quotient by infer_instance
+instance : One c.Quotient := inferInstanceAs (One c.toCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_one : (↑(1 : R) : c.Quotient) = 1 :=
@@ -240,8 +236,7 @@ section SMul
 
 variable [Add R] [MulOneClass R] [SMul α R] [IsScalarTower α R R] (c : RingCon R)
 
-instance : SMul α c.Quotient :=
-  show SMul α c.toCon.Quotient by infer_instance
+instance : SMul α c.Quotient := inferInstanceAs (SMul α c.toCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_smul (a : α) (x : R) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient) :=
@@ -254,24 +249,21 @@ section NegSubZsmul
 
 variable [AddGroup R] [Mul R] (c : RingCon R)
 
-instance : Neg c.Quotient :=
-  show Neg c.toAddCon.Quotient by infer_instance
+instance : Neg c.Quotient := inferInstanceAs (Neg c.toAddCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_neg (x : R) : (↑(-x) : c.Quotient) = -x :=
   rfl
 #align ring_con.coe_neg RingCon.coe_neg
 
-instance : Sub c.Quotient :=
-  show Sub c.toAddCon.Quotient by infer_instance
+instance : Sub c.Quotient := inferInstanceAs (Sub c.toAddCon.Quotient)
 
 @[simp, norm_cast]
 theorem coe_sub (x y : R) : (↑(x - y) : c.Quotient) = x - y :=
   rfl
 #align ring_con.coe_sub RingCon.coe_sub
 
-instance hasZsmul : SMul ℤ c.Quotient :=
-  show SMul ℤ c.toAddCon.Quotient by infer_instance
+instance hasZsmul : SMul ℤ c.Quotient := inferInstanceAs (SMul ℤ c.toAddCon.Quotient)
 #align ring_con.has_zsmul RingCon.hasZsmul
 
 @[simp, norm_cast]
@@ -285,8 +277,7 @@ section Nsmul
 
 variable [AddMonoid R] [Mul R] (c : RingCon R)
 
-instance hasNsmul : SMul ℕ c.Quotient :=
-  show SMul ℕ c.toAddCon.Quotient by infer_instance
+instance hasNsmul : SMul ℕ c.Quotient := inferInstanceAs (SMul ℕ c.toAddCon.Quotient)
 #align ring_con.has_nsmul RingCon.hasNsmul
 
 @[simp, norm_cast]
@@ -300,8 +291,7 @@ section Pow
 
 variable [Add R] [Monoid R] (c : RingCon R)
 
-instance : Pow c.Quotient ℕ :=
-  show Pow c.toCon.Quotient ℕ by infer_instance
+instance : Pow c.Quotient ℕ := inferInstanceAs (Pow c.toCon.Quotient ℕ)
 
 @[simp, norm_cast]
 theorem coe_pow (x : R) (n : ℕ) : (↑(x ^ n) : c.Quotient) = (x : c.Quotient) ^ n :=