feat(Topology/Compactness/CompactSystem): set system of countable intersections of sets in a compact system is again a compact system

Mathlib.lean

@@ -5625,6 +5625,7 @@ public import Mathlib.NumberTheory.RamificationInertia.Basic
 public import Mathlib.NumberTheory.RamificationInertia.Galois
 public import Mathlib.NumberTheory.RamificationInertia.HilbertTheory
 public import Mathlib.NumberTheory.RamificationInertia.Unramified
+public import Mathlib.NumberTheory.RatFunc.Ostrowski
 public import Mathlib.NumberTheory.Rayleigh
 public import Mathlib.NumberTheory.Real.GoldenRatio
 public import Mathlib.NumberTheory.Real.Irrational
@@ -5997,7 +5998,8 @@ public import Mathlib.Probability.Independence.Integration
 public import Mathlib.Probability.Independence.Kernel
 public import Mathlib.Probability.Independence.Kernel.Indep
 public import Mathlib.Probability.Independence.Kernel.IndepFun
-public import Mathlib.Probability.Independence.Process
+public import Mathlib.Probability.Independence.Process.Basic
+public import Mathlib.Probability.Independence.Process.HasIndepIncrements
 public import Mathlib.Probability.Independence.ZeroOne
 public import Mathlib.Probability.Kernel.Basic
 public import Mathlib.Probability.Kernel.CompProdEqIff

Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

@@ -199,7 +199,7 @@ lemma Submonoid.mem_closure_image_one_lt_iff [CommMonoid S] [IsOrderedCancelMono
     v i ∈ closure (v '' {i | 1 < f (v i)}) ↔ 1 < f (v i) := by
   refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩
   suffices v i = 1 ∨ 1 < f (v i) from this.resolve_left hv_one
-  refine closure_induction (by aesop) (by simp) (fun x y _ _ hx hy ↦ ?_) hi
+  refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi
   rcases hx with rfl | hx; · simpa
   rcases hy with rfl | hy; · right; simpa
   right

Mathlib/Algebra/Order/Group/Indicator.lean

@@ -168,6 +168,20 @@ lemma mulIndicator_iUnion_apply (h1 : (⊥ : M) = 1) (s : ι → Set α) (f : α
     simp only [mem_iUnion, not_exists] at hx
     simp [hx, ← h1]
 
+lemma Set.indicator_iUnion_of_disjoint [AddCommMonoid M] [TopologicalSpace M] (s : δ → Set α) (hs : Pairwise (Disjoint on s)) (f : α → M) (i : α) : (⋃ d, s d).indicator f i = tsum d, (s d).indicator f i := by
+  simp only [Set.indicator, Set.mem_iUnion]
+  by_cases h₀ : ∃ d, i ∈ s d <;> simp only [Set.mem_iUnion, h₀, ↓reduceIte]
+  · obtain ⟨j, hj⟩ := h₀
+    rw [ENNReal.tsum_eq_add_tsum_ite j]
+    simp only [hj, ↓reduceIte]
+    nth_rw 1 [← add_zero (f i)] ; congr
+    apply (ENNReal.tsum_eq_zero.mpr ?_).symm
+    simp only [ite_eq_left_iff, ite_eq_right_iff]
+    exact fun k hk hb ↦ False.elim <| Disjoint.notMem_of_mem_left (hs (id (Ne.symm hk))) hj hb
+  · refine (ENNReal.tsum_eq_zero.mpr (fun j ↦ ?_)).symm
+    push_neg at h₀
+    simp [h₀ j]
+
 variable [Nonempty ι]
 
 @[to_additive]

Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean

@@ -13,17 +13,17 @@ The purpose of this file is to introduce tools which will enable the
 construction of the Dold-Kan equivalence `SimplicialObject C ≌ ChainComplex C ℕ`
 for a pseudoabelian category `C` from the equivalence
 `Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)` and the two
-equivalences `simplicial_object C ≅ Karoubi (SimplicialObject C)` and
-`ChainComplex C ℕ ≅ Karoubi (ChainComplex C ℕ)`.
+equivalences `SimplicialObject C ≌ Karoubi (SimplicialObject C)` and
+`ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`.
 
 It is certainly possible to get an equivalence `SimplicialObject C ≌ ChainComplex C ℕ`
 using a composition of the three equivalences above, but then neither the functor
 nor the inverse would have good definitional properties. For example, it would be better
 if the inverse functor of the equivalence was exactly the functor
-`Γ₀ : SimplicialObject C ⥤ ChainComplex C ℕ` which was constructed in `FunctorGamma.lean`.
+`Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C` which was constructed in `FunctorGamma.lean`.
 
-In this file, given four categories `A`, `A'`, `B`, `B'`, equivalences `eA : A ≅ A'`,
-`eB : B ≅ B'`, `e' : A' ≅ B'`, functors `F : A ⥤ B'`, `G : B ⥤ A` equipped with certain
+In this file, given four categories `A`, `A'`, `B`, `B'`, equivalences `eA : A ≌ A'`,
+`eB : B ≌ B'`, `e' : A' ≌ B'`, functors `F : A ⥤ B'`, `G : B ⥤ A` equipped with certain
 compatibilities, we construct successive equivalences:
 - `equivalence₀` from `A` to `B'`, which is the composition of `eA` and `e'`.
 - `equivalence₁` from `A` to `B'`, with the same inverse functor as `equivalence₀`,
@@ -55,14 +55,14 @@ variable {A A' B B' : Type*} [Category* A] [Category* A'] [Category* B] [Categor
   (eB : B ≌ B') (e' : A' ≌ B') {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) {G : B ⥤ A}
   (hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor)
 
-/-- A basic equivalence `A ≅ B'` obtained by composing `eA : A ≅ A'` and `e' : A' ≅ B'`. -/
+/-- A basic equivalence `A ≌ B'` obtained by composing `eA : A ≌ A'` and `e' : A' ≌ B'`. -/
 @[simps! functor inverse unitIso_hom_app]
 def equivalence₀ : A ≌ B' :=
   eA.trans e'
 
 variable {eA} {e'}
 
-/-- An intermediate equivalence `A ≅ B'` whose functor is `F` and whose inverse is
+/-- An intermediate equivalence `A ≌ B'` whose functor is `F` and whose inverse is
 `e'.inverse ⋙ eA.inverse`. -/
 @[simps! functor]
 def equivalence₁ : A ≌ B' := (equivalence₀ eA e').changeFunctor hF
@@ -104,7 +104,7 @@ theorem equivalence₁UnitIso_eq : (equivalence₁ hF).unitIso = equivalence₁U
   ext X
   simp [equivalence₁]
 
-/-- An intermediate equivalence `A ≅ B` obtained as the composition of `equivalence₁` and
+/-- An intermediate equivalence `A ≌ B` obtained as the composition of `equivalence₁` and
 the inverse of `eB : B ≌ B'`. -/
 @[simps! functor]
 def equivalence₂ : A ≌ B :=
@@ -155,8 +155,8 @@ theorem equivalence₂UnitIso_eq : (equivalence₂ eB hF).unitIso = equivalence
 
 variable {eB}
 
-/-- The equivalence `A ≅ B` whose functor is `F ⋙ eB.inverse` and
-whose inverse is `G : B ≅ A`. -/
+/-- The equivalence `A ≌ B` whose functor is `F ⋙ eB.inverse` and
+whose inverse functor is `G : B ⥤ A`. -/
 @[simps! inverse]
 def equivalence : A ≌ B :=
   ((equivalence₂ eB hF).changeInverse

Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean

@@ -91,7 +91,7 @@ obtained by composing the previous equivalence with the equivalences
 `Karoubi (ChainComplex C ℕ) ≌ ChainComplex C ℕ`. Instead, we polish this construction
 in `Compatibility.lean` by ensuring good definitional properties of the equivalence (e.g.
 the inverse functor is definitionally equal to
-`Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject C`) and
+`Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which is induced by `Γ₀'`) and
 showing compatibilities for the unit and counit isomorphisms.
 
 In this file `Equivalence.lean`, assuming the category `A` is abelian, we obtain

Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

@@ -60,7 +60,7 @@ of the equivalence `ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`. -/
 def N [IsIdempotentComplete C] [HasFiniteCoproducts C] : SimplicialObject C ⥤ ChainComplex C ℕ :=
   N₁ ⋙ (toKaroubiEquivalence _).inverse
 
-/-- The functor `Γ` for the equivalence is `Γ'`. -/
+/-- The functor `Γ` for the equivalence is `Γ₀`. -/
 @[simps!, nolint unusedArguments]
 def Γ [IsIdempotentComplete C] [HasFiniteCoproducts C] : ChainComplex C ℕ ⥤ SimplicialObject C :=
   Γ₀

Mathlib/Analysis/Normed/Group/Indicator.lean

@@ -42,6 +42,21 @@ theorem enorm_indicator_le_enorm_self : ‖indicator s f a‖ₑ ≤ ‖f a‖
   rw [enorm_indicator_eq_indicator_enorm]
   apply indicator_enorm_le_enorm_self
 
+
+lemma Set.indicator_iUnion_of_disjoint (s : δ → Set α) (hs : Pairwise (Disjoint on s)) (f : α → ε) (i : α) : (⋃ d, s d).indicator f i = 1 --∑' (d : α), (s d).indicator f i := by
+  simp only [Set.indicator, Set.mem_iUnion]
+  by_cases h₀ : ∃ d, i ∈ s d <;> simp only [Set.mem_iUnion, h₀, ↓reduceIte]
+  · obtain ⟨j, hj⟩ := h₀
+    rw [ENNReal.tsum_eq_add_tsum_ite j]
+    simp only [hj, ↓reduceIte]
+    nth_rw 1 [← add_zero (f i)] ; congr
+    apply (ENNReal.tsum_eq_zero.mpr ?_).symm
+    simp only [ite_eq_left_iff, ite_eq_right_iff]
+    exact fun k hk hb ↦ False.elim <| Disjoint.notMem_of_mem_left (hs (id (Ne.symm hk))) hj hb
+  · refine (ENNReal.tsum_eq_zero.mpr (fun j ↦ ?_)).symm
+    push_neg at h₀
+    simp [h₀ j]
+
 end ESeminormedAddMonoid
 
 section SeminormedAddGroup

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -830,12 +830,12 @@ lemma Connected.connected_delete_edge_of_not_isBridge (hG : G.Connected) {x y :
   refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩
   obtain ⟨P, hP⟩ := hG.exists_isPath w x
   obtain heP | heP := em' <| s(x, y) ∈ P.edges
-  · exact ⟨(P.toDeleteEdges {s(x, y)} (by aesop)).reverse⟩
+  · exact ⟨(P.toDeleteEdges {s(x, y)} (by grind)).reverse⟩
   have hyP := P.snd_mem_support_of_mem_edges heP
   let P₁ := P.takeUntil y hyP
   have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne
   have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
-  exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by aesop)⟩)
+  exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by grind)⟩)
 
 /-- If `e` is an edge in `G` and is a bridge in a larger graph `G'`, then it's a bridge in `G`. -/
 theorem IsBridge.anti_of_mem_edgeSet {G' : SimpleGraph V} {e : Sym2 V} (hle : G ≤ G')

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -172,7 +172,7 @@ lemma IsMatching.exists_of_disjoint_sets_of_equiv {s t : Set V} (h : Disjoint s
       obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
       · exact hadj ⟨v, _⟩
       · exact (hadj ⟨w, _⟩).symm
-    edge_vert := by aesop }
+    edge_vert := by grind }
   simp only [Subgraph.IsMatching, Set.mem_union, true_and]
   intro v hv
   rcases hv with hl | hr
@@ -368,7 +368,7 @@ lemma IsCycles.existsUnique_ne_adj (h : G.IsCycles) (hadj : G.Adj v w) :
   intro y ⟨hwy, hwy'⟩
   obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)
   simp_rw [← SimpleGraph.mem_neighborSet] at *
-  aesop
+  grind
 
 lemma IsCycles.toSimpleGraph (c : G.ConnectedComponent) (h : G.IsCycles) :
     c.toSimpleGraph.spanningCoe.IsCycles := by
@@ -394,7 +394,7 @@ lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v
     ext w x
     simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
       Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
-    aesop
+    grind
   exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])
 
 lemma Walk.IsCycle.adj_toSubgraph_iff_of_isCycles [LocallyFinite G] {u} {p : G.Walk u u}
@@ -562,19 +562,19 @@ lemma IsAlternating.sup_edge {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G'
   simp only [sup_adj, edge_adj] at hvw hvv'
   obtain hl | hr := hvw <;> obtain h1 | h2 := hvv'
   · exact halt hww' hl h1
-  · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w') = s(u, x))]
+  · rw [G'.adj_congr_of_sym2 (by grind : s(v, w') = s(u, x))]
     simp only [hnadj, not_false_eq_true, iff_true]
     rcases h2.1 with ⟨h2l1, h2l2⟩ | ⟨h2r1, h2r2⟩
     · subst h2l1 h2l2
       exact (hx' _ hww' hl.symm).symm
     · simp_all
-  · rw [G'.adj_congr_of_sym2 (by aesop : s(v, w) = s(u, x))]
+  · rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))]
     simp only [hnadj, false_iff, not_not]
     rcases hr.1 with ⟨hrl1, hrl2⟩ | ⟨hrr1, hrr2⟩
     · subst hrl1 hrl2
       exact (hx' _ hww'.symm h1.symm).symm
-    · aesop
-  · aesop
+    · grind
+  · grind
 
 set_option backward.isDefEq.respectTransparency false in
 lemma Subgraph.IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatching)
@@ -591,7 +591,7 @@ lemma Subgraph.IsPerfectMatching.symmDiff_of_isAlternating (hM : M.IsPerfectMatc
     simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj,
       hmadj.mp hw.1, hw'.2, not_true_eq_false, and_self, not_false_eq_true, or_true, true_and]
     rintro y (hl | hr)
-    · aesop
+    · grind
     · obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
       by_contra! hc
       simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2]

Mathlib/Combinatorics/SimpleGraph/Operations.lean

@@ -72,13 +72,13 @@ theorem edgeSet_replaceVertex_of_not_adj (hn : ¬G.Adj s t) : (G.replaceVertex s
     G.edgeSet \ G.incidenceSet t ∪ (s(·, t)) '' (G.neighborSet s) := by
   ext e; refine e.inductionOn ?_
   simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]
-  intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by aesop]
+  intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by grind]
 
 theorem edgeSet_replaceVertex_of_adj (ha : G.Adj s t) : (G.replaceVertex s t).edgeSet =
     (G.edgeSet \ G.incidenceSet t ∪ (s(·, t)) '' (G.neighborSet s)) \ {s(t, t)} := by
   ext e; refine e.inductionOn ?_
   simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]
-  intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by aesop]
+  intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by grind]
 
 variable [Fintype V] [DecidableRel G.Adj]
 

Mathlib/Combinatorics/SimpleGraph/Tutte.lean

@@ -169,7 +169,7 @@ private theorem tutte_exists_isPerfectMatching_of_near_matchings {x a b c : V}
   -- Neither matching contains the edge that would make the other matching of G perfect
   have hM1nac : ¬M1.Adj a c := fun h ↦ by simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne]
     using h.adj_sub
-  have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by aesop
+  have hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = (G ⊔ edge a c) ⊔ edge x b := by grind
   -- We state conditions for our cycle that hold in all cases and show that this suffices
   suffices ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧
       G'.Adj a c ∧ G' ≤ G ⊔ edge a c by
@@ -228,7 +228,7 @@ private theorem tutte_exists_isPerfectMatching_of_near_matchings {x a b c : V}
     have : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd := by
       apply Walk.toSubgraph_adj_snd
       rw [Walk.nil_takeUntil]
-      aesop
+      grind
     rwa [Walk.snd_takeUntil, hp'.2.1] at this
     simp only [Finset.mem_insert, Finset.mem_singleton] at hx'
     obtain rfl | rfl := hx'

Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

@@ -87,6 +87,10 @@ theorem aeval_X_left_eq_algebraMap (p : K[X]) :
     p.aeval (X : K⟮X⟯) = algebraMap K[X] K⟮X⟯ p := by
   induction p using Polynomial.induction_on' <;> simp_all
 
+@[simp]
+theorem coePolynomial_eq_algebraMap (p : K[X]) :
+    (p : RatFunc K) = algebraMap (Polynomial K) (RatFunc K) p := rfl
+
 @[simp]
 lemma liftRingHom_C {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (x : K) :
     liftRingHom φ hφ (C x) = φ (.C x) :=
@@ -308,51 +312,46 @@ variable {Γ : Type*} [LinearOrderedCommGroupWithZero Γ]
 
 section Algebra
 
-variable (L : Type*) [Field L] [Algebra K L] {v : Valuation L Γ}
-  (hv : ∀ a : K, a ≠ 0 → v (algebraMap K L a) = 1)
-
-include hv
+variable (L : Type*) [Field L] [Algebra K L] {v : Valuation L Γ} [hv : v.IsTrivialOn K]
 
 lemma valuation_aeval_monomial_eq_valuation_pow (w : L) (n : ℕ) {a : K} (ha : a ≠ 0) :
     v ((monomial n a).aeval w) = (v w) ^ n := by
-  simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv a ha]
+  simp [← C_mul_X_pow_eq_monomial, map_mul, map_pow, one_mul, hv.eq_one a ha]
 
 theorem valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (w : L) (hpos : 1 < v w)
     {p : Polynomial K} (hp : p ≠ 0) : v (p.aeval w) = v w ^ p.natDegree := by
-  rw [← valuation_aeval_monomial_eq_valuation_pow _ _ hv _ _ (leadingCoeff_ne_zero.mpr hp)]
+  rw [← valuation_aeval_monomial_eq_valuation_pow _ _ _ _ ((leadingCoeff_ne_zero).mpr hp)]
   nth_rw 1 [as_sum_range p, map_sum]
   apply Valuation.map_sum_eq_of_lt _ (by simp)
   intro i hi
   simp only [Finset.mem_sdiff, Finset.mem_range, Nat.lt_add_one_iff, Finset.mem_singleton,
     ← lt_iff_le_and_ne] at hi
   simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree]
   by_cases h0 : (p.coeff i) = 0
-  · simp [h0, map_zero, zero_mul, one_mul, hv p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
+  · simp [h0, map_zero, zero_mul, one_mul, hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
       pow_pos (lt_trans zero_lt_one hpos) p.natDegree]
-  · simp [one_mul, hv p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
-      hv _ h0, one_mul, pow_lt_pow_right₀ hpos hi]
+  · simp [one_mul, hv.eq_one p.leadingCoeff ((leadingCoeff_ne_zero).mpr hp),
+      hv.eq_one _ h0, one_mul, pow_lt_pow_right₀ hpos hi]
 
 end Algebra
 
-variable {v : Valuation K⟮X⟯ Γ} (hv : ∀ a : K, a ≠ 0 → v (C a) = 1)
+variable {v : Valuation K⟮X⟯ Γ} [hv : v.IsTrivialOn K]
 
 open Valuation
 
-include hv
-
 /-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
 `(monomial n a)` is equal to `(v RatFunc.X) ^ n`. -/
 lemma valuation_monomial_eq_valuation_X_pow (n : ℕ) {a : K} (ha : a ≠ 0) :
     v (monomial n a) = v RatFunc.X ^ n := by
-  simp_all [RatFunc.coePolynomial, ← C_mul_X_pow_eq_monomial]
+  simp_all [← RatFunc.algebraMap_eq_C, hv.eq_one]
 
 /-- If a valuation `v` is trivial on constants and `1 < v RatFunc.X` then for every polynomial `p`,
 `v p = v RatFunc.X ^ p.natDegree`.
 
 Note: The condition `1 < v RatFunc.X` is typically satisfied by the valuation at infinity. -/
-theorem valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (hlt : 1 < v RatFunc.X)
-    {p : K[X]} (hp : p ≠ 0) : v p = v RatFunc.X ^ p.natDegree := by
-  convert valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X K K⟮X⟯ hv
+theorem valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
+     (hlt : 1 < v RatFunc.X) {p : K[X]} (hp : p ≠ 0) : v p = v RatFunc.X ^ p.natDegree := by
+  convert valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X K K⟮X⟯
     RatFunc.X hlt hp
   ext p
   nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]
@@ -368,14 +367,14 @@ theorem valuation_le_one_of_valuation_X_le_one (hle : v RatFunc.X ≤ 1) (p : K[
   by_cases h0 : p.coeff i = 0
   · simp_all
   · rw [← RatFunc.coePolynomial]
-    simp_all [valuation_monomial_eq_valuation_X_pow, pow_le_one']
+    simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0]
 
 /-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
 `1 / (monomial n a)` (as an element of the field of rational functions) is equal
 to `(v RatFunc.X) ^ (- n)`. -/
 lemma valuation_inv_monomial_eq_valuation_X_zpow (n : ℕ) {a : K} (ha : a ≠ 0) :
     v (1 / monomial n a) = v RatFunc.X ^ (-(n : ℤ)) := by
-  simpa using valuation_monomial_eq_valuation_X_pow _ hv n ha
+  simp [← RatFunc.algebraMap_eq_C, hv.eq_one _ ha]
 
 end TrivialOnConstants
 

Mathlib/FieldTheory/RatFunc/Degree.lean

@@ -82,6 +82,12 @@ theorem intDegree_mul {x y : K⟮X⟯} (hx : x ≠ 0) (hy : y ≠ 0) :
 theorem intDegree_inv (x : K⟮X⟯) : intDegree (x⁻¹) = - intDegree x := by
   by_cases hx : x = 0 <;> simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]
 
+set_option backward.isDefEq.respectTransparency false in
+lemma intDegree_div {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) :
+    (x / y).intDegree = x.intDegree - y.intDegree := by
+  rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg] <;> grind
+
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem intDegree_neg (x : K⟮X⟯) : intDegree (-x) = intDegree x := by
   by_cases hx : x = 0

Mathlib/LinearAlgebra/RootSystem/Base.lean

@@ -258,7 +258,7 @@ lemma sub_notMem_range_root
   have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
     have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
     rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
-      Finset.sum_insert (by aesop), Finset.sum_singleton]
+      Finset.sum_insert (by grind), Finset.sum_singleton]
     simp [f, hij, sub_eq_add_neg]
   intro contra
   rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg

Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean

@@ -560,7 +560,7 @@ lemma mem_allRoots (i : ι) :
     simp only [LinearMap.zero_apply]
     induction hx using Submodule.span_induction with
     | zero => simp
-    | mem => aesop
+    | mem => grind
     | add => simp_all
     | smul => simp_all
   simpa using LinearMap.congr_fun key (P.root i)