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

Goal state before:
pp: case hz
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 := ⋯
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 : ℕ
k_gt : n e < k
m : ℕ := ⋯
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
⊢ y ∈ Icc x (x + (1 / 2) ^ m / 2)

Tactic:
simp only [pow_add, tsub_le_iff_left] at h'k

Goal state after:
case hz
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 : ℕ
k_gt : n e < k
m : ℕ := k - 1
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
h'k : y ≤ x + (1 / 2) ^ m * (1 / 2) ^ 1
⊢ y ∈ Icc x (x + (1 / 2) ^ m / 2)
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0∞
s : Set X
hf : AEMeasurable f (μ.restrict s)
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
hs : MeasurableSet s
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x ↦ f x) = ∫ (x : X) in s, (f x).toReal • g x ∂μ

Tactic:
rw [restrict_withDensity hs, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
simp only [sub_eq_add_neg, neg_mul_eq_neg_mul]

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + -c * x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case refine_2
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ

Tactic:
intro p hmp IH h
    rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
    · refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_
      exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk
    · apply h
      simp [hmp]
    · intro k hk
      exact h _ (Ico_subset_Ico_right p.le_succ hk)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k volume
⊢ ∃ c ∈ s, ∃ d ∈ s, ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖

Tactic:
by
    rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
    have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ :=
      hf.eventually (eventually_gt_atTop _)
    exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩

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

Goal state before:
pp: case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
⊢ ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊ ≤ ENNReal.ofReal (g b - g a)

Tactic:
by_contra! H

Goal state after:
case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ a * c ^ n < ↑(n - d)!

Tactic:
calc a * c ^ n
    _ ≤ |a * c ^ n| := le_abs_self _
    _ ≤ ⌈|a|⌉₊ * (⌈|c|⌉₊ : K) ^ n := ?_
    _ = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) := ?_
    _ < (n - d)! := Nat.cast_lt.mpr h

Goal state after:
case calc_1
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a * c ^ n| ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

case calc_2
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case hs
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ Ι a₀ b₀ ⊆ Icc a b

Tactic:
exact uIoc_subset_uIcc.trans (uIcc_subset_Icc ⟨a_lt.1.le, lt_b.1.le⟩ ⟨a_lt.2.le, lt_b.2.le⟩)

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε

Tactic:
inter_eq_left,

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Metric.closedBall 0 ε ⊆ I
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: 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✝² : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)
neTopV : μ V ≠ ∞
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
by
  apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := h𝓕)
    (meas_V := meas_V)
  · rw [hμK]
    intro c_eq_zero
    apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
    · simp
    · apply Set.Nonempty.mono (preimage_interior_subset_interior_preimage continuous_coinduced_rng)
      apply hV.preimage'
      simp
    · apply measure_mono_null (h := interior_subset)
      apply h𝓕.measure_zero_of_invariant (ht := fun g ↦ QuotientGroup.sound _ _ g)
      exact c_eq_zero
  · exact hμK
  · exact neTopV

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
· simp +unfoldPartialApp [h₀, const]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), f z = ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)

Tactic:
by
  rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc]

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‖
⊢ ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν

Tactic:
gcongr with z
      simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]
      refine (hC _ _).trans ?_
      gcongr
      apply le_coe_toNNReal

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

Goal state before:
pp: case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z ↦ (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
refine integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt

Goal state after:
case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z ↦ (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c |R|
⊢ z ≠ w ∨ -1 ≤ n
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 μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ‖i - g‖) (𝓝 g) (𝓝 0)

Tactic:
← tendsto_iff_norm_sub_tendsto_zero

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 μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ i) (𝓝 g) (𝓝 g)
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 < ∞)
⊢ ∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    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
inst✝ : Fact (map (algebraMap F E) p).Splits
⊢ Function.Injective ⇑(galActionHom p E)

Tactic:
injective_iff_map_eq_one

Goal state after:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
⊢ ∀ (a : p.Gal), (galActionHom p E) a = 1 → a = 1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ (esymm σ R n).IsSymmetric

Tactic:
by
  intro
  rw [rename_esymm]

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

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
rw [support_esymm'']

Goal state after:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) =
    (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0

Tactic:
Finset.sum_eq_single_of_mem (Multiset.card s - k) _

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ (map (fun a ↦ X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
convert! p.roots.prod_X_sub_C_coeff this using 3

Goal state after:
case e'_5
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.roots.card - k

case e'_6
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.roots.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 : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c

Tactic:
← this,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
    (2 * ↑π * I / ↑n.factorial) • n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩

Goal state after:
case refine_1
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ Set.MapsTo Subtype.val {x | x ≤ 1} (Set.range (⇑v ∘ ⇑(algebraMap O F)))

case refine_2
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ Γ₀ → ↥(MonoidHom.mrange v)

case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ Set.MapsTo ?refine_2 (Set.range (⇑v ∘ ⇑(algebraMap O F))) {x | x ≤ 1}

case refine_4
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
    ∀ b ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)), a > b → ((fun x1 x2 ↦ x1 > x2) on ?refine_2) a b
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ (num * ↑n) • 1 < (↑n * ↑den) • x ↔ num • 1 < den • x

Tactic:
rw [mul_comm num, mul_smul, mul_smul, natCast_zsmul x den]
  exact ⟨fun h ↦ lt_of_smul_lt_smul_left h (Int.natCast_nonneg n),
    fun h ↦ zsmul_lt_zsmul_right (Int.natCast_pos.mpr hn) h⟩

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

Goal state before:
pp: case singleton
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
⊢ ∃ b ∈ {j}, ‖∏ i ∈ {j}, f i‖ ≤ ‖f b‖

Tactic:
| singleton j =>

Goal state after:
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
⊢ (coeff n) (φ * φ.invOfUnit u) = (coeff n) 1

Tactic:
by
      classical
      have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
      rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
        Finset.sum_insert (Finset.notMem_erase _ _), coeff_zero_eq_constantCoeff_apply, h,
        coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
        Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _),
        Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ←
        sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]
      rintro ⟨i, j⟩ hij
      rw [Finset.mem_erase, mem_antidiagonal] at hij
      obtain ⟨h₁, rfl⟩ := hij
      rw [if_pos]
      refine lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_
      rintro rfl
      simp at h₁

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ 0⁻¹ = 0

Tactic:
by
  rw [inv_eq_zero, constantCoeff_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ ↑u = ↑(Units.mk0 (constantCoeff φ) ⋯)

Tactic:
exact h.symm

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1

Tactic:
rw [mul_comm]
  exact mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ x ∈ v₁.asIdeal, x ∉ v₂.asIdeal

Tactic:
by_contra! H

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
H : ∀ x ∈ v₁.asIdeal, x ∈ v₂.asIdeal
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j

pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j

Tactic:
· by_cases h3 : (3 : F) = 0
    · have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
      simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]
      linear_combination 576 * h3
    · have := Fact.mk (Ne.isUnit h3)
      simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).j = j
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 c.toSections

Tactic:
← toSections_fac,

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