harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_self_ofReal_re (x : F) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ ↑(re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜

Tactic:
norm_num [ext_iff, inner_self_im]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_tensorProduct :
    finrank R (M ⊗[S] M') = finrank R M * finrank S M'

Proof state:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
⊢ finrank R (M ⊗[S] M') = finrank R M * finrank S M'

Tactic:
simp [finrank]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
lemma biprod.decomp_hom_to (f : Z ⟶ X ⊞ Y) :
    ∃ f₁ f₂, f = f₁ ≫ biprod.inl + f₂ ≫ biprod.inr :=
  ⟨f ≫ biprod.fst, f ≫ biprod.snd, by aesop⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
Z : C
f : Z ⟶ X ⊞ Y
⊢ f = (f ≫ fst) ≫ inl + (f ≫ snd) ≫ inr

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).getKey k (contains_insert_self _ h) = k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).getKey k ⋯ = k

Tactic:
simp_to_model [insert] using List.getKey_insertEntry_self

Result:
no goals
-- Mathlib/Tactic/Rify.lean
@[rify_simps] lemma ratCast_ne (a b : ℚ) : a ≠ b ↔ (a : ℝ) ≠ (b : ℝ)

Proof state:
a b : ℚ
⊢ a ≠ b ↔ ↑a ≠ ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_isNone_iff {f : Fin n → Option α} :
    (findSome? f).isNone ↔ ∀ i, (f i).isNone

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem nndist_div_left [Group G] [PseudoMetricSpace G] [IsometricSMul G G]
    [IsometricSMul Gᵐᵒᵖ G] (a b c : G) : nndist (a / b) (a / c) = nndist b c

Proof state:
G : Type v
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ nndist (a / b) (a / c) = nndist b c

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.single_apply (i : ι) (a : 𝕜) (j : ι) :
    (EuclideanSpace.single i a) j = ite (j = i) a 0

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq ι
i : ι
a : 𝕜
j : ι
⊢ single i a j = if j = i then a else 0

Tactic:
rw [EuclideanSpace.single, WithLp.equiv_symm_pi_apply, ← Pi.single_apply i a j]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem frontier_inter_open_inter {s t : Set X} (ht : IsOpen t) :
    frontier (s ∩ t) ∩ t = frontier s ∩ t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
ht : IsOpen t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t

Tactic:
simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff,
  ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
  Subtype.preimage_coe_self_inter]

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem zero_sub_eq_eval [AddCommGroup M] [Ring R] [Module R M] (l : NF R M) :
    0 - l.eval = (-l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ 0 - l.eval = (-l).eval

Tactic:
simp [eval_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem analyticSet_empty : AnalyticSet (∅ : Set α)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ AnalyticSet ∅

Tactic:
rw [AnalyticSet]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∅ = ∅ ∨ ∃ f, Continuous f ∧ range f = ∅

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∅ = ∅ ∨ ∃ f, Continuous f ∧ range f = ∅

Tactic:
exact Or.inl rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_ite_mem [DecidableEq α] (s t : Finset α) (f : α → β) :
    ∏ i ∈ s, (if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
⊢ (∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i

Tactic:
rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_reverse (L : List (List α)) :
    L.reverse.flatten = (L.map reverse).flatten.reverse

Proof state:
α : Type u_1
L : List (List α)
⊢ L.reverse.flatten = (map reverse L).flatten.reverse

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_nsmul_add (x : AddCircle T) {n : ℕ} (h : 1 < n) : Ergodic fun y => n • y + x :=
  ergodic_zsmul_add x (by simp [h] : 1 < |(n : ℤ)|)

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℕ
h : 1 < n
⊢ 1 < |↑n|

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
  ofReal_inj.1 <| by simp [tanh_eq_sinh_div_cosh]

Proof state:
x : ℝ
⊢ ↑(tanh x) = ↑(sinh x / cosh x)

Tactic:
simp [tanh_eq_sinh_div_cosh]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
lemma LSeries.convolution_congr {R : Type*} [Semiring R] {f f' g g' : ℕ → R}
    (hf : ∀ {n}, n ≠ 0 → f n = f' n) (hg : ∀ {n}, n ≠ 0 → g n = g' n) :
    f ⍟ g = f' ⍟ g'

Proof state:
R : Type u_1
inst✝ : Semiring R
f f' g g' : ℕ → R
hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n
⊢ f ⍟ g = f' ⍟ g'

Tactic:
simp [convolution, toArithmeticFunction_congr hf, toArithmeticFunction_congr hg]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
private lemma piScalarRightInv_single (x : N) (i : ι) :
    piScalarRightInv R S N ι (Pi.single i x) = x ⊗ₜ Pi.single i 1

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ (TensorProduct.piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

Tactic:
simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem toMatrix_lmul' (x : S) (i j) :
    LinearMap.toMatrix b b (lmul R S x) i j = b.repr (x * b j) i

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ (toMatrix b b) ((lmul R S) x) i j = (b.repr (x * b j)) i

Tactic:
simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']

Result:
no goals
-- Mathlib/RingTheory/Regular/IsSMulRegular.lean
lemma smul_top_inf_eq_smul_of_isSMulRegular_on_quot :
    IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N

Tactic:
convert map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2

Result:
case h'.h.e'_3
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
a✝ : IsSMulRegular (M ⧸ N) r
⊢ r • ⊤ ⊓ N = map (DistribMulAction.toLinearMap R M r) (comap ((LinearMap.lsmul R M) r) N)
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem coe_floor_self (k : K) : (floor (Basis.singleton ι K) k : K) = ⌊k⌋ :=
  Basis.ext_elem (Basis.singleton ι K) fun _ => by
    rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

Proof state:
ι : Type u_2
K : Type u_3
inst✝³ : NormedLinearOrderedField K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr ↑(floor (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr ↑⌊k⌋) x✝

Tactic:
rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

Result:
no goals
-- Mathlib/Data/Complex/BigOperators.lean
@[simp]
lemma re_balance [Fintype α] (f : α → ℂ) (a : α) : re (balance f a) = balance (re ∘ f) a

Proof state:
α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).re = balance (re ∘ f) a

Tactic:
simp [balance]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_mul_mul_comm (a b c d : G) : a * b * (c * d) = a * c * (b * d)

Proof state:
G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
simp only [mul_left_comm, mul_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
theorem transfer_center_eq_pow [FiniteIndex (center G)] (g : G) :
    transfer (MonoidHom.id (center G)) g = ⟨g ^ (center G).index, (center G).pow_index_mem g⟩ :=
  transfer_eq_pow (id (center G)) g fun k _ hk => by rw [← mul_right_inj, ← hk.comm,
    mul_inv_cancel_right]

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : (center G).FiniteIndex
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ x✝⁻¹ * g ^ k * x✝ = g ^ k

Tactic:
rw [← mul_right_inj, ← hk.comm,
mul_inv_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean
@[reassoc]
lemma equalizer.condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
⊢ ι f g ≫ f = ι f g ≫ g

Tactic:
simp [← range_le_equalizer_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Group/LIntegral.lean
theorem lintegral_eq_zero_of_isMulLeftInvariant [Regular μ] [NeZero μ] {f : G → ℝ≥0∞}
    (hf : Continuous f) : ∫⁻ x, f x ∂μ = 0 ↔ f = 0

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : BorelSpace G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

Tactic:
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε

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

Tactic:
rw [mem_ball', mem_ball]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@[simp]
lemma span_eq_toSubmodule (s : NonUnitalSubalgebra R A) :
    Submodule.span R (s : Set A) = s.toSubmodule

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
s : NonUnitalSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

Result:
no goals
-- Mathlib/Algebra/CharZero/Defs.lean
theorem cast_eq_zero {n : ℕ} : (n : R) = 0 ↔ n = 0

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0

Tactic:
rw [← cast_zero, cast_inj]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix. -/
lemma fromBlocks_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R)
    (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * (fromRows A₁ A₂) =
      fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Tactic:
ext (_ | _) _ <;> simp [mul_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLT_swap {o : Ordering} : o.swap.isLT = o.isGT

Proof state:
o : Ordering
⊢ o.swap.isLT = o.isGT

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem separableSpace_iff_countable [DiscreteTopology α] : SeparableSpace α ↔ Countable α

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ SeparableSpace α ↔ Countable α

Tactic:
simp [separableSpace_iff, countable_univ_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.const_inv_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul a⁻¹

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem degLex_single_lt_iff {a b : σ} :
    single a 1 ≺[degLex] single b 1 ↔ b < a

Proof state:
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ degLex.toSyn (single a 1) < degLex.toSyn (single b 1) ↔ b < a

Tactic:
rw [MonomialOrder.degLex_lt_iff, DegLex.single_lt_iff]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma imp_top (φ : L.BoundedFormula α n) : φ ⟹[T] ⊤ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_top, implies_true]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ ⊤).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_top, implies_true]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
lemma extChartAt_inl_apply {x y : M} :
    (extChartAt I (.inl x : M ⊕ M')) (Sum.inl y) = (extChartAt I x) y

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_16
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x y : M
⊢ ↑(extChartAt I (Sum.inl x)) (Sum.inl y) = ↑(extChartAt I x) y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem levenshtein_nil_nil : levenshtein C [] [] = 0

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ levenshtein C [] [] = 0

Tactic:
simp [levenshtein, suffixLevenshtein]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem AEMeasurable.mul_iff_right {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
    [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure α} {f g : α → G} (hf : AEMeasurable f μ) :
    AEMeasurable (f * g) μ ↔ AEMeasurable g μ :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
    fun h ↦ hf.mul h⟩

Proof state:
α : Type u_1
G : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSpace α
inst✝² : CommGroup G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
μ : Measure α
f g : α → G
hf : AEMeasurable f μ
h : AEMeasurable (f * g) μ
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hasSum_int_cosKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℤ ↦ if n = 0 then 0 else cexp (2 * π * I * a * n) * rexp (-π * n ^ 2 * t))
    (↑(cosKernel a t) - 1)

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)

Tactic:
simpa using hasSum_ite_sub_hasSum (hasSum_int_cosKernel a ht) 0

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos (h : 0 < d) :
    (invOneSubPow S d).val = (mk fun n => Nat.choose (d - 1 + n) (d - 1) : S⟦X⟧)

Proof state:
S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑(invOneSubPow S d) = mk fun n => ↑((d - 1 + n).choose (d - 1))

Tactic:
rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Topology/Sets/OpenCover.lean
/-- Pullback of a covering of `Y` by a continuous map `X → Y`, giving a covering of `X` with the
same index type. -/
lemma comap (hv : IsOpenCover v) (f : C(X, Y)) : IsOpenCover fun k ↦ (v k).comap f :=
  by simp [IsOpenCover, ← preimage_iUnion, hv.iSup_set_eq_univ]

Proof state:
κ : Type u_2
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
v : κ → Opens Y
hv : IsOpenCover v
f : C(X, Y)
⊢ IsOpenCover fun k => (Opens.comap f) (v k)

Tactic:
simp [IsOpenCover, ← preimage_iUnion, hv.iSup_set_eq_univ]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_nontrivial [Fintype s] : s.toFinset.Nontrivial ↔ s.Nontrivial

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, coe_toFinset]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_pos_iff_support_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) :
    (0 < ∫ x, f x ∂μ) ↔ 0 < μ (Function.support f)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ 0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)

Tactic:
simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
  integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
  Function.support]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioo_add_intCast :
    Pairwise (Disjoint on fun n : ℤ => Ioo (a + n) (a + n + 1))

Proof state:
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (a + ↑n) (a + ↑n + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  pairwise_disjoint_Ioo_add_zsmul a (1 : α)

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_sub : u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_symm_naturality {X X' Y Y' Z : C} [ExactPairing Y Y'] (f : X ⟶ X')
    (g : X' ⟶ Z ⊗ Y') :
    (tensorRightHomEquiv X Y Y' Z).symm (f ≫ g) =
      f ▷ Y ≫ (tensorRightHomEquiv X' Y Y' Z).symm g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Z ⊗ Y'
⊢ (tensorRightHomEquiv X Y Y' Z).symm (f ≫ g) = f ▷ Y ≫ (tensorRightHomEquiv X' Y Y' Z).symm g

Tactic:
simp [tensorRightHomEquiv]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_fintype [MeasurableSingletonClass α] [Fintype α] (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂μ = ∑ x, f x * μ {x}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x : α, f x * μ {x}

Tactic:
rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma map_loopyOn (f : α → β) (hf) : (loopyOn E).map f hf = loopyOn (f '' E)

Proof state:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (loopyOn E).E
⊢ (loopyOn E).map f hf = loopyOn (f '' E)

Tactic:
simp [eq_loopyOn_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem Monic.eq_X_add_C (hm : p.Monic) (hnd : p.natDegree = 1) : p = X + C (p.coeff 0)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = X + C (p.coeff 0)

Tactic:
rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem out' : ∀ {it}, ValidFor l r it → it = ⟨⟨l.reverse ++ r⟩, ⟨utf8Len l.reverse⟩⟩
  | _, ⟨⟩ => by simp [List.reverseAux_eq]

Proof state:
l r : List Char
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } } =
    { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }

Tactic:
simp [List.reverseAux_eq]

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

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ m.contains a = false → m.getKeyD a fallback = fallback

Tactic:
simp_to_model using List.getKeyD_eq_fallback

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S R R]
    (s : S) (a : ℍ[R,c₁,c₂,c₃]) :
    star (s • a) = s • star a :=
  QuaternionAlgebra.ext
    (by simp [mul_smul_comm]) (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm

Proof state:
S : Type u_1
R : Type u_3
c₁ c₂ c₃ : R
inst✝³ : CommRing R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : SMulCommClass S R R
s : S
a : ℍ[R,c₁,c₂,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
simp [mul_smul_comm]

Result:
no goals
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- Suprema of delta-generated topologies are delta-generated. -/
protected lemma DeltaGeneratedSpace.sup {X : Type*} {t₁ t₂ : TopologicalSpace X}
    (h₁ : @DeltaGeneratedSpace X t₁) (h₂ : @DeltaGeneratedSpace X t₂) :
    @DeltaGeneratedSpace X (t₁ ⊔ t₂)

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : DeltaGeneratedSpace X
h₂ : DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X

Tactic:
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_neg_of_neg_of_pos [SMulPosStrictMono α β] (ha : a < 0) (hb : 0 < b) : a • b < 0

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : a < 0
hb : 0 < b
⊢ a • b < 0

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_option_toFinset (o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Proof state:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
o : Option α
f : α → β
⊢ ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} {k : α} :
    k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k = true

Tactic:
simp [mem_iff_contains, contains_insertManyIfNewUnit_list h]

Result:
no goals