harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_sInf (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) :
    (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

Proof state:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

Tactic:
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs

Result:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

Proof state:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

Tactic:
simpa only [← sInf_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iInf hf)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
theorem tensor_id (X₁ X₂ : C) : tensorHom ℬ (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj ℬ X₁ X₂)

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ (ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ (ℬ X₁ X₂).cone.π.app { as := WalkingPair.right }

Tactic:
dsimp [tensorHom]

Result:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ (ℬ X₁ X₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.snd (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.snd (ℬ X₁ X₂).cone

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ (ℬ X₁ X₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.snd (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.snd (ℬ X₁ X₂).cone

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj ℬ X₁ X₂)

Tactic:
apply IsLimit.hom_ext (ℬ _ _).isLimit

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ (ℬ X₁ X₂).cone.π.app j = 𝟙 (tensorObj ℬ X₁ X₂) ≫ (ℬ X₁ X₂).cone.π.app j
-- Mathlib/Analysis/Convex/Between.lean
theorem affineSegment_image (f : P →ᵃ[R] P') (x y : P) :
    f '' affineSegment R x y = affineSegment R (f x) (f y)

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ ⇑f '' affineSegment R x y = affineSegment R (f x) (f y)

Tactic:
rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ (fun x_1 => f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(f.comp (lineMap x y)) '' Set.Icc 0 1

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ (fun x_1 => f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(f.comp (lineMap x y)) '' Set.Icc 0 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Indep.exists_isBasis_subset_union_isBasis (hI : M.Indep I) (hIX : I ⊆ X)
    (hJ : M.IsBasis J X) : ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
obtain ⟨I', hI', hII', hI'IJ⟩ :=
  (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : M.IsBasis I' X
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
exact ⟨I', hI', hII', hI'IJ⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J

Tactic:
rw [isBase_restrict_iff] at hI'

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : M.IsBasis I' X
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
-- Mathlib/Tactic/Abel.lean
theorem term_add_term {α} [AddCommMonoid α] (n₁ x a₁ n₂ a₂ n' a') (h₁ : n₁ + n₂ = n')
    (h₂ : a₁ + a₂ = a') : @term α _ n₁ x a₁ + @term α _ n₂ x a₂ = term n' x a'

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
n₁ : ℕ
x a₁ : α
n₂ : ℕ
a₂ : α
n' : ℕ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ term n₁ x a₁ + term n₂ x a₂ = term n' x a'

Tactic:
simp [h₁.symm, h₂.symm, term, add_nsmul, add_assoc, add_left_comm]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem commutator_subset_ker : commutator G ≤ f.ker

Proof state:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ f.ker

Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]

Result:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑f.ker

Proof state:
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑f.ker

Tactic:
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑f.ker

Tactic:
rintro x ⟨p, q, rfl⟩

Result:
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑f.ker
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem mconv_add [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ]
    [SFinite ν] [SFinite ρ] : μ ∗ (ν + ρ) = μ ∗ ν + μ ∗ ρ

Proof state:
case hf
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ Measurable fun x => x.1 * x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ μ ∗ (ν + ρ) = μ ∗ ν + μ ∗ ρ

Tactic:
unfold mconv

Result:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ map (fun x => x.1 * x.2) (μ.prod (ν + ρ)) = map (fun x => x.1 * x.2) (μ.prod ν) + map (fun x => x.1 * x.2) (μ.prod ρ)

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ map (fun x => x.1 * x.2) (μ.prod (ν + ρ)) = map (fun x => x.1 * x.2) (μ.prod ν) + map (fun x => x.1 * x.2) (μ.prod ρ)

Tactic:
rw [prod_add, map_add]

Result:
case hf
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ Measurable fun x => x.1 * x.2
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_neg (hi : i < i0) : toZ i0 i < 0

Proof state:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Tactic:
rw [← h_eq, h] at hi

Result:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[(-0).toNat] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Proof state:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0

Tactic:
by_contra h

Result:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ False

Proof state:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
⊢ False

Tactic:
have h_eq := iterate_pred_toZ i hi

Result:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Proof state:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

Tactic:
rw [toZ_of_lt hi]

Result:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ -↑(Nat.find ⋯) ≤ 0

Proof state:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ -↑(Nat.find ⋯) ≤ 0

Tactic:
omega

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[(-0).toNat] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Tactic:
simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i < 0

Tactic:
refine lt_of_le_of_ne ?_ ?_

Result:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem tangentMap_comp (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
    tangentMap I I'' (g ∘ f) = tangentMap I' I'' g ∘ tangentMap I I' f

Proof state:
case h
𝕜 : 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
p : TangentBundle I M
⊢ tangentMap I I'' (g ∘ f) p = (tangentMap I' I'' g ∘ tangentMap I I' f) p

Tactic:
exact tangentMap_comp_at _ (hg _) (hf _)

Result:
no goals

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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
⊢ tangentMap I I'' (g ∘ f) = tangentMap I' I'' g ∘ tangentMap I I' f

Tactic:
ext p : 1

Result:
case h
𝕜 : 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiable I I' f
p : TangentBundle I M
⊢ tangentMap I I'' (g ∘ f) p = (tangentMap I' I'' g ∘ tangentMap I I' f) p
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the Möbius function converges absolutely at `s` if and only if `re s > 1`. -/
lemma LSeriesSummable_moebius_iff {s : ℂ} : LSeriesSummable ↗μ s ↔ 1 < s.re

Proof state:
case refine_1
s : ℂ
H : LSeriesSummable (fun n => ↑(μ n)) s
⊢ 1 < s.re

Tactic:
by_contra! h

Result:
case refine_1
s : ℂ
H : LSeriesSummable (fun n => ↑(μ n)) s
h : s.re ≤ 1
⊢ False

Proof state:
case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ |μ n| ≤ 1

Tactic:
exact abs_moebius_le_one

Result:
no goals

Proof state:
s : ℂ
H : LSeriesSummable (fun n => ↑(μ n)) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simpa

Result:
no goals

Proof state:
s : ℂ
⊢ LSeriesSummable (fun n => ↑(μ n)) s ↔ 1 < s.re

Tactic:
refine ⟨fun H ↦ ?_, LSeriesSummable_of_bounded_of_one_lt_re (m := 1) fun n _ ↦ ?_⟩

Result:
case refine_1
s : ℂ
H : LSeriesSummable (fun n => ↑(μ n)) s
⊢ 1 < s.re

case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ ‖↑(μ n)‖ ≤ 1

Proof state:
case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ ‖↑(μ n)‖ ≤ 1

Tactic:
norm_cast

Result:
case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ |μ n| ≤ 1

Proof state:
case refine_1
s : ℂ
H : LSeriesSummable (fun n => ↑(μ n)) s
h : s.re ≤ 1
⊢ False

Tactic:
exact not_LSeriesSummable_moebius_at_one <| LSeriesSummable.of_re_le_re (by simpa) H

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_add_sum {ι : Type*} (μ ν : ι → Measure α) : sum μ + sum ν = sum fun n => μ n + ν n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
⊢ sum μ + sum ν = sum fun n => μ n + ν n

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ + sum ν) s = (sum fun n => μ n + ν n) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ + sum ν) s = (sum fun n => μ n + ν n) s

Tactic:
simp only [add_apply, sum_apply _ hs, Pi.add_apply, coe_add,
  tsum_add ENNReal.summable ENNReal.summable]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.prod_mem_iff_exists_mem {I : Ideal R} (hI : I.IsPrime) (s : Finset R) :
    s.prod (fun x ↦ x) ∈ I ↔ ∃ p ∈ s, p ∈ I

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
exact hI.multiset_prod_mem_iff_exists_mem s.val

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
rw [Finset.prod_eq_multiset_prod, Multiset.map_id']

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.gcd_mul_left_cancel (m : ℕ+) {n k : ℕ+} :
    k.Coprime n → (k * m).gcd n = m.gcd n

Proof state:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n

Tactic:
intro h

Result:
m n k : ℕ+
h : k.Coprime n
⊢ (k * m).gcd n = m.gcd n

Proof state:
case a.H
m n k : ℕ+
h : k.Coprime n
⊢ (↑k).Coprime ↑n

Tactic:
simpa

Result:
no goals

Proof state:
case a
m n k : ℕ+
h : k.Coprime n
⊢ (↑k * ↑m).gcd ↑n = (↑m).gcd ↑n

Tactic:
apply Nat.Coprime.gcd_mul_left_cancel

Result:
case a.H
m n k : ℕ+
h : k.Coprime n
⊢ (↑k).Coprime ↑n

Proof state:
m n k : ℕ+
h : k.Coprime n
⊢ (k * m).gcd n = m.gcd n

Tactic:
apply eq

Result:
case a
m n k : ℕ+
h : k.Coprime n
⊢ ↑((k * m).gcd n) = ↑(m.gcd n)

Proof state:
case a
m n k : ℕ+
h : k.Coprime n
⊢ ↑((k * m).gcd n) = ↑(m.gcd n)

Tactic:
simp only [gcd_coe, mul_coe]

Result:
case a
m n k : ℕ+
h : k.Coprime n
⊢ (↑k * ↑m).gcd ↑n = (↑m).gcd ↑n
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem hasSum_mul_left_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) ↔ HasSum f a₁ :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹, HasSum.mul_left _⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => a₂ * f i) (a₂ * a₁)
⊢ HasSum f a₁

Tactic:
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem equiv_of_isEmpty (x y : PSet) [IsEmpty x.Type] [IsEmpty y.Type] : Equiv x y :=
  equiv_iff.2 <| by simp

Proof state:
x : PSet.{u_1}
y : PSet.{u_2}
inst✝¹ : IsEmpty x.Type
inst✝ : IsEmpty y.Type
⊢ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lift_compr₂ (g : P →ₗ[R] Q) : lift (f.compr₂ g) = g.comp (lift f) :=
  Eq.symm <| lift.unique fun _ _ => by simp

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
g : P →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (g ∘ₗ lift f) (x✝¹ ⊗ₜ[R] x✝) = ((f.compr₂ g) x✝¹) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_nat {x y : ℕ} : IsPell (⟨x, y⟩ : ℤ√(d a1)) ↔ x * x - d a1 * y * y = 1 :=
  ⟨fun h =>
    (Nat.cast_inj (R := ℤ)).1
      (by rw [Int.ofNat_sub (Int.le_of_ofNat_le_ofNat <| Int.le.intro_sub _ h)]; exact h),
    fun h =>
    show ((x * x : ℕ) - (d a1 * y * y : ℕ) : ℤ) = 1 by
      rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h]; rfl⟩

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = 1

Tactic:
rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h]

Result:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑1 = 1

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = ↑1

Tactic:
exact h

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x - Pell.d a1 * y * y) = ↑1

Tactic:
rw [Int.ofNat_sub (Int.le_of_ofNat_le_ofNat <| Int.le.intro_sub _ h)]

Result:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = ↑1

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑1 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt {ι} {f : ι → Cardinal} {c : Cardinal} (hι : #ι < c.ord.cof) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt_lift (by rwa [(#ι).lift_id])

Proof state:
ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hι : #ι < c.ord.cof
⊢ Cardinal.lift.{?u.31235, u_1} #ι < c.ord.cof

Tactic:
rwa [(#ι).lift_id]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem disjoint_right : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s

Proof state:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
rw [disjoint_comm, disjoint_left]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive (attr := simp)]
lemma map_comp_div [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) :
    f ∘ (g / h) = f ∘ g / f ∘ h

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Proof state:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
    (G.incMatrix R * (G.incMatrix R)ᵀ) a a = G.degree a

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (∑ x : Sym2 α, if x ∈ G.incidenceSet a then if x ∈ G.incidenceSet a then 1 else 0 else 0) =
    ∑ x : Sym2 α, if x ∈ G.incidenceSet a then 1 else 0

Tactic:
simp_all only [ite_true, sum_boole]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
rw [← sum_incMatrix_apply]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e : Sym2 α, incMatrix R G a e

Tactic:
simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (∑ x : Sym2 α, if x ∈ G.incidenceSet a then if x ∈ G.incidenceSet a then 1 else 0 else 0) =
    ∑ x : Sym2 α, if x ∈ G.incidenceSet a then 1 else 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
classical
rw [← sum_incMatrix_apply]
simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
simp_all only [ite_true, sum_boole]

Result:
no goals