harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂

Proof state:
case intro.intro.intro.intro
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₂

Tactic:
have : l₁' = [] := by
  rw [eq_nil_iff_forall_not_mem]
  exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)

Result:
case intro.intro.intro.intro
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
this : l₁' = []
⊢ l₁' ++ l₂' <+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' = []

Tactic:
rw [eq_nil_iff_forall_not_mem]

Result:
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ ∀ (a : α✝), ¬a ∈ l₁'

Proof state:
α✝ : Type u_1
l l₁ l₂ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₁
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
⊢ l <+ l₂

Tactic:
obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h

Result:
case intro.intro.intro.intro
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₂

Proof state:
case intro.intro.intro.intro
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
this : l₁' = []
⊢ l₁' ++ l₂' <+ l₂

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
l l₁ l₂ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₁
h : l <+ l₁ ++ l₂
⊢ l <+ l₂

Tactic:
rw [sublist_append_iff] at h

Result:
α✝ : Type u_1
l l₁ l₂ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₁
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
⊢ l <+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₁
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ ∀ (a : α✝), ¬a ∈ l₁'

Tactic:
exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
lemma _root_.fderiv_continuousLinearEquiv_comp (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) (x : E) :
    fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) x =
      (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x =
    (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)

Tactic:
rw [ContinuousLinearEquiv.comp_fderiv]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (fun x => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)

Tactic:
change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = _

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x =
    (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
-- Mathlib/Logic/Relation.lean
theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
  | a, _, refl => by rfl
  | _, _, single h => ReflTransGen.tail ReflTransGen.refl h

Proof state:
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_pure {b : β} : f ×ˢ pure b = map (fun a => (a, b)) f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ f ×ˢ pure b = map (fun a => (a, b)) f

Tactic:
rw [prod_eq, seq_pure, map_map]

Result:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_id (N : Matroid β) : N.comap id = N :=
  ext_indep rfl <| by simp [injective_id.injOn]

Proof state:
β : Type u_2
N : Matroid β
⊢ ∀ ⦃I : Set β⦄, I ⊆ (N.comap id).E → ((N.comap id).Indep I ↔ N.Indep I)

Tactic:
simp [injective_id.injOn]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_le_bot_iff (f : M →ₛₗ[τ₁₂] M₂) : range f ≤ ⊥ ↔ f = 0

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range f ≤ ⊥ ↔ f = 0

Tactic:
rw [range_le_iff_comap]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Tactic:
exact ker_eq_top

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableAtFilter_top : IntegrableAtFilter f ⊤ μ ↔ Integrable f μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
⊢ IntegrableAtFilter f ⊤ μ ↔ Integrable f μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.integrableAtFilter ⊤⟩

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
h : IntegrableAtFilter f ⊤ μ
⊢ Integrable f μ

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s : Set α
hsf : s ∈ ⊤
hs : IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
exact (integrableOn_iff_integrable_of_support_subset fun _ _ ↦ hsf _).mp hs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
h : IntegrableAtFilter f ⊤ μ
⊢ Integrable f μ

Tactic:
obtain ⟨s, hsf, hs⟩ := h

Result:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s : Set α
hsf : s ∈ ⊤
hs : IntegrableOn f s μ
⊢ Integrable f μ
-- Mathlib/Combinatorics/Colex.lean
lemma insert_lt_insert (ha : a ∉ s) (hb : b ∉ s) :
    toColex (insert a s) < toColex (insert b s) ↔ a < b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := insert a s } < { ofColex := insert b s } ↔ a < b

Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem tangentMap_tangentBundle_pure [Is : IsManifold I 1 M]
    (p : TangentBundle I M) :
    tangentMap I I.tangent (zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩

Proof state:
case mk.e_a
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0))
      (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x)) =
    fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))

Tactic:
refine fderivWithin_congr (fun y hy => ?_) ?_

Result:
case mk.e_a.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
y : E
hy : y ∈ range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm y))), 0) = (y, 0)

case mk.e_a.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x
B :
  (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm (↑I (↑(chartAt H x) x))))), 0) =
    (↑I (↑(chartAt H x) x), 0)
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem AddTorsor.subsingleton_iff (G P : Type*) [AddGroup G] [AddTorsor G P] :
    Subsingleton G ↔ Subsingleton P

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
exact (Equiv.vaddConst default).subsingleton_congr

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
inhabit P

Result:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_zero (a : R) : a ^ 0 = (nat_lit 1).rawCast + 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ 0 = Nat.rawCast 1 + 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldl_subtype {p : α → Prop} {l : List { x // p x }}
    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
    l.foldl f x = l.unattach.foldl g x

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldl f x l = foldl g x (map (fun x => x.val) l)
x : β
⊢ foldl f x (a :: l) = foldl g x (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
x : β
⊢ foldl f x [] = foldl g x (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x (map (fun x => x.val) l)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x (map (fun x => x.val) l)

Tactic:
induction l generalizing x with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem ofSet_univ_eq_refl : ofSet univ isOpen_univ = PartialHomeomorph.refl X

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ofSet univ ⋯ = PartialHomeomorph.refl X

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_eq_pi_iff {θ : Angle} : (2 : ℤ) • θ = π ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ)

Proof state:
θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
/-- **No wrap-around principle**.

The first `k + 1` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k + 1` elements
of `ℕ` assuming there is no wrap-around. -/
lemma isAddFreimanIso_Iic (hm : m ≠ 0) (hkmn : m * k ≤ n) :
    IsAddFreimanIso m (Iic (k : Fin (n + 1))) (Iic k) val where
  bijOn.left

Proof state:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ ↑k
hu : u.card = m
⊢ (map val u).sum ≤ m * k

Tactic:
rw [← hu, ← card_map]

Result:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ ↑k
hu : u.card = m
⊢ (map val u).sum ≤ (map ?f u).card * k

case f
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ ↑k
hu : u.card = m
⊢ Fin (n + 1) → ?m.208397

k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
u : Multiset (Fin (n + 1))
huk : ∀ x ∈ u, x ≤ ↑k
hu : u.card = m
⊢ Type ?u.208395
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem UniformEquicontinuousOn.closure' {A : Set Y} {u : Y → β → α} {S : Set β}
    (hA : UniformEquicontinuousOn (u ∘ (↑) : A → β → α) S) (hu : Continuous (S.restrict ∘ u)) :
    UniformEquicontinuousOn (u ∘ (↑) : closure A → β → α) S

Proof state:
case h.mk.intro
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous (S.restrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy : ∀ (i : ↑A), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ U

Tactic:
rw [SetCoe.forall] at *

Result:
case h.mk.intro
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous (S.restrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ U

Proof state:
case h.mk.intro.refine_1
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous (S.restrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V
⊢ Continuous fun f => u f x

Tactic:
exact (continuous_apply ⟨x, hxS⟩).comp hu

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem map_lt_add_translationNumber_add_one (x : ℝ) : f x < x + τ f + 1 :=
  calc
    f x < x + ⌊τ f⌋ + 1 := f.map_lt_add_floor_translationNumber_add_one x
    _ ≤ x + τ f + 1

Proof state:
case bc.bc
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f

Tactic:
apply floor_le

Result:
no goals

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ x + ↑⌊τ f⌋ + 1 ≤ x + τ f + 1

Tactic:
gcongr

Result:
case bc.bc
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_eq_cons_Ioc (h : a ≤ b) : Icc a b = (Ioc a b).cons a left_not_mem_Ioc

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioc_insert_left h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
rw [cons_eq_insert, Ioc_insert_left h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_pos_of_root {p : R[X]} (hp : p ≠ 0) (h : IsRoot p a) : 0 < degree p :=
  lt_of_not_ge fun hlt => by
    have := eq_C_of_degree_le_zero hlt
    rw [IsRoot, this, eval_C] at h
    simp only [h, RingHom.map_zero] at this
    exact hp this

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : 0 ≥ p.degree
⊢ False

Tactic:
have := eq_C_of_degree_le_zero hlt

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : 0 ≥ p.degree
this : p = C (p.coeff 0)
⊢ False

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : 0 ≥ p.degree
this : p = C (p.coeff 0)
⊢ False

Tactic:
rw [IsRoot, this, eval_C] at h

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : 0 ≥ p.degree
this : p = C (p.coeff 0)
⊢ False

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : 0 ≥ p.degree
this : p = C (p.coeff 0)
⊢ False

Tactic:
simp only [h, RingHom.map_zero] at this

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : 0 ≥ p.degree
this : p = 0
⊢ False

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : 0 ≥ p.degree
this : p = 0
⊢ False

Tactic:
exact hp this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertManyIfNewUnit_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit m l).1 k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
fallback : Unit
⊢ getD (insertManyIfNewUnit m l).val k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem subNat_zero (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i

Proof state:
case h
n : Nat
i : Fin n
h : 0 ≤ ↑i
⊢ ↑(subNat 0 i h) = ↑i

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
i : Fin n
h : 0 ≤ ↑i
⊢ subNat 0 i h = i

Tactic:
ext

Result:
case h
n : Nat
i : Fin n
h : 0 ≤ ↑i
⊢ ↑(subNat 0 i h) = ↑i
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.of_inv (hf : Multipliable fun b ↦ (f b)⁻¹) : Multipliable f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable fun b => (f b)⁻¹
⊢ Multipliable f

Tactic:
simpa only [inv_inv] using hf.inv

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem EqOn.cancel_right (hf : s.EqOn (g₁ ∘ f) (g₂ ∘ f)) (hf' : s.SurjOn f t) : t.EqOn g₁ g₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
⊢ EqOn g₁ g₂ t

Tactic:
intro b hb

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)

Tactic:
exact hf ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf' hb

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem toWord_injective : Function.Injective (toWord : FreeGroup α → List (α × Bool))

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂

Tactic:
exact reduce.exact

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ Function.Injective toWord

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
-- Mathlib/Algebra/CharP/Two.lean
theorem of_one_ne_zero_of_two_eq_zero (h₁ : (1 : R) ≠ 0) (h₂ : (2 : R) = 0) : CharP R 2 where
  cast_eq_zero_iff' n

Proof state:
case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ¬↑n = 0

Tactic:
rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.two_dvd, iff_true]

Result:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0

Proof state:
case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.not_two_dvd_nat, iff_false]

Result:
case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ¬↑n = 0

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
obtain hn | hn := Nat.even_or_odd n

Result:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0 ↔ 2 ∣ n

case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ↑n = 0 ↔ 2 ∣ n

Proof state:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0

Tactic:
exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂

Result:
no goals