harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem PrimeSpectrum.comap_residue (T : Type u) [CommRing T] [IsLocalRing T]
    (x : PrimeSpectrum (ResidueField T)) : PrimeSpectrum.comap (residue T) x = closedPoint T

Proof state:
case asIdeal
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ ((PrimeSpectrum.comap (residue T)) ⊥).asIdeal = (closedPoint T).asIdeal

Tactic:
exact Ideal.mk_ker

Result:
no goals

Proof state:
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ (PrimeSpectrum.comap (residue T)) x = closedPoint T

Tactic:
rw [Subsingleton.elim x ⊥]

Result:
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ (PrimeSpectrum.comap (residue T)) ⊥ = closedPoint T

Proof state:
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ (PrimeSpectrum.comap (residue T)) ⊥ = closedPoint T

Tactic:
ext1

Result:
case asIdeal
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ ((PrimeSpectrum.comap (residue T)) ⊥).asIdeal = (closedPoint T).asIdeal
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_add_le_finrank_add_finrank (s t : Submodule K V) [FiniteDimensional K s]
    [FiniteDimensional K t] : finrank K (s ⊔ t : Submodule K V) ≤ finrank K s + finrank K t

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)

Tactic:
exact self_le_add_right _ _

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥s + finrank K ↥t

Tactic:
rw [← finrank_sup_add_finrank_inf_eq]

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem lt_mul_of_one_lt_left [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) : b < a * b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem id_c_app (X : PresheafedSpace C) (U) :
    (𝟙 X : X ⟶ X).c.app U = X.presheaf.map (𝟙 U)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X.presheaf).app U = 𝟙 (X.presheaf.obj U)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
rw [id_c, map_id]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X.presheaf).app U = 𝟙 (X.presheaf.obj U)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem anyM_toList [Monad m] (p : α → m Bool) (v : Vector α n) :
    v.toList.anyM p = v.anyM p

Proof state:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
v : Vector α n
⊢ List.anyM p v.toList = anyM p v

Tactic:
cases v

Result:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem proj_comp_of_subset (h : ∀ i, J i → K i) : (Proj J ∘ Proj K) =
    (Proj J : (I → Bool) → (I → Bool))

Proof state:
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ Proj J ∘ Proj K = Proj J

Tactic:
ext x i

Result:
case h.h
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (Proj J ∘ Proj K) x i = Proj J x i

Proof state:
case h.h
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (Proj J ∘ Proj K) x i = Proj J x i

Tactic:
dsimp [Proj]

Result:
case h.h
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false

Proof state:
case h.h
I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_mono_cokernel_desc [S.HasHomology] [HasCokernel S.f] :
    S.Exact ↔ Mono (cokernel.desc S.f S.g S.zero)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.opcyclesIsoCokernel.symm.hom ≫ (Arrow.mk S.fromOpcycles).hom =
    (Arrow.mk (cokernel.desc S.f S.g ⋯)).hom ≫ (Iso.refl (Arrow.mk (cokernel.desc S.f S.g ⋯)).right).hom

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ Mono S.fromOpcycles ↔ Mono (cokernel.desc S.f S.g ⋯)

Tactic:
refine (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ Arrow.mk (cokernel.desc S.f S.g ⋯) ≅ Arrow.mk S.fromOpcycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ Arrow.mk (cokernel.desc S.f S.g ⋯) ≅ Arrow.mk S.fromOpcycles

Tactic:
exact Arrow.isoMk S.opcyclesIsoCokernel.symm (Iso.refl _) (by aesop_cat)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.Exact ↔ Mono (cokernel.desc S.f S.g ⋯)

Tactic:
rw [exact_iff_mono_fromOpcycles]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ Mono S.fromOpcycles ↔ Mono (cokernel.desc S.f S.g ⋯)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_le_of_range_subset {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal}
    (h : Set.range f ⊆ Set.range g) : lsub.{u, max v w} f ≤ lsub.{v, max u w} g :=
  sup_le_of_range_subset.{u, v, w} (by convert Set.image_subset succ h <;> apply Set.range_comp)

Proof state:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)

Tactic:
convert Set.image_subset succ h <;> apply Set.range_comp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_ofReal_im (x : ℂ) (y : ℝ) : (x ^ (y : ℂ)).im = ‖x‖ ^ y * Real.sin (arg x * y)

Proof state:
x : ℂ
y : ℝ
⊢ (x ^ ↑y).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
rw [cpow_ofReal]

Result:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Proof state:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z

Tactic:
simp [Real.sin]

Result:
no goals

Proof state:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
generalize arg x * y = z

Result:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem leftUnitor_tensor_inv (X Y : C) :
    (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Exact.lean
/-- A necessary and sufficient condition for an exact sequence to descend to a quotient. -/
lemma Exact.exact_mapQ_iff
    (hfg : Exact f g) {p q r} (hpq : p ≤ comap f q) (hqr : q ≤ comap g r) :
    Exact (mapQ p q f hpq) (mapQ q r g hqr) ↔ range g ⊓ r ≤ map g q

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (ker (q.mapQ r g hqr)) = comap q.mkQ (range (p.mapQ q f hpq)) ↔ range g ⊓ r ≤ map g q

Tactic:
dsimp only [mapQ]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (ker (q.liftQ (r.mkQ ∘ₗ g) ⋯)) = comap q.mkQ (range (p.liftQ (q.mkQ ∘ₗ f) ⋯)) ↔ range g ⊓ r ≤ map g q

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (ker (q.liftQ (r.mkQ ∘ₗ g) ⋯)) = comap q.mkQ (range (p.liftQ (q.mkQ ∘ₗ f) ⋯)) ↔ range g ⊓ r ≤ map g q

Tactic:
rw [← ker_comp, range_liftQ, liftQ_mkQ, ker_comp, range_comp, comap_map_eq,
  ker_mkQ, ker_mkQ, ← hfg.linearMap_ker_eq, sup_comm,
  ← LE.le.le_iff_eq (sup_le hqr (ker_le_comap g)),
  ← comap_map_eq, ← map_le_iff_le_comap, map_comap_eq]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ Exact ⇑(p.mapQ q f hpq) ⇑(q.mapQ r g hqr) ↔ range g ⊓ r ≤ map g q

Tactic:
rw [exact_iff, ← (comap_injective_of_surjective (mkQ_surjective _)).eq_iff]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (ker (q.mapQ r g hqr)) = comap q.mkQ (range (p.mapQ q f hpq)) ↔ range g ⊓ r ≤ map g q
-- Mathlib/Combinatorics/Configuration.lean
theorem lineCount_eq_pointCount [Finite P] [Finite L] (p : P) (l : L) :
    lineCount L p = pointCount P l :=
  Exists.elim (exists_point l) fun q hq =>
    (lineCount_eq_lineCount L p q).trans <| by
      cases nonempty_fintype P
      cases nonempty_fintype L
      exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
⊢ lineCount L q = pointCount P l

Tactic:
cases nonempty_fintype P

Result:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
val✝ : Fintype P
⊢ lineCount L q = pointCount P l

Proof state:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L q = pointCount P l

Tactic:
exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

Result:
no goals

Proof state:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
val✝ : Fintype P
⊢ lineCount L q = pointCount P l

Tactic:
cases nonempty_fintype L

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
val✝¹ : Fintype P
val✝ : Fintype L
⊢ lineCount L q = pointCount P l
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem lintegral_fn_integral_sub_comp ⦃f g : γ → E⦄ (F : E → ℝ≥0∞)
    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫⁻ x, F (∫ y, f y - g y ∂η x) ∂κ a = ∫⁻ x, F (∫ y, f y ∂η x - ∫ y, g y ∂η x) ∂κ a

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
simp [integral_sub h2f h2g]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫⁻ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
refine lintegral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y - g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y - g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x)

Tactic:
filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt
    (h : ¬MDifferentiableWithinAt I I' f s x) : mfderivWithin I I' f s x = 0

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : ¬MDifferentiableWithinAt I I' f s x
⊢ mfderivWithin I I' f s x = 0

Tactic:
simp only [mfderivWithin, h, if_neg, not_false_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma toSingle₀Equiv_symm_apply_f_zero {C : ChainComplex V ℕ} {X : V}
    (f : C.X 0 ⟶ X) (hf : C.d 1 0 ≫ f = 0) :
    ((toSingle₀Equiv C X).symm ⟨f, hf⟩).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
hf : C.d 1 0 ≫ f = 0
⊢ ((C.toSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
simp [toSingle₀Equiv]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.noSibling_tail (le) (s : Heap α) : (s.tail le).NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (tail le s).NoSibling

Tactic:
simp only [Heap.tail]

Result:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ ((tail? le s).getD nil).NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
eq : tail? le s = none
⊢ (none.getD nil).NoSibling

Tactic:
cases s with cases eq | nil => constructor

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ ((some tl).getD nil).NoSibling

Tactic:
exact Heap.noSibling_tail? eq

Result:
no goals

Proof state:
case nil.refl
α : Type u_1
le : α → α → Bool
⊢ (none.getD nil).NoSibling

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ ((tail? le s).getD nil).NoSibling

Tactic:
match eq : s.tail? le with
| none => cases s with cases eq | nil => constructor
| some tl => exact Heap.noSibling_tail? eq

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem IsTerminal.mono_from {X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : Mono f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
this : IsSplitMono f
⊢ Mono f

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
⊢ Mono f

Tactic:
haveI := t.isSplitMono_from f

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
this : IsSplitMono f
⊢ Mono f
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).edges = p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edges = p.edges

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).edges = p.edges

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).edges = p.edges

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
theorem Convex.interior_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V}
    (hs : Convex ℝ s) : (interior s).Nonempty ↔ affineSpan ℝ s = ⊤

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (interior s).Nonempty ↔ affineSpan ℝ s = ⊤

Tactic:
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_mk (as : List α) : (Array.mk as).size = as.length

Proof state:
α : Type u_1
as : List α
⊢ { toList := as }.size = as.length

Tactic:
simp [size]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true

Proof state:
w : Nat
x y : BitVec w
⊢ x.ule y = carry w y (~~~x) true

Tactic:
simp [ule_eq_not_ult, ult_eq_not_carry]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_add_diff (hs : NullMeasurableSet s μ) (t : Set α) :
    μ s + μ (t \ s) = μ (s ∪ t)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ μ s + μ (t \ s) = μ (s ∪ t)

Tactic:
rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_diff_self]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem surjective_of_iterate_surjective {n : ℕ} (hn : n ≠ 0) (h : Surjective (f' ^ n)) :
    Surjective f'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))
⊢ Surjective ⇑f'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))
⊢ Surjective ⇑f'

Tactic:
exact Surjective.of_comp h

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_commute (s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s, Commute y x) :
    Commute y (s.noncommProd comm)

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y a✝.prod

Tactic:
exact Commute.list_prod_right _ _ h

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y (noncommProd ⟦a✝⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe]

Result:
case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y a✝.prod

Proof state:
α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
y : α
h : ∀ x ∈ s, Commute y x
⊢ Commute y (s.noncommProd comm)

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y (noncommProd ⟦a✝⟧ comm)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem decide_mem_replicate [BEq α] [LawfulBEq α] {a b : α} :
    ∀ {n}, decide (b ∈ replicate n a) = ((¬ n == 0) && b == a)
  | 0 => by simp
  | n+1 => by simp [replicate_succ, decide_mem_replicate, Nat.succ_ne_zero]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ decide (b ∈ replicate 0 a) = (decide ¬(0 == 0) = true && b == a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ decide (b ∈ replicate (n + 1) a) = (decide ¬(n + 1 == 0) = true && b == a)

Tactic:
simp [replicate_succ, decide_mem_replicate, Nat.succ_ne_zero]

Result:
no goals