harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem weird_seventy : Weird 70

Proof state:
case right
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70

Tactic:
rw [h]

Result:
case right
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 = 0 ∨ ∀ s ⊆ {1, 2, 5, 7, 10, 14, 35}, ∑ i ∈ s, i ≠ 70

Proof state:
⊢ 70 < ∑ i ∈ properDivisors 70, i ∧ (70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70)

Tactic:
have h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35} := by rfl

Result:
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ properDivisors 70, i ∧ (70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70)

Proof state:
case left
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ {1, 2, 5, 7, 10, 14, 35}, i

Tactic:
repeat norm_num

Result:
no goals

Proof state:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
s : Finset ℕ
hs : s ⊆ {1, 2, 5, 7, 10, 14, 35}
hs' : s ∈ {1, 2, 5, 7, 10, 14, 35}.powerset
⊢ ∑ i ∈ s, i ≠ 70

Tactic:
fin_cases hs' <;> decide

Result:
no goals

Proof state:
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ properDivisors 70, i ∧ (70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70)

Tactic:
constructor

Result:
case left
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ properDivisors 70, i

case right
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70

Proof state:
⊢ Weird 70

Tactic:
rw [Weird, Abundant, not_pseudoperfect_iff_forall]

Result:
⊢ 70 < ∑ i ∈ properDivisors 70, i ∧ (70 = 0 ∨ ∀ s ⊆ properDivisors 70, ∑ i ∈ s, i ≠ 70)

Proof state:
case left
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ properDivisors 70, i

Tactic:
rw [h]

Result:
case left
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ {1, 2, 5, 7, 10, 14, 35}, i

Proof state:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
s : Finset ℕ
hs : s ⊆ {1, 2, 5, 7, 10, 14, 35}
⊢ ∑ i ∈ s, i ≠ 70

Tactic:
have hs' := mem_powerset.mpr hs

Result:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
s : Finset ℕ
hs : s ⊆ {1, 2, 5, 7, 10, 14, 35}
hs' : s ∈ {1, 2, 5, 7, 10, 14, 35}.powerset
⊢ ∑ i ∈ s, i ≠ 70

Proof state:
⊢ properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}

Tactic:
rfl

Result:
no goals

Proof state:
case right
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 = 0 ∨ ∀ s ⊆ {1, 2, 5, 7, 10, 14, 35}, ∑ i ∈ s, i ≠ 70

Tactic:
right

Result:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ ∀ s ⊆ {1, 2, 5, 7, 10, 14, 35}, ∑ i ∈ s, i ≠ 70

Proof state:
case left
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ 70 < ∑ i ∈ {1, 2, 5, 7, 10, 14, 35}, i

Tactic:
norm_num

Result:
no goals

Proof state:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
⊢ ∀ s ⊆ {1, 2, 5, 7, 10, 14, 35}, ∑ i ∈ s, i ≠ 70

Tactic:
intro s hs

Result:
case right.h
h : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35}
s : Finset ℕ
hs : s ⊆ {1, 2, 5, 7, 10, 14, 35}
⊢ ∑ i ∈ s, i ≠ 70
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_self (x : V) : o.oangle x x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ o.oangle x x = 0

Tactic:
rw [oangle, kahler_apply_self, ← ofReal_pow]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(↑(‖x‖ ^ 2)).arg = 0

Proof state:
case h.e'_2.h.h.e'_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))
⊢ (↑(‖x‖ ^ 2)).arg = 0

Tactic:
apply arg_ofReal_of_nonneg

Result:
case h.e'_2.h.h.e'_1.hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))
⊢ 0 ≤ ‖x‖ ^ 2

Proof state:
case h.e'_2.h.h.e'_1.hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))
⊢ 0 ≤ ‖x‖ ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(↑(‖x‖ ^ 2)).arg = 0

Tactic:
convert QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π))

Result:
case h.e'_2.h.h.e'_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))
⊢ (↑(‖x‖ ^ 2)).arg = 0
-- Mathlib/Order/SuccPred/Limit.lean
lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
    IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsGLB s a
ha : a ∉ s
⊢ IsPredPrelimit a

Tactic:
simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 <| by
  rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]; gcongr; positivity

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p⁻¹ + 0 ≤ p⁻¹ + q⁻¹

Tactic:
gcongr

Result:
case bc
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ 0 ≤ q⁻¹

Proof state:
case bc
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ 0 ≤ q⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p⁻¹ ≤ 1

Tactic:
rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]

Result:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p⁻¹ + 0 ≤ p⁻¹ + q⁻¹
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationLineMapWeights_self [DecidableEq ι] (i : ι) (c : k) :
    affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
c : k
⊢ affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i

Tactic:
simp [affineCombinationLineMapWeights]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem ofRowLens_to_rowLens_eq_self {μ : YoungDiagram} : ofRowLens _ (rowLens_sorted μ) = μ

Proof state:
case cells.h.mk
μ : YoungDiagram
i j : ℕ
⊢ (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ

Tactic:
simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt

Result:
no goals

Proof state:
case cells.h.mk
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells

Tactic:
simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]

Result:
case cells.h.mk
μ : YoungDiagram
i j : ℕ
⊢ (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ

Proof state:
μ : YoungDiagram
⊢ ofRowLens μ.rowLens ⋯ = μ

Tactic:
ext ⟨i, j⟩

Result:
case cells.h.mk
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_eq_top_iff (k : ℕ) : N.ucs k = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
rw [eq_top_iff, ← lcs_le_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjectionFn_mem_orthogonal {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    orthogonalProjectionFn s p ∈ mk' p s.directionᗮ

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ orthogonalProjectionFn s p ∈ mk' p s.directionᗮ

Tactic:
rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑(mk' p s.directionᗮ)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑(mk' p s.directionᗮ)

Tactic:
exact Set.inter_subset_right

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma1_is_congruence (N : ℕ+) : IsCongruenceSubgroup (Gamma1 N)

Proof state:
N : ℕ+
A : SL(2, ℤ)
hA : ↑(↑A 0 0) = 1 ∧ ↑(↑A 0 1) = 0 ∧ ↑(↑A 1 0) = 0 ∧ ↑(↑A 1 1) = 1
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
simp only [hA, eq_self_iff_true, and_self_iff]

Result:
no goals

Proof state:
N : ℕ+
⊢ Γ(↑N) ≤ Gamma1 ↑N

Tactic:
intro A hA

Result:
N : ℕ+
A : SL(2, ℤ)
hA : A ∈ Γ(↑N)
⊢ A ∈ Gamma1 ↑N

Proof state:
N : ℕ+
A : SL(2, ℤ)
hA : A ∈ Γ(↑N)
⊢ A ∈ Gamma1 ↑N

Tactic:
simp only [Gamma1_mem, Gamma_mem] at *

Result:
N : ℕ+
A : SL(2, ℤ)
hA : ↑(↑A 0 0) = 1 ∧ ↑(↑A 0 1) = 0 ∧ ↑(↑A 1 0) = 0 ∧ ↑(↑A 1 1) = 1
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
N : ℕ+
⊢ IsCongruenceSubgroup (Gamma1 ↑N)

Tactic:
refine ⟨N, ?_⟩

Result:
N : ℕ+
⊢ Γ(↑N) ≤ Gamma1 ↑N
-- Mathlib/Topology/Bases.lean
theorem exists_countable_basis [SecondCountableTopology α] :
    ∃ b : Set (Set α), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
refine ⟨_, ?_, not_mem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩

Result:
case intro.intro.refine_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ b} \ {∅}).Countable

case intro.intro.refine_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Proof state:
case intro.intro.refine_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ b} \ {∅}).Countable

case intro.intro.refine_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}

Tactic:
exacts [((countable_setOf_finite_subset hb₁).image _).mono diff_subset, rfl]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem leadingCoeff_single [Nonempty A] (hD : D.Injective) (a : A) (r : R) :
    (single a r).leadingCoeff D = r

Proof state:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r) (Function.invFun D ⊥) = r

Tactic:
simp [hr]

Result:
no goals

Proof state:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r) (Function.invFun D (D a)) = r

Tactic:
rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r) (Function.invFun D (if r = 0 then ⊥ else D a)) = r

Tactic:
split_ifs with hr

Result:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r) (Function.invFun D ⊥) = r

case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r) (Function.invFun D (D a)) = r

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ leadingCoeff D (single a r) = r

Tactic:
rw [leadingCoeff, supDegree_single]

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₀₂_iff : (graph t).Adj (in₀ a) (in₂ c) ↔ ∃ b, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₀₂ h⟩

Proof state:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (graph t).Adj (in₀ a) (in₂ c) → ∃ b, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toENNRealVectorMeasure_zero : (0 : Measure α).toENNRealVectorMeasure = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
⊢ toENNRealVectorMeasure 0 = 0

Tactic:
ext i

Result:
case h
α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure 0) i = ↑0 i

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure 0) i = ↑0 i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.nonempty [RankPos M] (hB : M.IsBase B) : B.Nonempty

Proof state:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅

Proof state:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False

Tactic:
exact M.empty_not_isBase hB

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.fiberwise_right :
    f =O[l ×ˢ l'] g → ∀ᶠ a in l, (f ⟨a, ·⟩) =O[l'] (g ⟨a, ·⟩)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Tactic:
exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x => f (a, x)) =O[l'] fun x => g (a, x)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l

Tactic:
rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {a | ∃ c, {x | ‖f (a, x)‖ ≤ c * ‖g (a, x)‖} ∈ l'} ∈ l
-- Mathlib/Data/List/Forall2.lean
theorem Forall₂.imp (H : ∀ a b, R a b → S a b) {l₁ l₂} (h : Forall₂ R l₁ l₂) : Forall₂ S l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂

Tactic:
induction h <;> constructor <;> solve_by_elim

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Proof state:
α : Type u
s t : Set α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
simp only [subset_def, mem_insert_iff, or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem normalized_count_X_eq_of_coe {P : k[X]} (hP : P ≠ 0) :
    Multiset.count PowerSeries.X (normalizedFactors (P : k⟦X⟧)) =
      Multiset.count Polynomial.X (normalizedFactors P)

Proof state:
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ Multiset.count X (normalizedFactors ↑P) = Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
apply eq_of_forall_le_iff

Result:
case H
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), c ≤ Multiset.count X (normalizedFactors ↑P) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)

Proof state:
case H
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ ↑(Multiset.count X (normalizedFactors ↑P)) ↔ ↑c ≤ ↑(Multiset.count Polynomial.X (normalizedFactors P))

Tactic:
rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors
  irreducible_X hP, ← emultiplicity_eq_count_normalizedFactors X_irreducible] <;>
simp only [← pow_dvd_iff_le_emultiplicity, Polynomial.X_pow_dvd_iff,
  PowerSeries.X_pow_dvd_iff, Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP,
  not_false_eq_true]

Result:
no goals

Proof state:
case H
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), c ≤ Multiset.count X (normalizedFactors ↑P) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
simp only [← Nat.cast_le (α := ℕ∞)]

Result:
case H
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ ↑(Multiset.count X (normalizedFactors ↑P)) ↔ ↑c ≤ ↑(Multiset.count Polynomial.X (normalizedFactors P))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_neg {x : BitVec w} :
    (-x).toInt = (-x.toInt).bmod (2 ^ w)

Proof state:
w : Nat
x : BitVec w
⊢ (-x).toInt = (-x.toInt).bmod (2 ^ w)

Tactic:
rw [← BitVec.zero_sub, toInt_sub]

Result:
w : Nat
x : BitVec w
⊢ ((0#w).toInt - x.toInt).bmod (2 ^ w) = (-x.toInt).bmod (2 ^ w)

Proof state:
w : Nat
x : BitVec w
⊢ ((0#w).toInt - x.toInt).bmod (2 ^ w) = (-x.toInt).bmod (2 ^ w)

Tactic:
simp [BitVec.toInt_ofNat]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma ae_comp_of_ae_ae (hp : MeasurableSet {z | p z})
    (h : ∀ᵐ y ∂κ a, ∀ᵐ z ∂η y, p z) : ∀ᵐ z ∂(η ∘ₖ κ) a, p z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z
⊢ ∀ᵐ (z : γ) ∂(η ∘ₖ κ) a, p z

Tactic:
rwa [ae_iff, comp_null] at *

Result:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : (κ a) {a | ¬∀ᵐ (z : γ) ∂η a, p z} = 0
⊢ MeasurableSet {a | ¬p a}

Proof state:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : (κ a) {a | ¬∀ᵐ (z : γ) ∂η a, p z} = 0
⊢ MeasurableSet {a | ¬p a}

Tactic:
exact hp.compl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.rel_of_mem_take_of_mem_drop
    {l : List α} (h : l.Pairwise R) (hx : x ∈ l.take n) (hy : y ∈ l.drop n) : R x y

Proof state:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ [x] <+ List.take n l

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ ∃ l₁ l₂, [x, y] = l₁ ++ l₂ ∧ l₁ <+ List.take n l ∧ l₂ <+ List.drop n l

Tactic:
refine ⟨[x], [y], rfl, by simpa, by simpa⟩

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ [y] <+ List.drop n l

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ R x y

Tactic:
apply pairwise_iff_forall_sublist.mp h

Result:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ [x, y] <+ l

Proof state:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ [x, y] <+ l

Tactic:
rw [← take_append_drop n l, sublist_append_iff]

Result:
α : Type u_1
R : α → α → Prop
n : Nat
x y : α
l : List α
h : Pairwise R l
hx : x ∈ List.take n l
hy : y ∈ List.drop n l
⊢ ∃ l₁ l₂, [x, y] = l₁ ++ l₂ ∧ l₁ <+ List.take n l ∧ l₂ <+ List.drop n l