mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ⋂ l, ⋂ c, ⋂ (_ : ∀ y ∈ s, re (l y) ≤ c), {x | re (l x) ≤ c} = s

Tactic:
simp_rw [Set.iInter_ofPred]
  refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l c hc => hc x hx
  by_contra h
  obtain ⟨l, c, hls, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h
  exact (hl.trans_le (hx l c (fun y hy ↦ (hls y hy).le))).false

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ { toFun := s.domRestrict f, continuous_toFun := ⋯ } x = f ↑x

Tactic:
ContinuousMap.coe_mk,

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ s.domRestrict f x = f ↑x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_3
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
C1 : Continuous fun u ↦ ∫ (x : X), ↑↑u x ∂μ.withDensity fun x ↦ ↑(f x)
C2 : Continuous fun u ↦ ∫ (x : X), f x • ↑↑u x ∂μ
⊢ IsClosed {f_1 | (∫ (x : X), ↑↑f_1 x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • ↑↑f_1 x ∂μ}

Tactic:
exact isClosed_eq C1 C2

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

Goal state before:
pp: ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
⊢ IntervalIntegrable (∑ᶠ (i : ι), f i) μ a b

Tactic:
by_cases h₁ : f.support.Finite

Goal state after:
case pos
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : (support f).Finite
⊢ IntervalIntegrable (∑ᶠ (i : ι), f i) μ a b

case neg
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
⊢ IntervalIntegrable (∑ᶠ (i : ι), f i) μ a b
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ IntervalIntegrable f μ b₁ x

Tactic:
apply h_int.mono_set

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ IntervalIntegrable f μ a b₁

Tactic:
apply h_int.mono_set

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}

Tactic:
convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Tactic:
intervalIntegral_eq_integral_uIoc,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖(if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
intervalIntegral_eq_integral_uIoc,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
intervalIntegral_eq_integral_uIoc,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ = 0
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
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|

Tactic:
rw [norm_integral_eq_norm_integral_uIoc]

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂volume‖ ≤ C * |b - a|
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
μ : Measure ℝ
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ

Tactic:
intervalIntegral_eq_integral_uIoc,

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
μ : Measure ℝ
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, φ x ∂μ) v =
    (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, (φ x) v ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv

Goal state after:
case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * (R * C)

Tactic:
← mul_assoc

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ ((cauchyPowerSeries f c R n) fun x ↦ w) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

Tactic:
by
  simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const,
    div_eq_mul_inv, mul_pow, mul_smul, circleIntegral.integral_smul]
  rw [← smul_comm (w ^ n)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ ∫ (z : α × β), (B (f z.1)) (g z.2) ∂μ.prod ν = (B (∫ (x : α), f x ∂μ)) (∫ (y : β), g y ∂ν)

Tactic:
have : Integrable (fun z ↦ B (f z.1) (g z.2)) (μ.prod ν) :=
    hf.op_fst_snd (by fun_prop) ⟨‖B‖, B.le_opNorm₂⟩ hg
  simp_rw [integral_prod _ this, ContinuousLinearMap.integral_comp_comm _ hg]
  change ∫ x, B.flip (∫ y, g y ∂ν) (f x) ∂μ = _
  rw [ContinuousLinearMap.integral_comp_comm _ hf]
  simp

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
⊢ ∮ (z : ℂ) in C(c, R), f z = 0

Tactic:
rcases h0.eq_or_lt with (rfl | h0)

Goal state after:
case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hE : CompleteSpace E
h0 : 0 ≤ 0
hc : ContinuousOn f (closedBall c 0)
hd : ∀ z ∈ ball c 0 \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, 0), f z = 0

case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ ∮ (z : ℂ) in C(c, R), f z = 0
Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyCoherentSpace Y
f : X → Y
x✝ : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
⊢ IsClosed (Subtype.val ⁻¹' f '' s)

Tactic:
convert! (((h hK).inter_left hs).image hf).isClosed.preimage continuous_subtype_val using 1

Goal state after:
case e'_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyCoherentSpace Y
f : X → Y
x✝ : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
e_1✝ : ↑K = { x // x ∈ K }
⊢ Subtype.val ⁻¹' f '' s = Subtype.val ⁻¹' f '' (s ∩ f ⁻¹' K)
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✝ + C a).leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a))) l atTop

Tactic:
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf

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))) l atTop
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:

Tactic:
_ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left
      _ ≤ max B 1 ^ d * p.natDegree.choose i := by
        gcongr
        · apply le_max_right
        · exact le_trans (Nat.sub_le _ _) h3
      _ ≤ max B 1 ^ d * d.choose (d / 2) := by
        gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d)

Goal state after:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case inr
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✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered

Goal state after:
case inr
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✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_3
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 : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ mkRat (↑k * a.num) (k * a.den) = a

Tactic:
Rat.mkRat_mul_left hk0,

Goal state after:
case mp.refine_3
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 : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ mkRat a.num a.den = a
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: case pos
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : v x = 0
⊢ (map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) 0 = v x

Tactic:
simp [h0]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
⊢ ball x r = ball y r

Tactic:
ext a
  simp_rw [mem_ball] at h ⊢
  constructor <;> intro h' <;>
  exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
wlog! hrs : r ≤ s generalizing x y r s

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
wlog! hrs : r ≤ s generalizing x y r s

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
⊢ ‖∏ i ∈ s, f i‖ ≤ s.sup' hs fun x ↦ ‖f x‖

Tactic:
by
  simp only [Finset.le_sup'_iff]
  induction hs using Finset.Nonempty.cons_induction with
  | singleton j => simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]
  | cons j t hj _ IH =>
      simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]
      refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_ <;> intro h
      · exact (norm_mul_le_max _ _).trans (max_eq_left h).le
      · exact ⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩

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
⊢ φ.invOfUnit u * φ = 1

Tactic:
← mul_cancel_right_mem_nonZeroDivisors (r := φ.invOfUnit u),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
⊢ φ.invOfUnit u * φ * φ.invOfUnit u = 1 * φ.invOfUnit u

σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
⊢ φ.invOfUnit u ∈ nonZeroDivisors (MvPowerSeries σ R)
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

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

Tactic:
constantCoeff_zero

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

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

Tactic:
simp only [mk_apply]

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ ofJ 0 = ofJ0 F

Tactic:
by
  rw [ofJ, if_pos rfl, if_neg ((show (3 : F) = 1 by linear_combination h2) ▸ one_ne_zero)]

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

Goal state before:
pp: K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
l : L
⊢ Φ (1 ⊗ₜ[K] l) = (algebraMap L (adicCompletion L w)) l

Tactic:
simp [Φ, Algebra.algHom]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) = W'.dblZ P

Tactic:
by
  linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -3 * (P y - W'.negY P) * (equation_iff _).mp hP

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
hPz : P z = 0
⊢ (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) ⋯ else 0) = 0

Tactic:
dif_neg <| not_and_not_right.mpr fun _ => hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Equation (⇑f ∘ P) ↔ (W'⁄A).Equation P

Tactic:
rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Goal state after: