harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_hasFDerivAt_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] F
⊢ HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm).comp f') x

Tactic:
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_ge_length_sub_length' (w₁ w₂ : W) :
    ℓ w₂ - ℓ w₁ ≤ ℓ (w₁ * w₂)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

Tactic:
simpa [Nat.sub_le_of_le_add, add_comm] using cs.length_mul_le w₁⁻¹ (w₁ * w₂)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma id_tensorHom (X : LocalizedMonoidal L W ε) {Y₁ Y₂ : LocalizedMonoidal L W ε} (f : Y₁ ⟶ Y₂) :
    𝟙 X ⊗ f = X ◁ f

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y₁ Y₂ : LocalizedMonoidal L W ε
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ f = X ◁ f

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv_const_sub (c : F) : deriv (fun y => c - f y) x = -deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun y => c - f y) x = -deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_const_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
    (as.setIfInBounds i a)[j]? = as[j]?

Proof state:
α : Type u_1
as : Array α
i j : Nat
h : i ≠ j
a : α
⊢ (as.setIfInBounds i a)[j]? = as[j]?

Tactic:
simp [getElem?_setIfInBounds, h]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
theorem inclusion_exclusion_sum_inf_compl (s : Finset ι) (S : ι → Finset α) (f : α → G) :
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : DecidableEq α
inst✝¹ : AddCommGroup G
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a : α, f a - ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ filter (fun x => ¬x.Nonempty) s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a +
      ∑ t ∈ filter (fun x => x.Nonempty) s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Tactic:
simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
  sub_eq_add_neg, pow_succ]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : DecidableEq α
inst✝¹ : AddCommGroup G
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun i => (S i)ᶜ, f a = ∑ a : α, f a - ∑ a ∈ s.biUnion S, f a

Tactic:
rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem le_infEdist {d} : d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
d : ℝ≥0∞
⊢ d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y

Tactic:
simp only [infEdist, le_iInf_iff]

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toFinsupp_sum_eq (s : Multiset α) : s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ((toFinsupp s).sum fun x => id) = s.card

Tactic:
rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive] lemma mulEnergy_eq_card_filter (s t : Finset α) :
    Eₘ[s, t] = (((s ×ˢ t) ×ˢ s ×ˢ t).filter fun ((a, b), c, d) ↦ a * b = c * d).card :=
  card_equiv (.prodProdProdComm _ _ _ _) (by simp [and_and_and_comm])

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ (i : (α × α) × α × α),
    i ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t) ↔
      (Equiv.prodProdProdComm α α α α) i ∈
        filter
          (fun x =>
            match x with
            | ((a, b), c, d) => a * b = c * d)
          ((s ×ˢ t) ×ˢ s ×ˢ t)

Tactic:
simp [and_and_and_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_leftUnitor_hom_fst (X : C₁ × C₂) :
    ((λ_ X).hom : 𝟙_ _ ⊗ X ⟶ X).1 = (λ_ X.1).hom

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).hom.1 = (λ_ X.1).hom

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.1 = (λ_ (fst✝, snd✝).1).hom

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.1 = (λ_ (fst✝, snd✝).1).hom

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma algebraMap_le_cfc_iff (f : R → R) (r : R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.814627) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
r : R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ cfc f a ↔ ∀ x ∈ spectrum R a, r ≤ f x

Tactic:
rw [← cfc_const r a, cfc_le_iff ..]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isCompact_basicOpen (f : R) : IsCompact (basicOpen f : Set (PrimeSpectrum R))

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact ↑(basicOpen f)

Tactic:
rw [← localization_away_comap_range (Localization (Submonoid.powers f))]

Result:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact (Set.range ⇑(comap (algebraMap R (Localization (Submonoid.powers f)))))

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact (Set.range ⇑(comap (algebraMap R (Localization (Submonoid.powers f)))))

Tactic:
exact isCompact_range (map_continuous _)

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_span_le_card (s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card :=
  finrank_le_of_rank_le (by simpa using rank_span_le (R := R) s)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
s : Set M
inst✝ : Fintype ↑s
⊢ Module.rank R ↥(span R s) ≤ ↑s.toFinset.card

Tactic:
simpa using rank_span_le (R := R) s

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma eq_zero_of_dvd_of_div_eq_zero (hab : a ∣ b) (h : b / a = 0) : b = 0

Proof state:
a b : ℕ
hab : a ∣ b
h : b / a = 0
⊢ b = 0

Tactic:
rw [← Nat.div_mul_cancel hab, h, Nat.zero_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem inv_smul_mem_iff : a⁻¹ • b ∈ s ↔ b ∈ a • s

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_sub_Ico_right (a b c : α) : Ico a b - Ico c b = Ico a (min b c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico c b = Ico a (b ⊓ c)

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b

Proof state:
α : Type u
a b : α
l : List α
⊢ (b :: l).getLastD a = l.getLastD b

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ici_subset_Ioi_pred (a : α) : Ici a ⊆ Ioi (pred a)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ici a ⊆ Ioi (pred a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.isLocallyConstant_of_fderiv_eq_zero (h₁ : Differentiable 𝕜 f)
    (h₂ : ∀ x, fderiv 𝕜 f x = 0) : IsLocallyConstant f

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
h₁ : Differentiable 𝕜 f
h₂ : ∀ (x : E), fderiv 𝕜 f x = 0
⊢ IsLocallyConstant f

Tactic:
simpa using isOpen_univ.isOpen_inter_preimage_of_fderiv_eq_zero h₁.differentiableOn fun _ _ ↦ h₂ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_map_iff : map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
g : α✝¹ → α✝
⊢ map f l = map g l ↔ ∀ (a : α✝¹), a ∈ l → f a = g a

Tactic:
induction l <;> simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean
theorem UpperHalfPlane.norm_exp_two_pi_I_lt_one (τ : ℍ) :
    ‖(Complex.exp (2 * π * Complex.I * τ))‖ < 1

Proof state:
τ : ℍ
⊢ ‖cexp (2 * ↑π * Complex.I * ↑τ)‖ < 1

Tactic:
simpa [Function.Periodic.norm_qParam, Complex.norm_exp] using τ.norm_qParam_lt_one 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩

Proof state:
α✝ : Type u_1
l : List α✝
n : Nat
e : l.get? n = none
h' : n < l.length
⊢ False

Tactic:
cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem isEmpty : ∀ {s}, ValidFor l m r s → (s.isEmpty ↔ m = [])
  | _, h => by simp [Substring.isEmpty, h.bsize]

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ x✝.isEmpty = true ↔ m = []

Tactic:
simp [Substring.isEmpty, h.bsize]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanFinset_eq_zero {ι : Type*} {s : Finset ι} {f : ι → K} :
    spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

Tactic:
simp only [← coeToSubmodule_inj, spanFinset_coe, coe_zero, Submodule.span_eq_bot,
  Set.mem_image, Finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_interval_sub_interval_comm' (hab : IntervalIntegrable f μ a b)
    (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
    ((∫ x in a..b, f x ∂μ) - ∫ x in c..d, f x ∂μ) =
      (∫ x in d..b, f x ∂μ) - ∫ x in c..a, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in d..b, f x ∂μ - ∫ (x : ℝ) in c..a, f x ∂μ

Tactic:
rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
  sub_neg_eq_add, sub_eq_neg_add]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Regulator.lean
theorem regulator_eq_det' (e : {w : InfinitePlace K // w ≠ w₀} ≃ Fin (rank K)) :
    regulator K = |(Matrix.of fun i ↦
      logEmbedding K (Additive.ofMul (fundSystem K (e i)))).det|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
e : { w // w ≠ w₀ } ≃ Fin (rank K)
⊢ regulator K = |(Matrix.of fun i => (logEmbedding K) (Additive.ofMul (fundSystem K (e i)))).det|

Tactic:
simp_rw [regulator, ZLattice.covolume_eq_det _
  (((basisModTorsion K).map (logEmbeddingEquiv K)).reindex e.symm), Basis.coe_reindex,
  Function.comp_def, Basis.map_apply, ← fundSystem_mk, Equiv.symm_symm, logEmbeddingEquiv_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
e : { w // w ≠ w₀ } ≃ Fin (rank K)
⊢ ZLattice.covolume (unitLattice K) volume =
    |(Matrix.of fun i => (logEmbedding K) (Additive.ofMul (fundSystem K (e i)))).det|
-- Mathlib/Algebra/AlgebraicCard.lean
theorem cardinalMk_lift_le_max :
    Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } ≤ max (Cardinal.lift.{v} #R) ℵ₀ :=
  (cardinalMk_lift_le_mul R A).trans <|
    (mul_le_mul_right' (lift_le.2 cardinalMk_le_max) _).trans <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift.{v, u} (#R ⊔ ℵ₀) * ℵ₀ ≤ lift.{v, u} #R ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem?_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < i) :
    (l.eraseIdx i)[j]? = l[j]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < i
⊢ (l.eraseIdx i)[j]? = l[j]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
l : List α
i j : Nat
h : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem closure_thickening (hδ : 0 < δ) (s : Set E) :
    closure (thickening δ s) = cthickening δ s

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
⊢ closure (thickening δ s) = cthickening δ s

Tactic:
rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
lemma lift_openEmbedding_trans_apply
    (e e' : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) (z : Z) :
    (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) z = (e.symm.trans e') z

Proof state:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : PartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ ↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) z = ↑(e.symm.trans e') z

Tactic:
simp [hf.injective.extend_apply e']

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : Finset γ) :
    image₂ f s {b} = s

Proof state:
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image₂ f s {b} = s

Tactic:
rw [image₂_singleton_right, funext h, image_id']

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd [NormedSpace ℝ E]
    ⦃f : β × γ → E⦄ (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
    AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂η (a, x)) (κ a) :=
  ⟨fun x => ∫ y, hf.mk f (x, y) ∂η (a, x), hf.stronglyMeasurable_mk.integral_kernel_prod_right'', by
    filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) =ᶠ[ae (κ a)] fun x =>
    ∫ (y : γ), AEStronglyMeasurable.mk f hf (x, y) ∂η (a, x)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_reindex_symm {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
    (v : ι → M) (e : ι' ≃ ι) : (b.reindex e.symm).det (v ∘ e) = b.det v

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
⊢ (b.reindex e.symm).det (v ∘ ⇑e) = b.det v

Tactic:
rw [Basis.det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem matPolyEquiv_eval_eq_map (M : Matrix n n R[X]) (r : R) :
    (matPolyEquiv M).eval (scalar n r) = M.map (eval r)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ eval ((scalar n) r) (matPolyEquiv M) = M.map (eval r)

Tactic:
simpa only [AlgEquiv.symm_apply_apply] using (matPolyEquiv_symm_map_eval (matPolyEquiv M) r).symm

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasStrictFDerivAt_id (x : E) : HasStrictFDerivAt id (id 𝕜 E) x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left <| by simp

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ∀ (x : E × E), 0 x = _root_.id x.1 - _root_.id x.2 - (ContinuousLinearMap.id 𝕜 E) (x.1 - x.2)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Prod.lean
theorem prod_unique (f : R →+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Proof state:
R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f : R →+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem ble_eq_false {x y : ℕ} : x.ble y = false ↔ y < x

Proof state:
x y : ℕ
⊢ x.ble y = false ↔ y < x

Tactic:
rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_arithShiftRightConst : eval (arithShiftRightConst n) = (BitVec.sshiftRight · n : BitVec w → BitVec w)

Proof state:
n w : Nat
⊢ (arithShiftRightConst n).eval = fun x => x.sshiftRight n

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/QuotientGroup.lean
@[simp]
lemma index_zmultiples (a : ℤ) : (AddSubgroup.zmultiples a).index = a.natAbs

Proof state:
a : ℤ
⊢ (AddSubgroup.zmultiples a).index = a.natAbs

Tactic:
rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem volume_apply {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Box ι) (x : E) :
    BoxAdditiveMap.volume I x = (∏ j, (I.upper j - I.lower j)) • x

Proof state:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ (BoxAdditiveMap.volume I) x = (∏ j : ι, (I.upper j - I.lower j)) • x

Tactic:
rw [BoxAdditiveMap.volume, toSMul_apply]

Result:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ volume.toBoxAdditive I • x = (∏ j : ι, (I.upper j - I.lower j)) • x
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_eq_zero_iff_of_nonpos [Nonempty ι] (hf : f ≤ 0) : 𝔼 i, f i = 0 ↔ f = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
f : ι → α
inst✝ : Nonempty ι
hf : f ≤ 0
⊢ 𝔼 i : ι, f i = 0 ↔ f = 0

Tactic:
simp [expect, sum_eq_zero_iff_of_nonpos hf, univ_nonempty.ne_empty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem degree_normalize [DecidableEq R] : degree (normalize p) = degree p

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
⊢ (normalize p).degree = p.degree

Tactic:
simp [normalize_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
lemma denom_one : denom 1 z = 1

Proof state:
z : ℍ
⊢ denom 1 z = 1

Tactic:
simp [denom]

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) :
    (F.map (f ≫ g)) a = (F.map g) ((F.map f) a)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a : F.obj X
⊢ F.map (f ≫ g) a = F.map g (F.map f a)

Tactic:
simp [types_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.linearIndepOn_id (i : LinearIndependent R v) :
    LinearIndepOn R id (range v)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : LinearIndependent R v
⊢ LinearIndepOn R id (range v)

Tactic:
simpa using i.comp _ (rangeSplitting_injective v)

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem fin_mono {n} : Monotone (Finset.fin n) := fun s t h x => by simpa using @h x

Proof state:
n : ℕ
s t : Finset ℕ
h : s ≤ t
x : Fin n
⊢ x ∈ Finset.fin n s → x ∈ Finset.fin n t

Tactic:
simpa using @h x

Result:
no goals
-- Mathlib/GroupTheory/CosetCover.lean
theorem leftCoset_cover_const_iff_surjOn :
    ⋃ i ∈ s, g i • (H : Set G) = Set.univ ↔ Set.SurjOn (g · : ι → G ⧸ H) s Set.univ

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
⊢ ⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ

Tactic:
simp [Set.eq_univ_iff_forall, mem_leftCoset_iff, Set.SurjOn,
  QuotientGroup.forall_mk, QuotientGroup.eq]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem to_ofOption (o : Option α) : toOption (ofOption o) = o

Proof state:
α : Type u_1
o : Option α
⊢ (↑o).toOption = o

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Affine.CoordinateRing.mk_ψ (n : ℤ) : mk W (W.ψ n) = mk W (W.Ψ n)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.ψ n) = (mk W) (W.Ψ n)

Tactic:
simp only [ψ, normEDS, Ψ, preΨ, map_mul, map_pow, map_preNormEDS, ← mk_ψ₂_sq, ← pow_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem mem_range_aleph_iff {c : Cardinal} : c ∈ range aleph ↔ ℵ₀ ≤ c

Proof state:
c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ ℵ₀ ≤ c

Tactic:
rw [range_aleph, mem_Ici]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_top : 𝓝 (⊤ : Filter α) = ⊤

Proof state:
α : Type u_2
⊢ 𝓝 ⊤ = ⊤

Tactic:
simp [nhds_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean
theorem leftZigzagIso_inv : (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

Result:
no goals