harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
theorem whiskerRight_comp (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g) ▷ Q = f ▷ Q ≫ g ▷ Q

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
Q X Y Z : LocalizedMonoidal L W ε
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ▷ Q = f ▷ Q ≫ g ▷ Q

Tactic:
simp only [← tensorHom_id, ← tensor_comp, comp_id]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousAt.comp_continuousWithinAt_of_eq {g : β → γ} {y : β}
    (hg : ContinuousAt g y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
hf : ContinuousWithinAt f s x
hg : ContinuousAt g (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_continuousWithinAt hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
y : β
hg : ContinuousAt g y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
hf : ContinuousWithinAt f s x
hg : ContinuousAt g (f x)
⊢ ContinuousWithinAt (g ∘ f) s x
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma integrable_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℚ) :
    Integrable (fun a ↦ (preCDF ρ x a).toReal) ρ.fst

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
⊢ Integrable (fun a => (preCDF ρ x a).toReal) ρ.fst

Tactic:
refine integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
⊢ AEStronglyMeasurable (fun a => (preCDF ρ x a).toReal) ρ.fst

case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ ρ.fst univ

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst

Tactic:
refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ρ.fst univ

Tactic:
rw [← lintegral_one]

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ ρ.fst univ

Tactic:
simp_rw [← ofReal_norm_eq_enorm, Real.norm_of_nonneg ENNReal.toReal_nonneg]

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ρ.fst univ

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ⊤
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
⊢ AEStronglyMeasurable (fun a => (preCDF ρ x a).toReal) ρ.fst

Tactic:
exact measurable_preCDF.ennreal_toReal.aestronglyMeasurable

Result:
no goals
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma ruzsaSzemerediNumberNat_le : ruzsaSzemerediNumberNat n ≤ n.choose 3 :=
  ruzsaSzemerediNumber_le.trans_eq <| by rw [Fintype.card_fin]

Proof state:
n : ℕ
⊢ (Fintype.card (Fin n)).choose 3 = n.choose 3

Tactic:
rw [Fintype.card_fin]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem map_dotProduct [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v w : n → R) :
    f (v ⬝ᵥ w) = f ∘ v ⬝ᵥ f ∘ w

Proof state:
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w

Tactic:
simp only [dotProduct, map_sum f, f.map_mul, Function.comp]

Result:
no goals
-- Mathlib/NumberTheory/GaussSum.lean
theorem gaussSum_frob (χ : MulChar R R') (ψ : AddChar R R') :
    gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)

Tactic:
rw [← frobenius_def, gaussSum, gaussSum, map_sum]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, (frobenius R' p) (χ x * ψ x) = ∑ a : R, (χ ^ p) a * (ψ ^ p) a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, (frobenius R' p) (χ x * ψ x) = ∑ a : R, (χ ^ p) a * (ψ ^ p) a

Tactic:
simp_rw [pow_apply' χ fp.1.ne_zero, map_mul, frobenius_def]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, χ x ^ p * ψ x ^ p = ∑ x : R, χ x ^ p * (ψ ^ p) x

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x : R, χ x ^ p * ψ x ^ p = ∑ x : R, χ x ^ p * (ψ ^ p) x

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem basisFun_apply [DecidableEq η] (i) :
    basisFun R η i = Pi.single i 1

Proof state:
R : Type u_1
η : Type u_2
inst✝² : Semiring R
inst✝¹ : Finite η
inst✝ : DecidableEq η
i : η
⊢ (basisFun R η) i = single i 1

Tactic:
simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_map_fst (m) (l : Vector α n) : map Prod.fst (zipIdx l m) = l

Proof state:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ map Prod.fst ({ toArray := l, size_toArray := ⋯ }.zipIdx m) = { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.zipIdx_map_fst]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
l : Vector α n
⊢ map Prod.fst (l.zipIdx m) = l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ map Prod.fst ({ toArray := l, size_toArray := ⋯ }.zipIdx m) = { toArray := l, size_toArray := ⋯ }
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma nat_eq_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) = n ↔ m = n

Proof state:
m : ℕ
n : ℕ∞
⊢ ↑m = ↑n ↔ ↑m = n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_sub_int (m : ℤ) (h : Irrational (x - m)) : Irrational x :=
  of_sub_rat m <| by rwa [Rat.cast_intCast]

Proof state:
x : ℝ
m : ℤ
h : Irrational (x - ↑m)
⊢ Irrational (x - ↑↑m)

Tactic:
rwa [Rat.cast_intCast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_two_sub (x : ℝ) : tan (π / 2 - x) = (tan x)⁻¹

Proof state:
x : ℝ
⊢ tan (π / 2 - x) = (tan x)⁻¹

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem equivOfIsometry_refl :
    (equivOfIsometry <| QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

Proof state:
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
x : CliffordAlgebra Q₁
⊢ (equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁)) x = AlgEquiv.refl x

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
x : CliffordAlgebra Q₁
⊢ (equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁)) x = AlgEquiv.refl x

Tactic:
exact AlgHom.congr_fun (map_id Q₁) x

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup_symmDiff_iSup_le {g : ι → α} : (⨆ i, f i) ∆ (⨆ i, g i) ≤ ⨆ i, ((f i) ∆ (g i))

Proof state:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ ⨆ i, f i ≤ ⨆ x, g x ⊔ f x ∆ g x ∧ ⨆ i, g i ≤ ⨆ x, f x ⊔ f x ∆ g x

Tactic:
exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
  iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

Result:
no goals

Proof state:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ (⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i

Tactic:
simp_rw [symmDiff_le_iff, ← iSup_sup_eq]

Result:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ ⨆ i, f i ≤ ⨆ x, g x ⊔ f x ∆ g x ∧ ⨆ i, g i ≤ ⨆ x, f x ⊔ f x ∆ g x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α} :
    get! (m.erase k) a = if k == a then default else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
k a : α
⊢ get! (m.erase k) a = if (k == a) = true then default else get! m a

Tactic:
simp_to_model [erase] using List.getValue!_eraseKey

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem leadingCoeff_of_injective (hf : Injective f) (p : R[X]) :
    leadingCoeff (p.map f) = f (leadingCoeff p)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)

Tactic:
rw [coeff_map f, natDegree_map_eq_of_injective hf p]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
delta leadingCoeff

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)
-- Mathlib/SetTheory/Descriptive/Tree.lean
lemma mem_of_prefix {x y : List A} (h' : x <+: y) (h : y ∈ T) : x ∈ T

Proof state:
case intro
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : x ++ w✝ ∈ T
⊢ x ∈ T

Tactic:
exact mem_of_append h

Result:
no goals

Proof state:
A : Type u_1
T : ↥(tree A)
x y : List A
h' : x <+: y
h : y ∈ T
⊢ x ∈ T

Tactic:
obtain ⟨_, rfl⟩ := h'

Result:
case intro
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : x ++ w✝ ∈ T
⊢ x ∈ T
-- Mathlib/Algebra/Group/Basic.lean
theorem div_left_inj : b / a = c / a ↔ b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ b / a = c / a ↔ b = c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ b * a⁻¹ = c * a⁻¹ ↔ b = c

Tactic:
exact mul_left_inj _

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem xgcdAux_val (x y : R) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Tactic:
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem image_mul_right' :
    image (· * b⁻¹) t = preimage t (· * b) (mul_left_injective _).injOn

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
b : α
⊢ image (fun x => x * b⁻¹) t = t.preimage (fun x => x * b) ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem mul_ι_mul_ι_of_isOrtho (x : CliffordAlgebra Q) {a b : M} (h : Q.IsOrtho a b) :
    x * ι Q a * ι Q b = -(x * ι Q b * ι Q a)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)

Tactic:
rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem and_intro : ∀ {a b : Bool}, a → b → a && b

Proof state:
⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma mul_eq_mul_of_div_eq_div (hb : IsUnit b) (hd : IsUnit d)
    (a c : α) (h : a / b = c / d) : a * d = c * b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b

Tactic:
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Norm.lean
theorem extends_norm' (hf1 : f 1 = 1) (a : R) : f (a • (1 : S)) = ‖a‖

Proof state:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← hf1]

Result:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * f 1

Proof state:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * f 1

Tactic:
exact f.smul' _ _

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem lintegral_enorm_zero : ∫⁻ _ : α, ‖(0 : β)‖ₑ ∂μ = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
⊢ ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
@[simp]
lemma quotUliftToQuot_ι (F : J ⥤ Type u) (j : J) (x : (F ⋙ uliftFunctor.{u'}).obj j) :
    quotUliftToQuot F (Quot.ι _ j x) = Quot.ι F j x.down

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
j : J
x : (F ⋙ uliftFunctor.{u', u}).obj j
⊢ quotUliftToQuot F (Quot.ι (F ⋙ uliftFunctor.{u', u}) j x) = Quot.ι F j x.down

Tactic:
dsimp [quotUliftToQuot, Quot.ι]

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepSet_iff (s : ι → Set Ω) (hs : ∀ i, MeasurableSet (s i))
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepSet m' hm' s μ ↔
      ∀ S : Finset ι, μ⟦⋂ i ∈ S, s i | m'⟧ =ᵐ[μ] ∏ i ∈ S, μ⟦s i | m'⟧

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']

Tactic:
rw [iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs, iCondIndepSets_singleton_iff _ _ _ hs]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma whiskerRight_snd {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    (f ▷ Y) ≫ snd _ _ = snd _ _ :=
  (tensorHom_snd _ _).trans (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ snd X₁ Y ≫ 𝟙 Y = snd X₁ Y

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp]
lemma _root_.absorbs_union : Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t₁ t₂ : Set α
⊢ Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂

Tactic:
simp [Absorbs]

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasStrictDerivAt.complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasStrictDerivAt f f' x) :
    HasStrictFDerivAt f (f' • (1 : ℂ →L[ℝ] ℂ)) x

Proof state:
f : ℂ → ℂ
f' x : ℂ
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (f' • 1) x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight] using h.hasStrictFDerivAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_succ_left (m n : ℕ) :
    uniformBell (m+1) n = choose (m * n + n - 1) (n - 1) * uniformBell m n

Proof state:
m n : ℕ
⊢ (m + 1).uniformBell n = (m * n + n - 1).choose (n - 1) * m.uniformBell n

Tactic:
simp only [uniformBell_eq, Finset.prod_range_succ, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem comap_id (S : Subsemigroup P) : S.comap (MulHom.id _) = S :=
  ext (by simp)

Proof state:
P : Type u_3
inst✝ : Mul P
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem map {f : α →. β} {g : α → β → σ} (hf : Partrec f) (hg : Computable₂ g) :
    Partrec fun a => (f a).map (g a)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β → σ
hf : Partrec f
hg : Computable₂ g
⊢ Partrec fun a => Part.map (g a) (f a)

Tactic:
simpa [bind_some_eq_map] using Partrec.bind (g := fun a x => some (g a x)) hf hg

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem abv_sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c)

Proof state:
S : Type u_5
inst✝² : OrderedRing S
R : Type u_6
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_union {f : β → α} {s t : Set β} :
    ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
simp_rw [mem_union, iSup_or, iSup_sup_eq]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem model_insert_iff {φ : L.Sentence} : M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
T : L.Theory
φ : L.Sentence
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T

Tactic:
rw [Set.insert_eq, model_union_iff, model_singleton_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
    l₁ < l₂ ↔
      (l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i])

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ decide (l₁[i] < l₂[i]) = true) ↔
    l₁ = take l₁.length l₂ ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ l₁ < l₂ ↔
    l₁ = take l₁.length l₂ ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ decide (l₁[i] < l₂[i]) = true) ↔
    l₁ = take l₁.length l₂ ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
lemma weightedVSubOfPoint_vadd (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (v : V) :
    s.weightedVSubOfPoint (v +ᵥ p) b w = s.weightedVSubOfPoint p (-v +ᵥ b) w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
v : V
⊢ (s.weightedVSubOfPoint (v +ᵥ p) b) w = (s.weightedVSubOfPoint p (-v +ᵥ b)) w

Tactic:
simp [vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem abs_exp_sub_one_le {x : ℝ} (hx : |x| ≤ 1) : |exp x - 1| ≤ 2 * |x|

Proof state:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|

Tactic:
exact_mod_cast Complex.norm_exp_sub_one_le (x := x) this

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|

Tactic:
have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Result:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma opProdIsoCoprod_hom_fst : (opProdIsoCoprod A B).hom.unop ≫ prod.fst = coprod.inl.unop

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).hom.unop ≫ prod.fst = coprod.inl.unop

Tactic:
simp [opProdIsoCoprod]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_const_mul_left {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) :
    (fun x ↦ c * f x) =Θ[l] g ↔ f =Θ[l] g

Proof state:
α : Type u_1
F : Type u_4
𝕜 : Type u_14
inst✝¹ : Norm F
inst✝ : NormedField 𝕜
g : α → F
l : Filter α
c : 𝕜
f : α → 𝕜
hc : c ≠ 0
⊢ (fun x => c * f x) =Θ[l] g ↔ f =Θ[l] g

Tactic:
simpa only [← smul_eq_mul] using isTheta_const_smul_left hc

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosed_empty : InfClosed (∅ : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
⊢ InfClosed ∅

Tactic:
simp [InfClosed]

Result:
no goals