harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_prod' : Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

Proof state:
R : Type u
M M₁ : Type v
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Free R M₁
⊢ Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_inf_himp_inf_le : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Tactic:
simpa using @himp_le_himp_himp_himp

Result:
no goals
-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem CompactSpace.uniformEquicontinuous_of_equicontinuous {ι : Type*} {F : ι → β → α}
    [CompactSpace β] (h : Equicontinuous F) : UniformEquicontinuous F

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]

Result:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Equicontinuous F
⊢ UniformEquicontinuous F

Tactic:
rw [equicontinuous_iff_continuous] at h

Result:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)

Tactic:
exact CompactSpace.uniformContinuous_of_continuous h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq {m : MeasurableSpace α} (μ : Measure α) (f : α →ₛ F) :
    f.integral μ = ∑ x ∈ f.range, (μ (f ⁻¹' {x})).toReal • x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
f : α →ₛ F
⊢ integral μ f = ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal • x

Tactic:
simp [integral, setToSimpleFunc, weightedSMul_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : ℝ) :
    (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign =
      SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
rw [hr₁, zero_smul, zero_mul, zero_add, zero_sub, Left.sign_neg,
  oangle_sign_smul_left, add_comm, oangle_sign_smul_add_smul_right, oangle_rev,
  Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add,
  smul_smul, smul_smul, div_mul_cancel₀ _ hr₁, neg_smul, ← add_assoc, add_comm (-(r₃ • x)), ←
  sub_eq_add_neg, sub_add_cancel, ← add_smul, oangle_sign_smul_right,
  oangle_sign_smul_add_smul_left, ← mul_assoc, ← sign_mul, add_mul, mul_assoc, mul_comm r₂ r₁, ←
  mul_assoc, div_mul_cancel₀ _ hr₁, add_comm, neg_mul, ← sub_eq_add_neg, mul_comm r₄,
  mul_comm r₃]

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 y : V
r₁ r₂ r₃ r₄ : ℝ
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
by_cases hr₁ : r₁ = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem coeff_mul_mirror :
    (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun _ => (· ^ 2)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun x x => x ^ 2

Tactic:
rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 =
    p.sum fun x x => x ^ 2

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    p.coeff n ^ 2

Tactic:
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem setIntegral_condExpL1 (hf : Integrable f μ) (hs : MeasurableSet[m] s) :
    ∫ x in s, condExpL1 hm μ f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hf)) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [setIntegral_condExpL1CLM (hf.toL1 f) hs]

Result:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(Integrable.toL1 f hf) x ∂μ = ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
simp_rw [condExpL1_eq hf]

Result:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hf)) x ∂μ = ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(Integrable.toL1 f hf) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
exact setIntegral_congr_ae (hm s hs) (hf.coeFn_toL1.mono fun x hx _ => hx)

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
theorem nat_mul_inj {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
⊢ n = 0 ∨ a = b

Tactic:
rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_Z : ¬ λ ∣ S.Z :=
  fun h ↦ lambda_not_dvd_z S <| Z_u₃_spec S ▸ dvd_mul_of_dvd_left (dvd_pow h (by decide)) _

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.Z S
⊢ 3 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isNat_zpow_pos {α : Type*} [DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ}
    (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) :
    IsNat (a ^ b) ne

Proof state:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, zpow_natCast]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhdsWithin_eq_image_of_subset {y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' s] f.extend I y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
⊢ s ⊆ (f.extend I).source

Tactic:
rwa [extend_source]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
⊢ map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' s] ↑(f.extend I) y

Tactic:
rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
⊢ s ⊆ (f.extend I).source
-- Mathlib/Logic/Equiv/Basic.lean
theorem prodCongrRight_trans_prodComm :
    (prodCongrRight e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrLeft e)

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)

Tactic:
simp

Result:
no goals

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_left_of_factors_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y)
    (w : P.Factors (f + g)) (wg : P.Factors g) : P.Factors f :=
  (factors_iff _ _).mpr ⟨P.factorThru (f + g) w - P.factorThru g wg, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ (representative.obj P).arrow = f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem volumeForm_robust' (b : OrthonormalBasis (Fin n) ℝ E) (v : Fin n → E) :
    |o.volumeForm v| = |b.toBasis.det v|

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
v : Fin n → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
cases n

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
v : Fin (n✝ + 1) → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
v : Fin (n✝ + 1) → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
  b.abs_det_adjustToOrientation]

Result:
no goals

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem finset_card_const_le_le_of_tsum_le {ι : Type*} {a : ι → ℝ≥0∞} {c : ℝ≥0∞} (c_ne_top : c ≠ ∞)
    (tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) :
    ∃ hf : { i : ι | ε ≤ a i }.Finite, #hf.toFinset ≤ c / ε

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε ≤ c

Tactic:
calc #hf.toFinset * ε = ∑ _i ∈ hf.toFinset, ε := by rw [Finset.sum_const, nsmul_eq_mul]
  _ ≤ ∑ i ∈ hf.toFinset, a i := Finset.sum_le_sum fun i => hf.mem_toFinset.1
  _ ≤ ∑' i, a i := ENNReal.sum_le_tsum _
  _ ≤ c := tsum_le_c

Result:
no goals

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ ∃ (hf : {i | ε ≤ a i}.Finite), ↑(#hf.toFinset) ≤ c / ε

Tactic:
have hf : { i : ι | ε ≤ a i }.Finite :=
  finite_const_le_of_tsum_ne_top (ne_top_of_le_ne_top c_ne_top tsum_le_c) ε_ne_zero

Result:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ∃ (hf : {i | ε ≤ a i}.Finite), ↑(#hf.toFinset) ≤ c / ε

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ∃ (hf : {i | ε ≤ a i}.Finite), ↑(#hf.toFinset) ≤ c / ε

Tactic:
refine ⟨hf, (ENNReal.le_div_iff_mul_le (.inl ε_ne_zero) (.inr c_ne_top)).2 ?_⟩

Result:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε ≤ c

Proof state:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε = ∑ _i ∈ hf.toFinset, ε

Tactic:
rw [Finset.sum_const, nsmul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Iic_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Iic a = Ici (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Iic a = Ici (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_univ {s : Set α} : s ×ˢ (univ : Set β) = Prod.fst ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ univ = Prod.fst ⁻¹' s

Tactic:
simp [prod_eq]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Product.lean
theorem surjective_π_app :
    Function.Surjective (π_app C J)

Proof state:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
⊢ ∃ a, (π_app C J) a = x

Tactic:
obtain ⟨y, hy⟩ := x.prop

Result:
case intro
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = ↑x
⊢ ∃ a, (π_app C J) a = x

Proof state:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
⊢ Function.Surjective ⇑(π_app C J)

Tactic:
intro x

Result:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
⊢ ∃ a, (π_app C J) a = x

Proof state:
case intro
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = ↑x
⊢ ∃ a, (π_app C J) a = x

Tactic:
exact ⟨⟨y, hy.1⟩, Subtype.ext hy.2⟩

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem epi_of_mono_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact)
    (hR₂' : Mono (R₂.map' 0 1)) (h₀ : Epi (app' φ 1)) (h₁ : Mono (app' φ 2)) :
    Epi (app' φ 0) :=
  epi_of_mono_of_epi_of_mono' φ hR₁
    (by simpa only [map'_comp R₂ 0 1 2] using hR₂.toIsComplex.zero 0) hR₂' h₀ h₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)
h₀ : Epi (app' φ 1 ⋯)
h₁ : Mono (app' φ 2 ⋯)
⊢ R₂.map' 0 2 ⋯ ⋯ = 0

Tactic:
simpa only [map'_comp R₂ 0 1 2] using hR₂.toIsComplex.zero 0

Result:
no goals
-- Mathlib/Algebra/Lie/UniversalEnveloping.lean
theorem lift_ι_apply (x : L) : lift R f (ι R x) = f x

Proof state:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ((lift R) f) ((ι R) x) = f x

Tactic:
rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List α} {k fallback : α} :
    m.contains k = false → l.contains k = false → getKeyD (insertManyIfNewUnit m l).1 k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k fallback : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKeyD k fallback = fallback

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem moebius_mul_log_eq_vonMangoldt : (μ : ArithmeticFunction ℝ) * log = Λ

Proof state:
⊢ ↑μ * log = Λ

Tactic:
rw [mul_comm]

Result:
⊢ log * ↑μ = Λ

Proof state:
⊢ log * ↑μ = Λ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma toENNReal_eq_top_iff {x : EReal} : x.toENNReal = ⊤ ↔ x = ⊤

Proof state:
x : EReal
⊢ x.toENNReal = ⊤ ↔ x = ⊤

Tactic:
by_cases h : x = ⊤

Result:
case pos
x : EReal
h : x = ⊤
⊢ x.toENNReal = ⊤ ↔ x = ⊤

case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ⊤ ↔ x = ⊤

Proof state:
case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ⊤ ↔ x = ⊤

Tactic:
simp [h, toENNReal]

Result:
no goals

Proof state:
case pos
x : EReal
h : x = ⊤
⊢ x.toENNReal = ⊤ ↔ x = ⊤

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma liftCochain_v_fst_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) :
    (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (fst φ).1.v p₂ p₃ h₂₃ = α.v p₁ p₃ (by omega)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (↑(fst φ)).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯

Tactic:
simpa only [Cochain.comp_v _ _ h p₁ p₂ p₃ h₁₂ h₂₃]
  using Cochain.congr_v (liftCochain_fst φ α β h) p₁ p₃ (by omega)

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.186108, u_1} C
inst✝³ : Category.{?u.186112, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ p₁ + m = p₃

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ p₁ + m = p₃

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_of_prod {l : Vector α n} {l' : Vector β n} {lp : Vector (α × β) n} (hl : lp.map Prod.fst = l)
    (hr : lp.map Prod.snd = l') : lp = l.zip l'

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
l' : Vector β n
lp : Vector (α × β) n
hl : map Prod.fst lp = l
hr : map Prod.snd lp = l'
⊢ lp = l.zip l'

Tactic:
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_T_pow (n : ℤ) (x : Sˣ) : (T n : R[T;T⁻¹]).smeval x = (x ^ n).val

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
n : ℤ
x : Sˣ
⊢ (T n).smeval x = ↑(x ^ n)

Tactic:
rw [T, smeval_single, one_smul]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_closedBall' : y ∈ closedBall x ε ↔ edist x y ≤ ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedBall x ε ↔ edist x y ≤ ε

Tactic:
rw [edist_comm, mem_closedBall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem keys_map [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → γ a} :
    keys (l.map fun p => ⟨p.1, f p.1 p.2⟩) = keys l

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝ : BEq α
l : List ((a : α) × β a)
f : (a : α) → β a → γ a
⊢ keys (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = keys l

Tactic:
induction l using assoc_induction <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem proj_comp_single (i j : ι) : (proj i).comp (single R φ j) = diag j i

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i j : ι
⊢ proj i ∘ₗ single R φ j = diag j i

Tactic:
rw [single_eq_pi_diag, proj_pi]

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma odd_of_val {n : ℕ} [NeZero n] {k : Fin n} (h : Odd k.val) : Odd k

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : Odd ↑k
⊢ Odd ↑↑k

Tactic:
exact h.natCast

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : Odd ↑k
⊢ Odd k

Tactic:
rw [← Fin.cast_val_eq_self k]

Result:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : Odd ↑k
⊢ Odd ↑↑k