mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case cpos.a
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := ⋯
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
h : ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) = 0
i' : ν.IsOpenPosMeasure
⊢ (interior ↑K).Nonempty

pp: case cpos.a
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := ⋯
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
h : ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) = 0
i' : ν.IsOpenPosMeasure
⊢ ν (interior ↑K) = 0

Tactic:
· exact K.interior_nonempty

Goal state after:
case cpos.a
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := ⋯
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
h : ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) = 0
i' : ν.IsOpenPosMeasure
⊢ ν (interior ↑K) = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case hV
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ (interior ↑K).Nonempty

pp: case hμK
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K = ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)

pp: case neTopV
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K ≠ ∞

Tactic:
· exact K.interior_nonempty

Goal state after:
case hμK
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K = ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)

case neTopV
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case ofNat
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.ofNat n • T, f x = Int.ofNat n • ∫ (x : ℝ) in 0..T, f x

Tactic:
simp [← this n]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Tactic:
have := Box.continuousOn_face_Icc (Hc i) (Set.left_mem_Icc.2 (I.lower_le_upper i))
    have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
      Box.coe_subset_Icc
    exact (this.hasBoxIntegral ⊥ rfl).integral_eq

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν < ∞

Tactic:
apply_rules [ENNReal.mul_lt_top, hf.2, hg.2, ENNReal.ofReal_lt_top]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
by_cases! H : w ∈ sphere c |R| ∧ n < -1
  · rcases H with ⟨hw, hn⟩
    exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw
  have hd : ∀ z, z ≠ w ∨ -1 ≤ n →
      HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z := by
    intro z hne
    convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
    · have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
      simp [mul_div_cancel_left₀ _ hn']
    exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
  refine integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt
  exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ

Tactic:
by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
⊢ Function.Bijective (mapRoots p E)

Tactic:
constructor
  · exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))
  · intro y
    -- this is just an equality of two different ways to write the roots of `p` as an `E`-polynomial
    have key := (IsSplittingField.splits p.SplittingField p).roots_map
      (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
    rw [map_map, AlgHom.comp_algebraMap] at key
    have hy := Subtype.mem y
    simp only [rootSet, Finset.mem_coe, Multiset.mem_toFinset, key, Multiset.mem_map] at hy
    rcases hy with ⟨x, hx1, hx2⟩
    exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
⊢ P (p₁ * p₂)

pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
· rcases comp_eq_zero_iff.mp h₁ with h | h
      · rw [h, zero_mul]
        simp [P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
⊢ P (p₁ * p₂)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a)) + abv (-f a)) l atTop

Tactic:
refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a) + -f a)) l atTop
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
⊢ (∏ i, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Tactic:
let s := Finset.univ.val.map fun i => (MvPolynomial.X i : MvPolynomial σ R)

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ (∏ i, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
hc : DiffContOnCl ℂ f (ball c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑π * I) • deriv f c

Tactic:
simpa using DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul h0 1 hc

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots
⊢ ‖z‖ ≤ B

Tactic:
classical
  rw [← Multiset.mem_toFinset] at hz
  obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
  exact h φ

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ a.card = (b ∪ c).card

Tactic:
apply congr_arg Finset.card

Goal state after:
case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ (aeval z) p = 0 ∧ z.im ≠ 0
⊢ a = b ∪ c
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : (valuation R).IsNontrivial
⊢ IsRankLeOne R

Tactic:
have h' : MulArchimedean (ValueGroup₀ (.ofClass (valuation R))) :=
        MulArchimedean.comap embedding.toMonoidHom embedding_strictMono

Goal state after:
case pos
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : (valuation R).IsNontrivial
h' : MulArchimedean (ofClass (valuation R)).ValueGroup₀
⊢ IsRankLeOne R
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case hs
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ s.Countable

Tactic:
assumption

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case Hcf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))

Tactic:
assumption

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case Hcg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))

Tactic:
assumption

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case Hdf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt f (f' x) x

Tactic:
assumption

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case Hdg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt g (g' x) x

Tactic:
assumption

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case Hi
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ∃ b ∈ Finset.cons j t hj, ‖∏ i ∈ Finset.cons j t hj, f i‖ ≤ ‖f b‖

Tactic:
simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]

Goal state after:
case cons
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : IsUnit (valuation.restrict x)
⊢ 1 = valuation.restrict x

Tactic:
rw [eq_comm]

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : IsUnit (valuation.restrict x)
⊢ valuation.restrict x = 1
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ constantCoeff (φ.invOfUnit u) = ↑u⁻¹

Tactic:
← coeff_zero_eq_constantCoeff_apply,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ (coeff 0) (φ.invOfUnit u) = ↑u⁻¹
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ r ∈ nonZeroDivisorsLeft R → (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)

Tactic:
· intro H p hrp
    ext i
    have := congr(coeff (i + n) $hrp)
    rw [coeff_monomial_mul, if_pos le_add_self, add_tsub_cancel_right] at this
    simpa using H _ this

Goal state after: