harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.convolution_integrand_bound_left (hcf : HasCompactSupport f)
    (hf : Continuous f) {x t : G} {s : Set G} (hx : x ∈ s) :
    ‖L (f (x - t)) (g t)‖ ≤
      (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous f
x t : G
s : Set G
hx : x ∈ s
⊢ ‖(L (f (x - t))) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t

Tactic:
convert hcf.convolution_integrand_bound_right L.flip hf hx using 1

Result:
case h.e'_4
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous f
x t : G
s : Set G
hx : x ∈ s
⊢ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t =
    (-tsupport f + s).indicator (fun t => ‖L.flip‖ * ‖g t‖ * ⨆ i, ‖f i‖) t

Proof state:
case h.e'_4
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous f
x t : G
s : Set G
hx : x ∈ s
⊢ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t =
    (-tsupport f + s).indicator (fun t => ‖L.flip‖ * ‖g t‖ * ⨆ i, ‖f i‖) t

Tactic:
simp_rw [L.opNorm_flip, mul_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma sUnion_insert_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C)
    (ht : t ∈ C) (hst : t ⊆ s) :
    ⋃₀ insert t (hC.disjointOfDiff hs ht) = s

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
⊢ ⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = t ∪ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Tactic:
simp only [mem_coe, sUnion_insert]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
⊢ ⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = s

Tactic:
conv_rhs => rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
⊢ ⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = t ∪ ⋃₀ ↑(hC.disjointOfDiff hs ht)
-- Mathlib/Topology/Compactification/OnePointEquiv.lean
@[simp]
lemma equivProjectivization_apply_coe (t : K) :
    equivProjectivization K t = mk K ⟨t, 1⟩ (by simp) :=
  rfl

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
t : K
⊢ (t, 1) ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_add [AddMonoid α] [StarAddMonoid α] (M N : Matrix m n α) :
    (M + N)ᴴ = Mᴴ + Nᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M + N)ᴴ i j = (Mᴴ + Nᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
lemma Topology.IsInducing.continuousWithinAt_iff {f : α → β} {g : β → γ} (hg : IsInducing g)
    {s : Set α} {x : α} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Tactic:
simp_rw [ContinuousWithinAt, hg.tendsto_nhds_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem integral_mul_eq_integral [HasPDF X ℙ] : ∫ x, x * (pdf X ℙ volume x).toReal = ∫ x, X x ∂ℙ :=
  calc
    _ = ∫ x, (pdf X ℙ volume x).toReal * x

Proof state:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝¹ : IsFiniteMeasure ℙ
inst✝ : HasPDF X ℙ volume
x : ℝ
⊢ x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x

Tactic:
exact mul_comm _ _

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝¹ : IsFiniteMeasure ℙ
inst✝ : HasPDF X ℙ volume
⊢ ∫ (x : ℝ), x * (pdf X ℙ volume x).toReal = ∫ (x : ℝ), (pdf X ℙ volume x).toReal * x

Tactic:
congr with x

Result:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝¹ : IsFiniteMeasure ℙ
inst✝ : HasPDF X ℙ volume
x : ℝ
⊢ x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem ord_term_aux {o : Ordinal} (ho : o < Ordinal.type ((· < ·) : I → I → Prop)) :
    ord I (term I ho) = o

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ord I (term I ho) = o

Tactic:
simp only [ord, term, Ordinal.typein_enum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <:+ l₁.filter p ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.filter p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ l₂ <:+ filter p l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filter p l

Tactic:
rw [← filterMap_eq_filter, isSuffix_filterMap_iff]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem eq_bot_iff_forall_lt (x : EReal) : x = ⊥ ↔ ∀ y : ℝ, x < (y : EReal)

Proof state:
case mpr
x : EReal
⊢ x ≠ ⊥ → ∃ y, ↑y ≤ x

Tactic:
intro h

Result:
case mpr
x : EReal
h : x ≠ ⊥
⊢ ∃ y, ↑y ≤ x

Proof state:
case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

Tactic:
rintro rfl

Result:
case mp

⊢ ∀ (y : ℝ), ⊥ < ↑y

Proof state:
case mp

⊢ ∀ (y : ℝ), ⊥ < ↑y

Tactic:
exact bot_lt_coe

Result:
no goals

Proof state:
case mpr
x : EReal
h : x ≠ ⊥
⊢ ∃ y, ↑y ≤ x

Tactic:
exact ⟨x.toReal, coe_toReal_le h⟩

Result:
no goals

Proof state:
x : EReal
⊢ x = ⊥ ↔ ∀ (y : ℝ), x < ↑y

Tactic:
constructor

Result:
case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Proof state:
case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Tactic:
contrapose!

Result:
case mpr
x : EReal
⊢ x ≠ ⊥ → ∃ y, ↑y ≤ x
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_ne_zero_iff_right (hb : b ≠ 0) : a * b ≠ 0 ↔ a ≠ 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b ≠ 0 ↔ a ≠ 0

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem comp {g : B →+* C} {f : A →+* B} (hg : g.FinitePresentation) (hf : f.FinitePresentation) :
    (g.comp f).FinitePresentation

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Algebra.FinitePresentation B C
algebraizeInst✝ : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.trans A B C

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
⊢ (g.comp f).FinitePresentation

Tactic:
algebraize [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Algebra.FinitePresentation B C
algebraizeInst✝ : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeD_eq_takeDTR : @takeD = @takeDTR

Proof state:
case h.h.h.h
α : Type u_1
f : Nat
n : List α
l : α
⊢ takeD f n l = takeDTR f n l

Tactic:
simp [takeDTR, takeDTR_go_eq]

Result:
no goals

Proof state:
⊢ @takeD = @takeDTR

Tactic:
funext α f n l

Result:
case h.h.h.h
α : Type u_1
f : Nat
n : List α
l : α
⊢ takeD f n l = takeDTR f n l
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem antidiagonal_congr (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
    p = q ↔ p.1 = q.1

Proof state:
A : Type u_1
inst✝¹ : AddCancelMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p.1 + p.2 = n
hq : q.1 + q.2 = n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2

Tactic:
rw [hq, ← h, hp]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : AddCancelMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p = q ↔ p.1 = q.1

Tactic:
refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩

Result:
A : Type u_1
inst✝¹ : AddCancelMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2

Proof state:
A : Type u_1
inst✝¹ : AddCancelMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2

Tactic:
rw [mem_antidiagonal] at hp hq

Result:
A : Type u_1
inst✝¹ : AddCancelMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p.1 + p.2 = n
hq : q.1 + q.2 = n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem CokernelCofork.condition (s : CokernelCofork f) : f ≫ s.π = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ f ≫ Cofork.π s = 0

Tactic:
rw [Cofork.condition, zero_comp]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.le_max? {t : RBNode α} [TransCmp cmp] (ht : t.Ordered cmp) (h : t.max? = some a)
    (x) (hx : x ∈ t) : cmp x a ≠ .gt :=
  ht.reverse.min?_le ((min?_reverse _).trans h) _ (by simpa using hx)

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : t.max? = some a
x : α
hx : x ∈ t
⊢ x ∈ t.reverse

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_iff_exists_monotone_subseq :
    s.PartiallyWellOrderedOn r ↔
      ∀ f : ℕ → α, (∀ n, f n ∈ s) → ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n))

Proof state:
case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨g, gmon⟩ := h f hf

Result:
case mpr.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case mpr.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨g 0, g 1, g.lt_iff_lt.2 Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
constructor <;> intro h f hf

Result:
case mp
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case mp
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
exact h.exists_monotone_subseq f hf

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_map_left_iff {f : γ → α} :
    ∀ {l u}, Forall₂ R (map f l) u ↔ Forall₂ (fun c b => R (f c) b) l u
  | [], _ => by simp only [map, forall₂_nil_left_iff]
  | a :: l, _ => by simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝

Tactic:
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
x✝ : List β
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝

Tactic:
simp only [map, forall₂_nil_left_iff]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem fg_iff : FG L M ↔ ∃ S : Set M, S.Finite ∧ closure L S = (⊤ : L.Substructure M)

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ FG L M ↔ ∃ S, S.Finite ∧ (closure L).toFun S = ⊤

Tactic:
rw [fg_def, Substructure.fg_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Count.lean
theorem le_countP_tail (l) : countP p l - 1 ≤ countP p l.tail

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ countP p l - 1 ≤ countP p l.tail

Tactic:
have := (tail_sublist l).le_countP p

Result:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
this : countP p l - (l.length - l.tail.length) ≤ countP p l.tail
⊢ countP p l - 1 ≤ countP p l.tail

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
this : countP p l - (l.length - (l.length - 1)) ≤ countP p l.tail
⊢ countP p l - 1 ≤ countP p l.tail

Tactic:
omega

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
this : countP p l - (l.length - l.tail.length) ≤ countP p l.tail
⊢ countP p l - 1 ≤ countP p l.tail

Tactic:
simp only [length_tail] at this

Result:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
this : countP p l - (l.length - (l.length - 1)) ≤ countP p l.tail
⊢ countP p l - 1 ≤ countP p l.tail
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionOf_eq_top_iff (m : M) : torsionOf R M m = ⊤ ↔ m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ m = 0

Tactic:
rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : m = 0
⊢ torsionOf R M m = ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ torsionOf R M m = ⊤ ↔ m = 0

Tactic:
refine ⟨fun h => ?_, fun h => by simp [h]⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ m = 0
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ :=
  ⟨fun h => top_unique fun Y f _ => by simpa using downward_closed _ h f, fun h => h.symm ▸ trivial⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f

Tactic:
simpa using downward_closed _ h f

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_linear_lt_degree_C_mul_X_sq (ha : a ≠ 0) :
    degree (C b * X + C c) < degree (C a * X ^ 2)

Proof state:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b * X + C c).degree < (C a * X ^ 2).degree

Tactic:
simpa only [degree_C_mul_X_pow 2 ha] using degree_linear_lt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_range (n : Nat) : (range n).toList = List.range n

Proof state:
n : Nat
⊢ (range n).toList = List.range n

Tactic:
apply List.ext_getElem <;> simp [range]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_iUnion {ι} [Finite ι] (s : ι → Set α) (a : α) :
    𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a

Tactic:
rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_empty {a : α} {fallback : α} {c} :
    (empty c : Raw₀ α β).getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a fallback : α
c : Nat
⊢ (empty c).getKeyD a fallback = fallback

Tactic:
simp [getKeyD, empty]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_mul {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    Multiset.Rel Associated (factors (x * y)) (factors x + factors y)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x + factors y).prod

Tactic:
rw [Multiset.prod_add]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x).prod * (factors y).prod

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ Multiset.Rel Associated (factors (x * y)) (factors x + factors y)

Tactic:
refine
  factors_unique irreducible_of_factor
    (fun a ha =>
      (Multiset.mem_add.mp ha).by_cases (irreducible_of_factor _) (irreducible_of_factor _))
    ((factors_prod (mul_ne_zero hx hy)).trans ?_)

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x + factors y).prod

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x).prod * (factors y).prod

Tactic:
exact (Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
    forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b

Proof state:
m✝ : Type ?u.3503 → Type ?u.3456
α : Type ?u.3461
β : Type ?u.3503
inst✝ : Monad m✝
o : Option α
b✝ : β
f : (a : α) → a ∈ o.toList → β → m✝ (ForInStep β)
a : α
m : a ∈ o
b : β
⊢ a ∈ o.toList

Tactic:
simpa using m

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
o : Option α
b : β
f : (a : α) → a ∈ o.toList → β → m (ForInStep β)
⊢ forIn' o.toList b f = forIn' o b fun a m b => f a ⋯ b

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_toFinset [DecidableEq α] {s : Multiset α} :
    s.toFinset.image f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_image, Multiset.mem_toFinset, exists_prop, Multiset.mem_map]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq α
s : Multiset α
x✝ : β
⊢ x✝ ∈ image f s.toFinset ↔ x✝ ∈ (Multiset.map f s).toFinset

Tactic:
simp only [mem_image, Multiset.mem_toFinset, exists_prop, Multiset.mem_map]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem gc : GaloisConnection (adjoin R : Set A → StarSubalgebra R A) (↑)

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
⊢ GaloisConnection (adjoin R) SetLike.coe

Tactic:
intro s S

Result:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ ↑S

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ ↑S

Tactic:
rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_toSubalgebra]

Result:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ≤ ↑S

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ≤ ↑S

Tactic:
exact
  ⟨fun h => Set.subset_union_left.trans h, fun h =>
    Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem norm_le_one_iff : ‖x‖ ≤ 1 ↔ val.v x ≤ 1

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ ‖x‖ ≤ 1 ↔ v x ≤ 1

Tactic:
simpa only [_root_.map_one] using (Valuation.RankOne.strictMono val.v).le_iff_le (b := 1)

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem inr_map_mul (b₁ b₂ : B) :
    LinearMap.inr R A B (b₁ * b₂) = LinearMap.inr R A B b₁ * LinearMap.inr R A B b₂ :=
  Prod.ext (by simp) rfl

Proof state:
R : Type u
inst✝⁴ : Semiring R
A : Type u_4
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
B : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Module R B
b₁ b₂ : B
⊢ ((inr R A B) (b₁ * b₂)).1 = ((inr R A B) b₁ * (inr R A B) b₂).1

Tactic:
simp

Result:
no goals