harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsStrictRestriction.exists_eq_restrict (h : N <r M) : ∃ R, R ⊂ M.E ∧ N = M ↾ R :=
  ⟨N.E, h.ssubset, by rw [h.eq_restrict]⟩

Proof state:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N = M ↾ N.E

Tactic:
rw [h.eq_restrict]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_left_comm : a ∆ (b ∆ c) = b ∆ (a ∆ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)

Tactic:
simp_rw [← symmDiff_assoc, symmDiff_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head_attachWith {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) :
    (xs.attachWith P H).head h = ⟨xs.head (by simpa using h), H _ (head_mem _)⟩

Proof state:
α : Type ?u.47210
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : xs.attachWith P H ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
case nil
α : Type u_1
P : α → Prop
H : ∀ (a : α), a ∈ [] → P a
h : [].attachWith P H ≠ []
⊢ ([].attachWith P H).head h = ⟨[].head ⋯, ⋯⟩

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
P : α → Prop
x : α
xs : List α
H : ∀ (a : α), a ∈ x :: xs → P a
h : (x :: xs).attachWith P H ≠ []
⊢ ((x :: xs).attachWith P H).head h = ⟨(x :: xs).head ⋯, ⋯⟩

Tactic:
simp [head_attachWith, h]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : xs.attachWith P H ≠ []
⊢ (xs.attachWith P H).head h = ⟨xs.head ⋯, ⋯⟩

Tactic:
cases xs with
| nil => simp at h
| cons x xs => simp [head_attachWith, h]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.eq_bot_of_minimalPrimes_eq_empty (h : I.minimalPrimes = ∅) : I = ⊤

Proof state:
case intro.mk
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ False

Tactic:
exact Set.not_mem_empty p (h ▸ hp)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by_contra hI

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes hI

Result:
case intro.mk
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ False
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma differentialAlgebraFiniteDimensional [FiniteDimensional F K] :
    letI := differentialFiniteDimensional F K
    DifferentialAlgebra F K

Proof state:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this : Fact (minpoly F k).Monic
⊢ DifferentialAlgebra F K

Tactic:
haveI : Fact (Irreducible (minpoly F k)) :=
  ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩

Result:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this✝ : Fact (minpoly F k).Monic
this : Fact (Irreducible (minpoly F k))
⊢ DifferentialAlgebra F K

Proof state:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
⊢ DifferentialAlgebra F K

Tactic:
haveI h : F⟮k⟯ = ⊤ := (Field.exists_primitive_element F K).choose_spec

Result:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
⊢ DifferentialAlgebra F K

Proof state:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
⊢ DifferentialAlgebra F K

Tactic:
let k := (Field.exists_primitive_element F K).choose

Result:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
⊢ DifferentialAlgebra F K

Proof state:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this✝ : Fact (minpoly F k).Monic
this : Fact (Irreducible (minpoly F k))
⊢ DifferentialAlgebra F K

Tactic:
apply DifferentialAlgebra.equiv

Result:
no goals

Proof state:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
⊢ DifferentialAlgebra F K

Tactic:
haveI : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩

Result:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this : Fact (minpoly F k).Monic
⊢ DifferentialAlgebra F K
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
@[simp, mfld_simps] lemma sum_chartAt_inl_apply {x y : M} :
    (chartAt H (.inl x : M ⊕ M')) (Sum.inl y) = (chartAt H x) y

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inl y) = ↑(chartAt H x) y

Tactic:
exact PartialHomeomorph.lift_openEmbedding_apply _ _

Result:
no goals

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
this : Nonempty H
⊢ ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y

Tactic:
rw [ChartedSpace.sum_chartAt_inl]

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
this : Nonempty H
⊢ ↑((chartAt H x).lift_openEmbedding ⋯) (Sum.inl y) = ↑(chartAt H x) y

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
⊢ ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y

Tactic:
haveI : Nonempty H := nonempty_of_chartedSpace x

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
this : Nonempty H
⊢ ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem star_mul_self_ne_zero_iff (x : E) : x⋆ * x ≠ 0 ↔ x ≠ 0

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x⋆ * x ≠ 0 ↔ x ≠ 0

Tactic:
simp only [Ne, star_mul_self_eq_zero_iff]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem aeval_of_algebraicIndependent
    {f : ι → MvPolynomial ι R} (hf : AlgebraicIndependent R f) :
    AlgebraicIndependent R fun i ↦ aeval x (f i)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval fun i => (aeval x) (f i)) p = 0
⊢ p = 0

Tactic:
exact hf _ (hx _ (by rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp))

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι → MvPolynomial ι R
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent R fun i => (aeval x) (f i)

Tactic:
rw [algebraicIndependent_iff] at hx hf ⊢

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval fun i => (aeval x) (f i)) p = 0
⊢ (aeval x) ((aeval f) p) = 0

Tactic:
rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0

Tactic:
intro p hp

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval fun i => (aeval x) (f i)) p = 0
⊢ p = 0
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
lemma extChartAt_inr_apply {x y : M'} :
    (extChartAt I (.inr x : M ⊕ M')) (Sum.inr y) = (extChartAt I x) y

Proof state:
𝕜 : 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
M' : Type u_16
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x y : M'
⊢ ↑(extChartAt I (Sum.inr x)) (Sum.inr y) = ↑(extChartAt I x) y

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0

Tactic:
calc
  ∑ x ∈ Icc a b, (if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x := by
    congr! with x hx; exact if_pos (mem_Icc.1 hx).2
  _ = ∑ x ∈ Icc (ofDual b) (ofDual a), mu 𝕜 x (ofDual a) := by simp [Icc_orderDual_def, mud]
  _ = if ofDual b = ofDual a then 1 else 0 := sum_Icc_mu_left ..
  _ = if a = b then 1 else 0 := by simp [eq_comm]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a

Tactic:
let mud : IncidenceAlgebra 𝕜 αᵒᵈ :=
  { toFun := fun a b ↦ mu 𝕜 (ofDual b) (ofDual a)
    eq_zero_of_not_le' := fun a b hab ↦ apply_eq_zero_of_not_le (by exact hab) _ }

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ mud (toDual a) (toDual b) = (mu 𝕜) b a

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud

Tactic:
rw [← mu_mul_zeta] at this

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = mu 𝕜 * zeta 𝕜
⊢ mu 𝕜 = mud
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_eq_top_of_not_connected [Nonempty α] (h : ¬G.Connected) : G.ediam = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
⊢ G.ediam = ⊤

Tactic:
obtain ⟨_, hw⟩ := h Classical.ofNonempty

Result:
case intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.ediam = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬∃ v, ∀ (w : α), G.Reachable v w
⊢ G.ediam = ⊤

Tactic:
push_neg at h

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
⊢ G.ediam = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.Connected
⊢ G.ediam = ⊤

Tactic:
rw [connected_iff_exists_forall_reachable] at h

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬∃ v, ∀ (w : α), G.Reachable v w
⊢ G.ediam = ⊤

Proof state:
case intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.edist Classical.ofNonempty w✝ ≤ G.ediam

Tactic:
exact edist_le_ediam

Result:
no goals

Proof state:
case intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.ediam = ⊤

Tactic:
rw [eq_top_iff, ← edist_eq_top_of_not_reachable hw]

Result:
case intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.edist Classical.ofNonempty w✝ ≤ G.ediam
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma integrable [IsFiniteMeasure μ] (f : X →ᵇ E) :
    Integrable f μ

Proof state:
X : Type u_1
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ HasFiniteIntegral (⇑f) μ

Tactic:
calc  ∫⁻ x, ‖f x‖₊ ∂μ
  _ ≤ ‖f‖₊ * (μ Set.univ)   := f.lintegral_nnnorm_le μ
  _ < ∞                     := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

Result:
no goals

Proof state:
X : Type u_1
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable (⇑f) μ

Tactic:
refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩

Result:
X : Type u_1
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ HasFiniteIntegral (⇑f) μ
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniSeq_lt_eulerMascheroniConstant (n : ℕ) :
    eulerMascheroniSeq n < eulerMascheroniConstant

Proof state:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniConstant

Tactic:
refine (strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_

Result:
n : ℕ
⊢ eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant

Proof state:
n : ℕ
⊢ eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant

Tactic:
apply strictMono_eulerMascheroniSeq.monotone.ge_of_tendsto tendsto_eulerMascheroniSeq

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive existing]
lemma cast_divConst (A B : Finset G) : (δₘ[A, B] : 𝕜) = #(A / B) / #A

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑δₘ[A, B] = ↑(#(A / B)) / ↑(#A)

Tactic:
simp [divConst]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdrop_eq_reverse_drop_reverse : l.rdrop n = reverse (l.reverse.drop n)

Proof state:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse

Tactic:
induction' l using List.reverseRecOn with xs x IH generalizing n

Result:
case nil
α : Type u_1
n : ℕ
⊢ take ([].length - n) [] = (drop n [].reverse).reverse

case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Proof state:
case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Tactic:
cases n

Result:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
⊢ take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse

case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n✝ : ℕ
⊢ take ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (drop (n✝ + 1) (xs ++ [x]).reverse).reverse

Proof state:
case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n✝ : ℕ
⊢ take ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (drop (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [take_append_eq_append_take, IH]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : ℕ
⊢ l.rdrop n = (drop n l.reverse).reverse

Tactic:
rw [rdrop]

Result:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse

Proof state:
case nil
α : Type u_1
n : ℕ
⊢ take ([].length - n) [] = (drop n [].reverse).reverse

Tactic:
simp

Result:
no goals

Proof state:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
⊢ take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse

Tactic:
simp [take_append]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem sum_le_of_monotoneOn_Iic (f : α → E) {s : Set α} {n : ℕ} {u : ℕ → α}
    (hu : MonotoneOn u (Iic n)) (us : ∀ i ≤ n, u i ∈ s) :
    (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
hu : MonotoneOn u (Iic n)
us : ∀ i ≤ n, u i ∈ s
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
simpa using sum_le_of_monotoneOn_Icc f (m := 0) (hu.mono Icc_subset_Iic_self) fun i hi ↦ us i hi.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_push_iff {a b c : Array α} {x : α} :
    a ++ b = c.push x ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b')

Proof state:
case mk
α : Type u_1
b c : Array α
x : α
a : List α
⊢ { toList := a } ++ b = c.push x ↔
    b = #[] ∧ { toList := a } = c.push x ∨ ∃ b', b = b'.push x ∧ c = { toList := a } ++ b'

Tactic:
rcases b with ⟨b⟩

Result:
case mk.mk
α : Type u_1
c : Array α
x : α
a b : List α
⊢ { toList := a } ++ { toList := b } = c.push x ↔
    { toList := b } = #[] ∧ { toList := a } = c.push x ∨ ∃ b', { toList := b } = b'.push x ∧ c = { toList := a } ++ b'

Proof state:
case mk.mk.mk.mp
α : Type u_1
x : α
a b c : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = c ++ c' ∧ [x] = c' ++ b) →
    b = [] ∧ a = c ++ [x] ∨ ∃ b', { toList := b } = b'.push x ∧ c = a ++ b'.toList

Tactic:
rintro (⟨a', rfl, rfl⟩ | ⟨b', rfl, h⟩)

Result:
case mk.mk.mk.mp.inl.intro.intro
α : Type u_1
x : α
a a' : List α
⊢ a' ++ [x] = [] ∧ a = a ++ a' ++ [x] ∨ ∃ b', { toList := a' ++ [x] } = b'.push x ∧ a ++ a' = a ++ b'.toList

case mk.mk.mk.mp.inr.intro.intro
α : Type u_1
x : α
b c b' : List α
h : [x] = b' ++ b
⊢ b = [] ∧ c ++ b' = c ++ [x] ∨ ∃ b'_1, { toList := b } = b'_1.push x ∧ c = c ++ b' ++ b'_1.toList

Proof state:
α : Type u_1
x : α
c : List α
⊢ c ++ [x] = c ++ [x] ∧ [x] = [x] ++ []

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_zip_left {l₁ : Vector α n} {l₂ : Vector β n}  :
    (unzip (zip l₁ l₂)).1 = l₁

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
⊢ (l₁.zip l₂).unzip.fst = l₁

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip.fst = { toArray := l₁, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip.fst = { toArray := l₁, size_toArray := ⋯ }

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip.fst =
    { toArray := l₁, size_toArray := ⋯ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip.fst =
    { toArray := l₁, size_toArray := ⋯ }

Tactic:
simp [Array.unzip_zip_left, h, Array.map_fst_zip]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mul_bot : I * ⊥ = ⊥

Proof state:
R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ I * ⊥ = ⊥

Tactic:
simp

Result:
no goals