harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma absolutelyContinuous_sum_right {μs : ι → Measure α} (i : ι) (hνμ : ν ≪ μs i) :
    ν ≪ Measure.sum μs

Proof state:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : (sum μs) s = 0
⊢ ν s = 0

Tactic:
simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0

Result:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), (μs i) s = 0
⊢ ν s = 0

Proof state:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
⊢ ν ≪ sum μs

Tactic:
refine AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_

Result:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : (sum μs) s = 0
⊢ ν s = 0

Proof state:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), (μs i) s = 0
⊢ ν s = 0

Tactic:
exact hνμ (hs0 i)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_left_mono [IsDomain R] {x : R} (hx : x ≠ 0) :
    I * span {x} ≤ J * span {x} ↔ I ≤ J

Proof state:
R : Type u
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ I * span {x} ≤ J * span {x} ↔ I ≤ J

Tactic:
simpa only [mul_comm I, mul_comm J] using span_singleton_mul_right_mono hx

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem mul_spec [Nonempty N] {i} {p q : Ω^ N X x} :
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: introduce `HomotopyGroup.mk` and remove defeq abuse.
    ((· * ·) : _ → _ → HomotopyGroup N X x) ⟦p⟧ ⟦q⟧ = ⟦transAt i q p⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 => x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧

Tactic:
apply Quotient.sound

Result:
case a
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm
      (Path.trans ((loopHomeo (Classical.arbitrary N)).toEquiv q) ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈
    fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))

Proof state:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 => x1 * x2) ⟦p⟧ ⟦q⟧ = ⟦transAt i q p⟧

Tactic:
rw [transAt_indep (Classical.arbitrary N) q, ← fromLoop_trans_toLoop]

Result:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 => x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧

Proof state:
case a
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm
      (Path.trans ((loopHomeo (Classical.arbitrary N)).toEquiv q) ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈
    fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See also `inv_le_of_inv_le₀` for a one-sided implication with one fewer assumption. -/
lemma inv_le_comm₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem tendsto_iterate_fixedPoint (x) :
    Tendsto (fun n ↦ f^[n] x) atTop (𝓝 <| fixedPoint f hf)

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ Tendsto (fun n => f^[n] x) atTop (𝓝 (fixedPoint f hf))

Tactic:
convert tendsto_iterate_efixedPoint hf (edist_ne_top x _)

Result:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x ⋯

Proof state:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x ⋯

Tactic:
refine (fixedPoint_unique _ ?_).symm

Result:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x ⋯)

Proof state:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x ⋯)

Tactic:
apply efixedPoint_isFixedPt

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem setLIntegral_pdf_le_map {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
    (μ : Measure E

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
s : Set E
⊢ (withDensity μ (pdf X ℙ μ)) s ≤ (map X ℙ) s

Tactic:
exact withDensity_pdf_le_map _ _ _ s

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
s : Set E
⊢ ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ ≤ (map X ℙ) s

Tactic:
apply (withDensity_apply_le _ s).trans

Result:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
s : Set E
⊢ (withDensity μ (pdf X ℙ μ)) s ≤ (map X ℙ) s
-- Mathlib/Topology/Order.lean
theorem isOpen_iSup_iff {s : Set α} : IsOpen[⨆ i, t i] s ↔ ∀ i, IsOpen[t i] s :=
  show s ∈ {s | IsOpen[iSup t] s} ↔ s ∈ { x : Set α | ∀ i : ι, IsOpen[t i] x } by
    simp [setOf_isOpen_iSup]

Proof state:
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ s ∈ {s | IsOpen s} ↔ s ∈ {x | ∀ (i : ι), IsOpen x}

Tactic:
simp [setOf_isOpen_iSup]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_omega0 : IsLimit ω

Proof state:
o : Ordinal.{u_1}
h : o < ω
⊢ succ o < ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Result:
case intro
n : ℕ
h : ↑n < ω
⊢ succ ↑n < ω

Proof state:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω

Tactic:
refine ⟨omega0_ne_zero, fun o h => ?_⟩

Result:
o : Ordinal.{u_1}
h : o < ω
⊢ succ o < ω

Proof state:
⊢ ω.IsLimit

Tactic:
rw [isLimit_iff, isSuccPrelimit_iff_succ_lt]

Result:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω

Proof state:
case intro
n : ℕ
h : ↑n < ω
⊢ succ ↑n < ω

Tactic:
exact nat_lt_omega0 (n + 1)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_apply (μ : Measure α) [SFinite μ] (f : α → ℝ) (s : Set α) :
    μ.tilted f s = ∫⁻ a in s, ENNReal.ofReal (exp (f a) / ∫ x, exp (f x) ∂μ) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ

Tactic:
rw [Measure.tilted, withDensity_apply' _ s]

Result:
no goals
-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- If the composition of two continuous functions `g ∘ f` is proper and `g` is injective,
then `f` is proper. -/
lemma isProperMap_of_comp_of_inj {f : X → Y} {g : Y → Z} (hf : Continuous f) (hg : Continuous g)
    (hgf : IsProperMap (g ∘ f)) (g_inj : g.Injective) : IsProperMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
⊢ IsProperMap f

Tactic:
refine ⟨hf, fun ℱ y h ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
x : X
hx1 : (g ∘ f) x = g y
hx2 : ClusterPt x ℱ
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
exact ⟨x, g_inj hx1, hx2⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
rcases hgf.clusterPt_of_mapClusterPt (h.map hg.continuousAt tendsto_map) with ⟨x, hx1, hx2⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
x : X
hx1 : (g ∘ f) x = g y
hx2 : ClusterPt x ℱ
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_map [HasColimitsOfShape K C] (E : K ⥤ J) :
    colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (whiskerLeft E α) ≫ pre G E

Tactic:
rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (whiskerLeft E α).app j✝ ≫ ι G (E.obj j✝)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ pre G E

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (whiskerLeft E α) ≫ pre G E

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (whiskerLeft E α).app j✝ ≫ ι G (E.obj j✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem smul {R : Type*} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {r : R}
    {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ≪ᵥ w) : r • v ≪ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(r • v) s = 0

Tactic:
rw [smul_apply, h hs, smul_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ r • v ≪ᵥ w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(r • v) s = 0
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} :
    IsOpen (connectedComponent x)

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponentIn univ x)

Tactic:
exact isOpen_univ.connectedComponentIn

Result:
no goals

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponent x)

Tactic:
rw [← connectedComponentIn_univ]

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponentIn univ x)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_comap_le : map f (comap f J) ≤ J

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
⊢ map f (comap f J) ≤ J

Tactic:
rw [map_le_iff_le_comap]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem coeff_expand_mul {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff (n * p) = f.coeff n

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (n * p) = f.coeff n

Tactic:
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
    IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
s t : ℝ
⊢ IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ

Tactic:
have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)
⊢ IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)
⊢ IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ

Tactic:
change IndepFun ((fun x => exp (s * x)) ∘ X) ((fun x => exp (t * x)) ∘ Y) μ

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)
⊢ IndepFun ((fun x => rexp (s * x)) ∘ X) ((fun x => rexp (t * x)) ∘ Y) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)
⊢ IndepFun ((fun x => rexp (s * x)) ∘ X) ((fun x => rexp (t * x)) ∘ Y) μ

Tactic:
exact IndepFun.comp h_indep (h_meas s) (h_meas t)

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

Proof state:
case hC.H
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M✝ : (Matrix n n R)[X]
r : R
M : Matrix n n R
⊢ (((aeval r).mapMatrix.comp ↑matPolyEquiv.symm).comp CAlgHom) M =
    ((eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯).comp CAlgHom) M

Tactic:
simp [Function.comp_def]

Result:
no goals

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
⊢ (matPolyEquiv.symm M).map (eval r) = eval ((scalar n) r) M

Tactic:
suffices ((aeval r).mapMatrix.comp matPolyEquiv.symm.toAlgHom : (Matrix n n R)[X] →ₐ[R] _) =
    (eval₂AlgHom' (AlgHom.id R _) (scalar n r)
      fun x => (scalar_commute _ (Commute.all _) _).symm) from
  DFunLike.congr_fun this M

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ (aeval r).mapMatrix.comp ↑matPolyEquiv.symm = eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯

Proof state:
case hC
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm).comp CAlgHom =
    (eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯).comp CAlgHom

Tactic:
ext M : 1

Result:
case hC.H
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M✝ : (Matrix n n R)[X]
r : R
M : Matrix n n R
⊢ (((aeval r).mapMatrix.comp ↑matPolyEquiv.symm).comp CAlgHom) M =
    ((eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯).comp CAlgHom) M

Proof state:
case hX
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm) X = (eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯) X

Tactic:
simp [smul_eq_diagonal_mul]

Result:
no goals

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
⊢ (aeval r).mapMatrix.comp ↑matPolyEquiv.symm = eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯

Tactic:
ext : 1

Result:
case hC
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm).comp CAlgHom =
    (eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯).comp CAlgHom

case hX
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm) X = (eval₂AlgHom' (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯) X
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.size, a[i] = b

Proof state:
α : Type u_1
b : α
i : Nat
a : Array α
⊢ some b = a[i]? ↔ ∃ h, a[i] = b

Tactic:
rw [eq_comm, getElem?_eq_some_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem LinearMap.annihilator_le_of_surjective (f : M →ₗ[R] M')
    (hf : Function.Surjective f) : Module.annihilator R M ≤ Module.annihilator R M' := fun x h ↦ by
  rw [Module.mem_annihilator] at h ⊢
  intro m; obtain ⟨m, rfl⟩ := hf m
  rw [← map_smul, h, f.map_zero]

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
⊢ ∀ (m : M'), x • m = 0

Tactic:
intro m

Result:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M'
⊢ x • m = 0

Proof state:
case intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ x • f m = 0

Tactic:
rw [← map_smul, h, f.map_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M'
⊢ x • m = 0

Tactic:
obtain ⟨m, rfl⟩ := hf m

Result:
case intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ x • f m = 0

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : x ∈ Module.annihilator R M
⊢ x ∈ Module.annihilator R M'

Tactic:
rw [Module.mem_annihilator] at h ⊢

Result:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
⊢ ∀ (m : M'), x • m = 0
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma mul_zero_subset (s : Set α) : s * 0 ⊆ 0

Proof state:
α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_def, mem_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
    x.getLsbD i.rev = x.getMsbD i

Proof state:
case e_n
w : Nat
x : BitVec w
i : Fin w
⊢ w - (↑i + 1) = w - 1 - ↑i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getLsbD ↑i.rev = x.getMsbD ↑i

Tactic:
simp only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_true, Bool.true_and]

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ x.toNat.testBit (w - (↑i + 1)) = x.toNat.testBit (w - 1 - ↑i)

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.toNat.testBit (w - (↑i + 1)) = x.toNat.testBit (w - 1 - ↑i)

Tactic:
congr 1

Result:
case e_n
w : Nat
x : BitVec w
i : Fin w
⊢ w - (↑i + 1) = w - 1 - ↑i