harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LaurentSeries.lean
theorem eq_coeff_of_valuation_sub_lt {d n : ℤ} {f g : K⸨X⸩}
    (H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))) : n < d → g.coeff n = f.coeff n

Proof state:
case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ g.coeff n = f.coeff n

Tactic:
apply eq_of_sub_eq_zero

Result:
case neg.h
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ g.coeff n - f.coeff n = 0

Proof state:
case pos
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : g = f
⊢ n < d → g.coeff n = f.coeff n

Tactic:
exact fun _ => by rw [triv]

Result:
no goals

Proof state:
case neg.h
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ (g - f).coeff n = 0

Tactic:
apply coeff_zero_of_lt_valuation K H hn

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
⊢ n < d → g.coeff n = f.coeff n

Tactic:
intro hn

Result:
case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ g.coeff n = f.coeff n

Proof state:
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : g = f
x✝ : n < d
⊢ g.coeff n = f.coeff n

Tactic:
rw [triv]

Result:
no goals

Proof state:
case neg.h
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ g.coeff n - f.coeff n = 0

Tactic:
rw [← HahnSeries.coeff_sub]

Result:
case neg.h
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
hn : n < d
⊢ (g - f).coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
⊢ n < d → g.coeff n = f.coeff n

Tactic:
by_cases triv : g = f

Result:
case pos
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : g = f
⊢ n < d → g.coeff n = f.coeff n

case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))
triv : ¬g = f
⊢ n < d → g.coeff n = f.coeff n
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_source_mem_nhds {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝 x :=
  (isOpen_extend_source f).mem_nhds <| by rwa [f.extend_source]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem mem_cons_of_mem {a : α} {s : Stream' α} (b : α) : a ∈ s → a ∈ b::s := fun ⟨n, h⟩ =>
  Exists.intro (succ n) (by rw [get_succ, tail_cons, h])

Proof state:
α : Type u
a : α
s : Stream' α
b : α
x✝ : a ∈ s
n : ℕ
h : (fun b => a = b) (s.get n)
⊢ (fun b => a = b) ((b :: s).get n.succ)

Tactic:
rw [get_succ, tail_cons, h]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_right_comm : s ○ t ○ u = s ○ u ○ t

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ t ○ u = s ○ u ○ t

Tactic:
simp_rw [disjSups_assoc, disjSups_comm]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem map_reverse_tails (l : List α) : map reverse l.tails = (reverse <| inits <| reverse l)

Proof state:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse

Tactic:
simp [reverse_involutive.comp_self, ← map_reverse]

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
rw [tails_eq_inits l]

Result:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
-- Mathlib/Topology/Compactness/Exterior.lean
theorem IsCompact.exterior_iff : IsCompact (exterior s) ↔ IsCompact s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → exterior s ⊆ ⋃ i, U i → ∃ t, exterior s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
peel with ι U hUo

Result:
case h.h.h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen (U i)
⊢ (exterior s ⊆ ⋃ i, U i → ∃ t, exterior s ⊆ ⋃ i ∈ t, U i) ↔ s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (exterior s) ↔ IsCompact s

Tactic:
simp only [isCompact_iff_finite_subcover]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → exterior s ⊆ ⋃ i, U i → ∃ t, exterior s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
case h.h.h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen (U i)
⊢ (exterior s ⊆ ⋃ i, U i → ∃ t, exterior s ⊆ ⋃ i ∈ t, U i) ↔ s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
simp only [(isOpen_iUnion hUo).exterior_subset,
  (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).exterior_subset]

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem sum_toPOUFun_eq (x : X) : ∑ᶠ i, f.toPOUFun i x = 1 - ∏ᶠ i, (1 - f i x)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i => f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝ : i ∈ s
⊢ f.toPOUFun i x = (f i) x * ∏ j ∈ Finset.filter (fun j => j < i) s, (1 - (f j) x)

Tactic:
convert f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _

Result:
case convert_4
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i => f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : (f j) x ≠ 0
⊢ j ∈ s
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma GrowsPolynomially.of_isTheta {f g : ℝ → ℝ} (hg : GrowsPolynomially g) (hf : f =Θ[atTop] g)
    (hf' : ∀ᶠ x in atTop, 0 ≤ f x) : GrowsPolynomially f

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
have h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹ := by positivity

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => ‖g x‖) u ∈ Set.Icc (c₃ * (fun x => ‖g x‖) x) (c₄ * (fun x => ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem WfDvdMonoid.of_wellFoundedLT_associates [CancelCommMonoidWithZero α]
    (h : WellFoundedLT (Associates α)) : WfDvdMonoid α :=
  WfDvdMonoid.of_wfDvdMonoid_associates
    ⟨by
      convert h.wf
      ext
      exact Associates.dvdNotUnit_iff_lt⟩

Proof state:
case h.e'_2.h.h.h.e.h.h.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFoundedLT (Associates α)
x✝³ x✝² x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝

Tactic:
exact Associates.dvdNotUnit_iff_lt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFoundedLT (Associates α)
⊢ WellFounded DvdNotUnit

Tactic:
convert h.wf

Result:
case h.e'_2.h.h.h.e
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFoundedLT (Associates α)
x✝¹ x✝ : Associates α
⊢ DvdNotUnit = LT.lt

Proof state:
case h.e'_2.h.h.h.e
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFoundedLT (Associates α)
x✝¹ x✝ : Associates α
⊢ DvdNotUnit = LT.lt

Tactic:
ext

Result:
case h.e'_2.h.h.h.e.h.h.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFoundedLT (Associates α)
x✝³ x✝² x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_prod_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, (f j).degreeOf i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
x✝¹ x✝ : σ →₀ ℕ
⊢ (x✝¹ + x✝) i = x✝¹ i + x✝ i

Tactic:
simp only [coe_add, Pi.add_apply]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∏ j ∈ s, f j).support.sup fun m => m i) ≤ ∑ x ∈ s, (f x).support.sup fun m => m i

Tactic:
exact supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply])
  (fun _ _ => by simp only [coe_add, Pi.add_apply])

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 i = 0

Tactic:
simp only [coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)

Tactic:
simp_rw [degreeOf_eq_sup]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∏ j ∈ s, f j).support.sup fun m => m i) ≤ ∑ x ∈ s, (f x).support.sup fun m => m i
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_mono {K K' V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : (interior V).Nonempty) :
    index K V ≤ index K' V

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K V ≤ index K' V

Tactic:
apply Nat.sInf_le

Result:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K' V ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
⊢ index K V ≤ index K' V

Tactic:
rcases index_elim hK' hV with ⟨s, h1s, h2s⟩

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K V ≤ index K' V

Proof state:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ x ∈ {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = index K' V

Tactic:
exact ⟨s, Subset.trans h h1s, h2s⟩

Result:
no goals

Proof state:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ index K' V ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
rw [mem_image]

Result:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ x ∈ {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = index K' V
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.sub [IsTopologicalAddGroup M₄] {f g : M₁ → M₄} (hf : IsCompactOperator f)
    (hg : IsCompactOperator g) : IsCompactOperator (f - g)

Proof state:
M₁ : Type u_3
M₄ : Type u_5
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f - g)

Tactic:
rw [sub_eq_add_neg]

Result:
M₁ : Type u_3
M₄ : Type u_5
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)

Proof state:
M₁ : Type u_3
M₄ : Type u_5
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)

Tactic:
exact hf.add hg.neg

Result:
no goals
-- Mathlib/Topology/MetricSpace/Closeds.lean
theorem continuous_infEdist_hausdorffEdist :
    Continuous fun p : α × Closeds α => infEdist p.1 p.2

Proof state:
α : Type u
inst✝ : EMetricSpace α
⊢ ∀ (x y : α × Closeds α), infEdist x.1 ↑x.2 ≤ infEdist y.1 ↑y.2 + 2 * edist x y

Tactic:
rintro ⟨x, s⟩ ⟨y, t⟩

Result:
case mk.mk
α : Type u
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist (x, s).1 ↑(x, s).2 ≤ infEdist (y, t).1 ↑(y, t).2 + 2 * edist (x, s) (y, t)

Proof state:
α : Type u
inst✝ : EMetricSpace α
⊢ Continuous fun p => infEdist p.1 ↑p.2

Tactic:
refine continuous_of_le_add_edist 2 (by simp) ?_

Result:
α : Type u
inst✝ : EMetricSpace α
⊢ ∀ (x y : α × Closeds α), infEdist x.1 ↑x.2 ≤ infEdist y.1 ↑y.2 + 2 * edist x y

Proof state:
case mk.mk
α : Type u
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist (x, s).1 ↑(x, s).2 ≤ infEdist (y, t).1 ↑(y, t).2 + 2 * edist (x, s) (y, t)

Tactic:
calc
  infEdist x s ≤ infEdist x t + hausdorffEdist (t : Set α) s :=
    infEdist_le_infEdist_add_hausdorffEdist
  _ ≤ infEdist y t + edist x y + hausdorffEdist (t : Set α) s :=
    (add_le_add_right infEdist_le_infEdist_add_edist _)
  _ = infEdist y t + (edist x y + hausdorffEdist (s : Set α) t) := by
    rw [add_assoc, hausdorffEdist_comm]
  _ ≤ infEdist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) :=
    (add_le_add_left (add_le_add (le_max_left _ _) (le_max_right _ _)) _)
  _ = infEdist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]

Result:
no goals

Proof state:
α : Type u
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + edist x y + hausdorffEdist ↑t ↑s = infEdist y ↑t + (edist x y + hausdorffEdist ↑s ↑t)

Tactic:
rw [add_assoc, hausdorffEdist_comm]

Result:
no goals

Proof state:
α : Type u
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t)) = infEdist y ↑t + 2 * edist (x, s) (y, t)

Tactic:
rw [← mul_two, mul_comm]

Result:
no goals

Proof state:
α : Type u
inst✝ : EMetricSpace α
⊢ 2 ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem comul_counit_hom (M : Bimon_ C) :
    M.comul.hom ≫ (_ ◁ M.counit.hom) = (ρ_ _).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.comul.hom ≫ M.X.X ◁ M.counit.hom = (ρ_ M.X.X).inv

Tactic:
simpa [- Comon_.comul_counit] using congr_arg Mon_.Hom.hom M.comul_counit

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem psumPart_zero : psumPart σ R (.indiscrete 0) = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ psumPart σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
simp [psumPart]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma reduce_mem_reps {m : ℤ} (hm : m ≠ 0) (A : Δ m) : reduce A ∈ reps m

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ ↑A 1 0 = 0 ∧ n * ↑A 1 0 < ↑A 0 0 ∧ n * ↑A 1 1 ≤ ↑A 0 1 ∧ |↑A 0 1 + -(n * ↑A 1 1)| < |↑A 1 1|

Tactic:
simp_all only [h, mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
  Fin.isValue, h1, h3, and_true, true_and]

Result:
no goals

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ reduce A ∈ reps m

Tactic:
simp only [reduce_of_pos h h1]

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Proof state:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
this : ↑A 1 0 = 0 ∧ n * ↑A 1 0 < ↑A 0 0 ∧ n * ↑A 1 1 ≤ ↑A 0 1 ∧ |↑A 0 1 + -(n * ↑A 1 1)| < |↑A 1 1|
⊢ ⟨!![1, -n; 0, 1] * ↑A, ⋯⟩ ∈ reps m

Tactic:
simpa only [reps, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, empty_mul,
  Equiv.symm_apply_apply, Set.mem_setOf_eq, of_apply, cons_val', vecMul, cons_dotProduct,
  vecHead, one_mul, vecTail, Function.comp_apply, Fin.succ_zero_eq_one, neg_mul,
  dotProduct_empty, add_zero, zero_mul, zero_add, empty_val', cons_val_fin_one,
  cons_val_one, cons_val_zero, lt_add_neg_iff_add_lt, le_add_neg_iff_add_le]

Result:
no goals

Proof state:
case base
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
⊢ reduce A ∈ reps m

Tactic:
have hd := A_d_ne_zero h hm

Result:
case base
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
⊢ reduce A ∈ reps m
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive sum_nonneg]
lemma one_le_prod_of_one_le [Preorder M] [MulLeftMono M] {l : List M}
    (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : 1 ≤ l.prod

Proof state:
case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ [].prod

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ 1 ≤ l.prod

Tactic:
induction' l with hd tl ih

Result:
case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ [].prod

case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Proof state:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod

Tactic:
exact one_le_mul (hl₁ hd (mem_cons_self hd tl)) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Result:
no goals

Proof state:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Tactic:
rw [prod_cons]

Result:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod
-- Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
theorem MemLp.meas_ge_lt_top {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0) :
    μ { x | ε ≤ ‖f x‖₊ } < ∞

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε ≠ 0

Tactic:
simp [hε]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ↑ε ≤ ↑‖f x‖₊} < ⊤

Tactic:
apply hℒp.meas_ge_lt_top' hp_ne_zero hp_ne_top (by simp [hε])

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ε ≤ ‖f x‖₊} < ⊤

Tactic:
simp_rw [← ENNReal.coe_le_coe]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
μ : Measure α
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ↑ε ≤ ↑‖f x‖₊} < ⊤
-- Mathlib/Analysis/Complex/Circle.lean
@[simp]
protected lemma norm_smul {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E]
    (u : Circle) (v : E) :
    ‖u • v‖ = ‖v‖

Proof state:
E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖u • v‖ = ‖v‖

Tactic:
rw [Submonoid.smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/DualNumber.lean
theorem exp_smul_eps (r : R) : exp 𝕜 (r • eps : DualNumber R) = 1 + r • eps

Proof state:
𝕜 : Type u_1
R : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : CharZero 𝕜
inst✝⁴ : CommRing R
inst✝³ : Algebra 𝕜 R
inst✝² : UniformSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
r : R
⊢ exp 𝕜 (r • ε) = 1 + r • ε

Tactic:
rw [eps, ← inr_smul, exp_inr]

Result:
no goals