mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
⊢ 1 / 2 < 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this✝ : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
this : (1 / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1)
⊢ 0 < 1 / 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this✝ : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
this : (1 / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1)
⊢ 1 / 2 < 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
g : ℝ → ε
h : EqOn f g (uIoo a b)
⊢ f =ᵐ[μ.restrict (Ioc (min a b) (max a b))] g

Tactic:
← restrict_Ioo_eq_restrict_Ioc

Goal state after:
ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
g : ℝ → ε
h : EqOn f g (uIoo a b)
⊢ f =ᵐ[μ.restrict (Ioo (min a b) (max a b))] g
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : ↥{ carrier := [[a, b]], isCompact' := ⋯ } := ⟨x✝, ⋯⟩
⊢ Summable fun n ↦ (f n) x✝

Tactic:
have := hf_sum.of_norm

Goal state after:
case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : ↥{ carrier := [[a, b]], isCompact' := ⋯ } := ⟨x✝, ⋯⟩
this : Summable fun i ↦ ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)
⊢ Summable fun n ↦ (f n) x✝
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
by
  have h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ⊤ := by
    rw [min_sub_sub_right, sub_add, sub_self, sub_zero]
    exact h
  wlog hab : a ≤ b generalizing a b
  · apply IntervalIntegrable.symm (this hf.symm ?_ ?_ (le_of_not_ge hab))
    · rw [min_comm]; exact h
    · rw [min_comm]; exact h'
  rw [intervalIntegrable_iff' h] at hf
  rw [intervalIntegrable_iff' h'] at ⊢
  have A : MeasurableEmbedding fun x => x + c :=
    (Homeomorph.addRight c).isClosedEmbedding.measurableEmbedding
  rw [← map_add_right_eq_self volume c] at hf
  convert! (MeasurableEmbedding.integrableOn_map_iff A).mp hf using 1
  rw [preimage_add_const_uIcc]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
set s := {t | g b - g t ≤ ∫ u in t..b, φ u} ∩ Icc a b

Goal state after:
case inr
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] (↑n + 1)

Tactic:
rw [← @cast_one α, ← cast_add]

Goal state after:
α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] ↑(n + 1)
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case convert_2
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 ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := ⋯
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ ν (QuotientGroup.mk ⁻¹' V ∩ s) ≠ 0

Tactic:
exact trans hV.symm neZeroV

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

Goal state before:
pp: case mp
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (fun z ↦ (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Tactic:
contrapose! h

Goal state after:
case mp
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
⊢ ¬CircleIntegrable (fun z ↦ (z - w) ^ n) c R
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
⊢ ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)

Tactic:
set g := fun y => f y - a - f' (y - x) with hg
    change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε
    clear_value g; obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]
    convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
    · congr 1
      have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
      simp only [← this, f'.map_sub]; abel
    · have : ∀ z ∈ Icc (I.lower i) (I.upper i), e z y ∈ (Box.Icc I) := fun z hz =>
        I.mapsTo_insertNth_face_Icc hz hy
      replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I) := by
        intro y hy
        refine (hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)
        rw [← dist_eq_norm]
        exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI
      rw [two_mul, add_mul]
      exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑R ^ n = 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖

Tactic:
rw_mod_cast [hR, mul_zero]
    exact mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
      (intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)

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
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ¬Integrable f μ ∨ ¬Integrable g ν

Tactic:
contrapose! h

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable f μ ∧ Integrable g ν
⊢ Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ Tendsto f (cocompact E) (𝓝 c')

Tactic:
by simpa [hc'] using! tendsto_const_nhds

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: 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
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ q.natDegree = 0

Tactic:
by rw [h.2, natDegree_C]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: 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
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ q.natDegree = 0

Tactic:
by rw [h.2, natDegree_C]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (rename ⇑e) (Multiset.map X ↑↑x✝).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x✝)).prod

Tactic:
rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (Multiset.map (⇑(rename ⇑e) ∘ X) ↑↑x✝).prod =
    (Multiset.map X
        ↑↑({ toFun := fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩,
                left_inv := ⋯, right_inv := ⋯ }
              x✝)).prod
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]

Goal state after:
case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ 0 ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h3.a
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) conj').support.card = (p.rootSet ℂ).toFinset.card

Tactic:
exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
y : ℚ
hy : y.num • 1 < 0
hyx : ↑y = x
⊢ ↑y ≤ 0

Tactic:
Rat.cast_nonpos,

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
y : ℚ
hy : y.num • 1 < 0
hyx : ↑y = x
⊢ y ≤ 0
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)

Goal state after:
case pos.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
s : Finset ι
⊢ 0 ≤ ⨆ i, ‖f i‖

case pos.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
s : Finset ι
⊢ ∀ i ∈ s, ‖f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (φ * ψ).lexOrder ≤ ↑(toLex p) + ↑(toLex q)

Tactic:
apply lexOrder_le_of_coeff_ne_zero (d := p + q)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
q : σ →₀ ℕ
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff (p + q)) (φ * ψ) ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ∈ (antidiagonal n).erase (0, n)
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, n).2 then (coeff (i, j).1) φ * (coeff (i, j).2) (φ.invOfUnit u) else 0

Tactic:
rw [Finset.mem_erase, mem_antidiagonal] at hij

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, n).2 then (coeff (i, j).1) φ * (coeff (i, j).2) (φ.invOfUnit u) else 0
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ Function.Bijective (Types.sectionOfCone c) ↔ Function.Bijective (⇑I.sectionsEquiv.symm ∘ Types.sectionOfCone c)

Tactic:
EquivLike.comp_bijective

Goal state after:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ Function.Bijective (Types.sectionOfCone c) ↔ Function.Bijective (Types.sectionOfCone c)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ (fun m ↦ m • W'.add P Q) ((hu.unit * hv.unit) ^ 2) = W'.add (u • P) (v • Q)

Tactic:
convert! (add_smul_of_not_equiv h hu hv).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x * Q z = Q x * P z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))

Tactic:
← Y_eq_iff' hPz hQz

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 * (eval P) W'.polynomial =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
  ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
· rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hP : W.Nonsingular P
  · by_cases hPz : P z = 0
    · rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
    · rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
      simp only [smul_fin3_ext, mul_div_mul_left _ _ hu.ne_zero, and_self]
  · rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
⊢ PreservesLimitsOfShape (Discrete ι) F

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_of_discrete

Goal state after:
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
⊢ ∀ (f : ι → Schemeᵒᵖ), PreservesLimit (Discrete.functor f) F
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R] ↔
    FormallySmooth R (Localization.Away f)

Tactic:
Set.subset_inter_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A (H1Cotangent R A))ᶜ ∧
      ↑(PrimeSpectrum.basicOpen f) ⊆ Module.freeLocus A Ω[A⁄R] ↔
    FormallySmooth R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
this : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (e i) = 1
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

Tactic:
by simp [ι, ← he', this]

Goal state after: