harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Log.lean
theorem pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ log b y) : b ^ x ≤ y

Proof state:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y

Tactic:
rw [log_of_left_le_one hb, Nat.le_zero] at h

Result:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y

Proof state:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y

Tactic:
rwa [h, Nat.pow_zero, one_le_iff_ne_zero]

Result:
no goals

Proof state:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y

Tactic:
refine (le_or_lt b 1).elim (fun hb => ?_) fun hb => (pow_le_iff_le_log hb hy).2 h

Result:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y
-- Mathlib/Data/Set/Insert.lean
theorem diff_singleton_eq_self {a : α} {s : Set α} (h : a ∉ s) : s \ {a} = s :=
  sdiff_eq_self_iff_disjoint.2 <| by simp [h]

Proof state:
α : Type u
a : α
s : Set α
h : a ∉ s
⊢ Disjoint {a} s

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem orderTop_eq_of_le {x : HahnSeries Γ R} {g : Γ} (hg : g ∈ x.support)
    (hx : ∀ g' ∈ x.support, g ≤ g') : orderTop x = g

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
⊢ x.orderTop = ↑g

Tactic:
rw [orderTop_of_ne <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
  x.isWF_support.min_eq_of_le hg hx]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma isSymm_posForm :
    B.posForm.IsSymm

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ LinearMap.IsSymm B.posForm

Tactic:
intro x y

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (RingHom.id S) ((B.posForm x) y) = (B.posForm y) x

Proof state:
case a
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) ((RingHom.id S) ((B.posForm x) y)) = (algebraMap S R) ((B.posForm y) x)

Tactic:
simpa using B.symm.eq x y

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (RingHom.id S) ((B.posForm x) y) = (B.posForm y) x

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Result:
case a
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) ((RingHom.id S) ((B.posForm x) y)) = (algebraMap S R) ((B.posForm y) x)
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma compls_univ [Fintype α] : (univ : Finset α)ᶜˢ = univ

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
⊢ univᶜˢ = univ

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univᶜˢ ↔ a✝ ∈ univ

Proof state:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univᶜˢ ↔ a✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem dist_center_inversion (c x : P) (R : ℝ) : dist c (inversion c R x) = R ^ 2 / dist c x

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ dist c (inversion c R x) = R ^ 2 / dist c x

Tactic:
rw [dist_comm c, dist_comm c, dist_inversion_center]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (map₂ f a b).map g = map₂ f' b (a.map g')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)

Tactic:
cases a <;> cases b <;> simp [h_antidistrib]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.neg {f : α → β} (hfi : HasFiniteIntegral f μ) :
    HasFiniteIntegral (-f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} :
    (m.insertMany l).size ≤ m.size + l.length

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
⊢ (m.insertMany l).size ≤ m.size + l.length

Tactic:
simp_to_raw using Raw₀.size_insertMany_list_le

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem le_floor {z : ℤ} : ∀ {r : ℚ}, z ≤ Rat.floor r ↔ (z : ℚ) ≤ r
  | ⟨n, d, h, c⟩ => by
    simp only [Rat.floor_def']
    rw [mk'_eq_divInt]
    have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
    conv =>
      rhs
      rw [intCast_eq_divInt, Rat.divInt_le_divInt zero_lt_one h', mul_one]
    exact Int.le_ediv_iff_mul_le h'

Proof state:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d

Tactic:
have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)

Result:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d

Proof state:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
⊢ z ≤ { num := n, den := d, den_nz := h, reduced := c }.floor ↔ ↑z ≤ { num := n, den := d, den_nz := h, reduced := c }

Tactic:
simp only [Rat.floor_def']

Result:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
⊢ z ≤ n / ↑d ↔ ↑z ≤ { num := n, den := d, den_nz := h, reduced := c }

Proof state:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
⊢ z ≤ n / ↑d ↔ ↑z ≤ { num := n, den := d, den_nz := h, reduced := c }

Tactic:
rw [mk'_eq_divInt]

Result:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d

Proof state:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d

Tactic:
conv =>
  rhs
  rw [intCast_eq_divInt, Rat.divInt_le_divInt zero_lt_one h', mul_one]

Result:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ z * ↑d ≤ n

Proof state:
z n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ z * ↑d ≤ n

Tactic:
exact Int.le_ediv_iff_mul_le h'

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldl_eq_foldl_toList {t : RBNode.Stream α} : t.foldl f init = t.toList.foldl f init

Proof state:
α : Type u_1
α✝ : Type u_2
f : α✝ → α → α✝
init : α✝
t : RBNode.Stream α
⊢ foldl f init t = List.foldl f init t.toList

Tactic:
induction t generalizing init <;> simp [*, RBNode.foldl_eq_foldl_toList]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToFun_le_mul_norm (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E)
    (hC : 0 ≤ C) : ‖setToFun μ T hT f‖ ≤ C * ‖f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
⊢ ‖(L1.setToL1 hT) f‖ ≤ C * ‖f‖

Tactic:
exact L1.norm_setToL1_le_mul_norm hT hC f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
⊢ ‖setToFun μ T hT ↑↑f‖ ≤ C * ‖f‖

Tactic:
rw [L1.setToFun_eq_setToL1]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
hC : 0 ≤ C
⊢ ‖(L1.setToL1 hT) f‖ ≤ C * ‖f‖
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma nnnorm_quasispectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σₙ 𝕜 a) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : autoParam (p a) _auto✝
⊢ ‖x‖₊ ≤ ‖a‖₊

Tactic:
simpa only [cfcₙ_id 𝕜 a] using nnnorm_apply_le_nnnorm_cfcₙ (id : 𝕜 → 𝕜) a hx

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem isRkFinite_iff_cRk_lt_aleph0 : M.IsRkFinite X ↔ M.cRk X < ℵ₀

Proof state:
α : Type u
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀

Tactic:
rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem orElse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
  destruct_eq_think <| by
    unfold_projs
    simp [orElse]

Proof state:
α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think.orElse fun x => c₂.think).destruct = Sum.inr (c₁.orElse fun x => c₂)

Tactic:
simp [orElse]

Result:
no goals

Proof state:
α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think <|> c₂.think).destruct = Sum.inr (c₁ <|> c₂)

Tactic:
unfold_projs

Result:
α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think.orElse fun x => c₂.think).destruct = Sum.inr (c₁.orElse fun x => c₂)
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Icc_succ_left_eq_Ioc (a b : α) : Icc (succ a) b = Ioc a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ ↑(Icc (succ a) b) = ↑(Ioc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_left_mem_of_not_le (a_mem : a ∈ 𝒜 i) (h : ¬i ≤ n) :
    (decompose 𝒜 (a * b) n : A) = 0

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = 0

Tactic:
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

Tactic:
lift a to 𝒜 i using a_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = 0
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem range_face_points {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : Set.range (s.face h).points = s.points '' ↑fs

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ Set.range (s.face h).points = s.points '' ↑fs

Tactic:
rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_ext {f₁ f₂ g₁ g₂ : R} {U hu₁ hu₂} (h : f₁ * g₂ = f₂ * g₁) :
    const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂ :=
  Subtype.eq <|
    funext fun x =>
      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

Proof state:
R : Type u
inst✝ : CommRing R
f₁ f₂ g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl
h : f₁ * g₂ = f₂ * g₁
x : ↥(unop (op U))
⊢ ↑⟨g₁, ⋯⟩ * f₂ = ↑⟨g₂, ⋯⟩ * f₁

Tactic:
rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_mul_of_tdiv_eq_right {a b c : Int}
    (H1 : b ∣ a) (H2 : a.tdiv b = c) : a = b * c

Proof state:
a b c : Int
H1 : b ∣ a
H2 : a.tdiv b = c
⊢ a = b * c

Tactic:
rw [← H2, Int.mul_tdiv_cancel' H1]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem deriv_fourierIntegral
    {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) :
    deriv (𝓕 f) = 𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
⊢ deriv (𝓕 f) = 𝓕 fun x => (-2 * ↑π * I * ↑x) • f x

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
x : ℝ
⊢ deriv (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) x

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x => x • f x) volume
x : ℝ
⊢ deriv (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) x

Tactic:
exact (hasDerivAt_fourierIntegral hf hf' x).deriv

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem AEMeasurable.nnreal_tsum {α : Type*} {_ : MeasurableSpace α} {ι : Type*} [Countable ι]
    {f : ι → α → NNReal} {μ : Measure α} (h : ∀ i : ι, AEMeasurable (f i) μ) :
    AEMeasurable (fun x : α => ∑' i : ι, f i x) μ

Proof state:
α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => (∑' (b : ι), ↑(f b x)).toNNReal) μ

Tactic:
exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Result:
no goals

Proof state:
α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => ∑' (i : ι), f i x) μ

Tactic:
simp_rw [NNReal.tsum_eq_toNNReal_tsum]

Result:
α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => (∑' (b : ι), ↑(f b x)).toNNReal) μ
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ι_leftInverse : Function.LeftInverse ιInv (ι R : M → ExteriorAlgebra R M) := fun x => by
  -- Porting note: Original proof didn't have `letI` and `haveI`
  letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
  haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
  simp [ιInv]

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ ιInv ((ι R) x) = x

Tactic:
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ ιInv ((ι R) x) = x

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ ιInv ((ι R) x) = x

Tactic:
simp [ιInv]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ ιInv ((ι R) x) = x

Tactic:
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ ιInv ((ι R) x) = x
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_pullback {X Y : C} (g : X ⟶ Y) (f₁ f₂) :
    (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Tactic:
apply Quotient.ind'

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₁ f₂ : Subobject Y
⊢ (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Tactic:
revert f₁

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Tactic:
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
  map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp,
  pullback.condition]

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (pullback.snd f₁.arrow g)).obj ((pullback (pullback.snd f₁.arrow g ≫ g)).obj f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂

Tactic:
intro f₁

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (pullback.snd f₁.arrow g)).obj ((pullback (pullback.snd f₁.arrow g ≫ g)).obj f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem map_inr : q.map (inr R M M₂) = prod ⊥ q

Proof state:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q

Tactic:
simp [and_left_comm, eq_comm, and_comm]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
⊢ map (inr R M M₂) q = ⊥.prod q

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
    {h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
h : k ∈ m.alter k f
⊢ (m.alter k f).getKey k h = k

Tactic:
simp [getKey_alter]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set (a : α) {m n} (l : List α) :
    (set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
⊢ (l.set m a).get? n = if m = n then (fun x => a) <$> l.get? n else l.get? n

Tactic:
simp [getElem?_set']

Result:
α : Type u_1
a : α
m n : Nat
l : List α
⊢ (if m = n then Option.map (Function.const α a) l[n]? else l[n]?) =
    if m = n then Option.map (fun x => a) l[n]? else l[n]?

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
⊢ (if m = n then Option.map (Function.const α a) l[n]? else l[n]?) =
    if m = n then Option.map (fun x => a) l[n]? else l[n]?

Tactic:
rfl

Result:
no goals