harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self [Fintype ι']
    (a : OrthonormalBasis ι' 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) :
    (a.toBasis.toMatrix b)ᴴ * a.toBasis.toMatrix b = 1

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
⊢ (a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b = 1

Tactic:
ext i j

Result:
case a
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ ((a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b) i j = 1 i j

Proof state:
case a
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ ((a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b) i j = 1 i j

Tactic:
convert a.repr.inner_map_map (b i) (b j)

Result:
case h.e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = inner (b i) (b j)

Proof state:
case h.e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = inner (b i) (b j)

Tactic:
rw [orthonormal_iff_ite.mp b.orthonormal i j]

Result:
case h.e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = if i = j then 1 else 0

Proof state:
case h.e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = if i = j then 1 else 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_one_sub_ordered [LinearOrder ι] (s : Finset ι) (f : ι → α) :
    ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ filter (fun j => j < i) s, (1 - f j)

Tactic:
rw [prod_sub_ordered]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ filter (fun j => j < i) s, (1 - f j)) * ∏ j ∈ filter (fun j => i < j) s, 1 =
    1 - ∑ i ∈ s, f i * ∏ j ∈ filter (fun j => j < i) s, (1 - f j)

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ filter (fun j => j < i) s, (1 - f j)) * ∏ j ∈ filter (fun j => i < j) s, 1 =
    1 - ∑ i ∈ s, f i * ∏ j ∈ filter (fun j => j < i) s, (1 - f j)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem mul_sub_algebraMap_pow_commutes [Ring A] [Algebra R A] (x : A) (r : R) (n : ℕ) :
    x * (x - algebraMap R A r) ^ n = (x - algebraMap R A r) ^ n * x

Proof state:
case zero
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - (algebraMap R A) r) ^ 0 = (x - (algebraMap R A) r) ^ 0 * x

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ x * (x - (algebraMap R A) r) ^ (n + 1) = (x - (algebraMap R A) r) ^ (n + 1) * x

Tactic:
rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

Result:
no goals

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
⊢ x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/AbsolutelyContinuous.lean
lemma MutuallySingular.compProd_of_right' (μ ν : Measure α) (hκη : ∀ᵐ a ∂ν, κ a ⟂ₘ η a) :
    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ ∀ᵐ (a : α) ∂ν, η a ⟂ₘ κ a

Tactic:
simp_rw [MutuallySingular.comm, hκη]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
refine (MutuallySingular.compProd_of_right _ _ ?_).symm

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ ∀ᵐ (a : α) ∂ν, η a ⟂ₘ κ a
-- Mathlib/Order/UpperLower/Basic.lean
theorem IsUpperSet.image (hs : IsUpperSet s) (f : α ≃o β) : IsUpperSet (f '' s : Set β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑f '' s)

Tactic:
change IsUpperSet ((f : α ≃ β) '' s)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑↑f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)

Tactic:
exact hs.preimage f.symm.monotone

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑↑f '' s)

Tactic:
rw [Set.image_equiv_eq_preimage_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)
-- Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
lemma mfderiv_chartAt_eq_tangentCoordChange {x y : M} (hsrc : x ∈ (chartAt H y).source) :
    mfderiv I I (chartAt H y) x = tangentCoordChange I x y x

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
inst✝ : IsManifold I 1 M
x y : M
hsrc : x ∈ (chartAt H y).source
this : MDifferentiableAt I I (↑(ChartedSpace.chartAt y)) x
⊢ mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x

Tactic:
simp [mfderiv, if_pos this, Function.comp_assoc]

Result:
no goals

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
inst✝ : IsManifold I 1 M
x y : M
hsrc : x ∈ (chartAt H y).source
⊢ mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x

Tactic:
have := mdifferentiableAt_atlas (I := I) (ChartedSpace.chart_mem_atlas _) hsrc

Result:
𝕜 : 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
inst✝ : IsManifold I 1 M
x y : M
hsrc : x ∈ (chartAt H y).source
this : MDifferentiableAt I I (↑(ChartedSpace.chartAt y)) x
⊢ mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem SeminormedCommGroup.mem_closure_iff :
    a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
s : Set E
a : E
⊢ a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Tactic:
simp [Metric.mem_closure_iff, dist_eq_norm_div]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem HasSum.norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : HasSum f a)
    (hg : HasSum g b) (h : ∀ i, ‖f i‖ ≤ g i) : ‖a‖ ≤ b

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : E
b : ℝ
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖a‖ ≤ b

Tactic:
classical exact le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : E
b : ℝ
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖a‖ ≤ b

Tactic:
exact le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getLsb?_isSome (x : BitVec w) (i : Nat) : x[i]?.isSome → i < w

Proof state:
case some
w : Nat
x : BitVec w
i : Nat
val✝ : Bool
h : x[i]? = some val✝
⊢ (some val✝).isSome = true → i < w

Tactic:
by_cases i < w <;> simp_all

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x[i]?.isSome = true → i < w

Tactic:
cases h : x[i]? with
| none => simp
| some => by_cases i < w <;> simp_all

Result:
no goals

Proof state:
case none
w : Nat
x : BitVec w
i : Nat
h : x[i]? = none
⊢ none.isSome = true → i < w

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem eq_bot_of_commute_of_self (H : A.LinearDisjoint A)
    (hc : ∀ (a b : A), Commute a.1 b.1) : A = ⊥

Proof state:
R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
⊢ A ⊓ A = ⊥

Tactic:
exact H.inf_eq_bot_of_commute hc

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
⊢ A = ⊥

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢

Result:
R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
⊢ A ⊓ A = ⊥
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBySet_iff_torsionBySet_eq_top :
    IsTorsionBySet R M s ↔ torsionBySet R M s = ⊤ :=
  ⟨fun h => eq_top_iff.mpr fun _ _ => (mem_torsionBySet_iff _ _).mpr <| @h _, fun h x => by
    rw [← mem_torsionBySet_iff, h]
    trivial⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ ∀ ⦃a : ↑s⦄, ↑a • x = 0

Tactic:
rw [← mem_torsionBySet_iff, h]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_trailingCoeff (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) :
    (trinomial k m n u v w).trailingCoeff = u

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).trailingCoeff = u

Tactic:
rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
theorem smul_left [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : μ ≪ ν) (c : R) :
    c • μ ≪ ν := fun s hνs => by
  simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

Proof state:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : ν s = 0
⊢ (c • μ) s = 0

Tactic:
simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem Codisjoint.map_orderIso [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β]
    {a b : α} (f : α ≃o β) (ha : Codisjoint a b) : Codisjoint (f a) (f b)

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ f ⊤ ≤ f (a ⊔ b)

Tactic:
exact f.monotone ha.top_le

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (f a) (f b)

Tactic:
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]

Result:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ f ⊤ ≤ f (a ⊔ b)
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_smul [IsScalarTower R ℝ≥0 ℝ≥0] [PseudoMetricSpace R] [Zero R]
    [BoundedSMul R ℝ≥0] (μ : FiniteMeasure Ω) (c : R) (f : Ω →ᵇ ℝ≥0) :
    μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : BoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), c • 1 * ↑(f ω) ∂↑μ = c • 1 * ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

Tactic:
exact lintegral_const_mul (c • (1 : ℝ≥0∞)) f.measurable_coe_ennreal_comp

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : BoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), c • ↑(f ω) ∂↑μ = c • ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

Tactic:
simp_rw [← smul_one_smul ℝ≥0∞ c (f _ : ℝ≥0∞), ← smul_one_smul ℝ≥0∞ c (lintegral _ _ : ℝ≥0∞),
  smul_eq_mul]

Result:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : BoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), c • 1 * ↑(f ω) ∂↑μ = c • 1 * ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

Proof state:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : BoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

Tactic:
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, testAgainstNN_coe_eq,
  ENNReal.coe_smul]

Result:
Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : BoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), c • ↑(f ω) ∂↑μ = c • ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem ContinuousOn.isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α}
    (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable (f '' s)

Tactic:
rw [image_eq_range, ← image_univ]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable ((fun x => f ↑x) '' univ)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable ((fun x => f ↑x) '' univ)

Tactic:
exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
    (flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h)

Proof state:
α : Type ?u.26537
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ (findSome? (fun l => l.head?) L).isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ L.flatten.head ⋯ = (findSome? (fun l => l.head?) L).get ⋯

Tactic:
simp [head_eq_iff_head?_eq_some, head?_flatten]

Result:
no goals

Proof state:
α : Type ?u.26537
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ L.flatten ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_rotation (θ₁ θ₂ : Real.Angle) (x : V) :
    o.rotation θ₁ (o.rotation θ₂ x) = o.rotation (θ₁ + θ₂) x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ θ₁.cos • (θ₂.cos • x + θ₂.sin • o.rightAngleRotation x) + θ₁.sin • (θ₂.cos • o.rightAngleRotation x + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x + (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) • o.rightAngleRotation x

Tactic:
module

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ (o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x

Tactic:
simp only [o.rotation_apply, Real.Angle.cos_add, Real.Angle.sin_add, LinearIsometryEquiv.map_add,
  LinearIsometryEquiv.trans_apply, map_smul, rightAngleRotation_rightAngleRotation]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ θ₁.cos • (θ₂.cos • x + θ₂.sin • o.rightAngleRotation x) + θ₁.sin • (θ₂.cos • o.rightAngleRotation x + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x + (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) • o.rightAngleRotation x
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem π_tensor_id_actRight :
    (coequalizer.π _ _ ▷ T.X) ≫ actRight P Q =
      (α_ _ _ _).hom ≫ (P.X ◁ Q.actRight) ≫ coequalizer.π _ _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q =
    (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
erw [map_π_preserves_coequalizer_inv_colimMap (tensorRight _)]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ≫
      coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ≫
      coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
simp only [Category.assoc]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_one (S : Type*) [Semiring S] (n : ℕ) :
    (ascPochhammer S n).eval (1 : S) = (n ! : S)

Proof state:
S : Type u_2
inst✝ : Semiring S
n : ℕ
⊢ eval 1 (ascPochhammer S n) = ↑n !

Tactic:
rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem sum_ite_self_eq' [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (x = a) v 0) = f a

Proof state:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = if a ∈ f.support then id (f a) else 0

Tactic:
simp [ite_eq_right_iff.2 Eq.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v => if x = a then v else 0) = f a

Tactic:
convert f.sum_ite_eq' a fun _ => id

Result:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = if a ∈ f.support then id (f a) else 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v => if x = a then v else 0) = f a

Tactic:
classical
  convert f.sum_ite_eq' a fun _ => id
  simp [ite_eq_right_iff.2 Eq.symm]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem codisjoint_coe : Codisjoint (a : α) b ↔ Codisjoint a b

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Codisjoint ↑a ↑b ↔ Codisjoint a b

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]

Result:
no goals