internlm/Lean-Github huggingface dataset:
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
dec : Decidable c
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
⊢ IsLinearMap R fun x => if c then t x else e x
Tactic:
induction dec
Proof state after:
case isFalse
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h✝ : ¬c
⊢ IsLinearMap R fun x => if c then t x else e x

case isTrue
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h✝ : c
⊢ IsLinearMap R fun x => if c then t x else e x
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : c
⊢ IsLinearMap R fun x => if c then t x else e x
Tactic:
case isTrue h  => simp[h]; fun_prop
Proof state after:
no goals
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : ¬c
⊢ IsLinearMap R fun x => if c then t x else e x
Tactic:
case isFalse h => simp[h]; fun_prop
Proof state after:
no goals
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : c
⊢ IsLinearMap R fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : c
⊢ IsLinearMap R fun x => t x
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : c
⊢ IsLinearMap R fun x => t x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : ¬c
⊢ IsLinearMap R fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : ¬c
⊢ IsLinearMap R fun x => e x
Theorem: ite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.166215
ι : Type ?u.166218
E : ι → Type ?u.166223
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsLinearMap R t
he : IsLinearMap R e
h : ¬c
⊢ IsLinearMap R fun x => e x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
dec : Decidable c
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
induction dec
Proof state after:
case isFalse
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h✝ : ¬c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x

case isTrue
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h✝ : c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isTrue h  => simp[h]; apply ht
Proof state after:
no goals
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : ¬c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isFalse h => simp[h]; apply he
Proof state after:
no goals
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[h]
Proof state after:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : c
⊢ IsLinearMap R fun x => t ⋯ x
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : c
⊢ IsLinearMap R fun x => t ⋯ x
Tactic:
apply ht
Proof state after:
no goals
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : ¬c
⊢ IsLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[h]
Proof state after:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : ¬c
⊢ IsLinearMap R fun x => e ⋯ x
Theorem: dite.arg_te.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.170153
ι : Type ?u.170156
E : ι → Type ?u.170161
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsLinearMap R (e p)
h : ¬c
⊢ IsLinearMap R fun x => e ⋯ x
Tactic:
apply he
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a1.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.177202
ι : Type ?u.177205
E : ι → Type ?u.177210
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : R
f : X → Y
hf : IsLinearMap R f
a : Y →ₗ[R] Y := mk' (fun z => c • z) ⋯
b : X →ₗ[R] Y := mk' f hf
⊢ ∀ (x : X), c • f x = (a ∘ₗ b) x
Tactic:
simp (config:={zetaDelta:=true})
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.229117
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.229120
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.229206
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.229209
inst✝ : FinVec IZ K Z
i : IX
⊢ IsLinearMap K fun x => ℼ i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DualBasis.dualProj.arg_x.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.235784
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.235787
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.235873
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.235876
inst✝ : FinVec IZ K Z
i : IX
⊢ IsLinearMap K fun x => ℼ' i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.toDual.arg_x.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.242451
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.242454
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.242540
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.242543
inst✝ : FinVec IZ K Z
⊢ IsLinearMap K fun x => toDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.246767
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.246770
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.246856
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.246859
inst✝ : FinVec IZ K Z
⊢ IsLinearMap K fun x => fromDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Measure.restrict_restrict
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
t w : R
X : Type u_1
inst✝ : MeasurableSpace X
μ : Measure X
A B : Set X
⊢ (μ.restrict A).restrict B = μ.restrict (A ∩ B)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Measure.prod_restrict
Proof state before:
R : Type
inst✝³ : RealScalar R
inst✝² : MeasureSpace R
t w : R
X : Type u_1
Y : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
A : Set X
B : Set Y
⊢ Measure.prod (μ.restrict A) (ν.restrict B) = (Measure.prod μ ν).restrict (A ×ˢ B)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Measure.prod_volume
Proof state before:
R : Type
inst✝³ : RealScalar R
inst✝² : MeasureSpace R
t w : R
X : Type u_1
Y : Type u_2
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
⊢ Measure.prod volume volume = volume
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.bungeeDomain_preimage
Proof state before:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' bungeeDomain height = if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
unfold bungeeDomain
Proof state after:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} = if x ∈ Icc 1 height then Icc 0 x else ∅
Theorem: SciLean.bungeeDomain_preimage
Proof state before:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} = if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
ext
Proof state after:
case h
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x x✝ : R
⊢ x✝ ∈ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} ↔
    x✝ ∈ if x ∈ Icc 1 height then Icc 0 x else ∅
Theorem: SciLean.bungeeDomain_preimage
Proof state before:
case h
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x x✝ : R
⊢ x✝ ∈ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} ↔
    x✝ ∈ if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
simp[and_assoc]
Proof state after:
no goals
Theorem: SciLean.ite_apply
Proof state before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.ite_apply
Proof state before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
h : c
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.ite_apply
Proof state before:
R : Type ?u.110294
inst✝⁶ : RealScalar R
W : Type ?u.110300
inst✝⁵ : SemiHilbert R W
X : Type ?u.110330
inst✝⁴ : SemiHilbert R X
Y : Type ?u.110354
inst✝³ : SemiHilbert R Y
Z : Type ?u.110378
inst✝² : SemiHilbert R Z
inst✝¹ : MeasureSpace R
m l₁ l₂ k₁ k₂ α✝ height : R
α : Type u_1
β : Type u_2
c : Prop
inst✝ : Decidable c
t e : α → β
x : α
h : ¬c
⊢ (if c then t else e) x = if c then t x else e x
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_bind
Proof state before:
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ bind (bind x g) f = bind x fun x' => bind (g x') f
Tactic:
apply ext
Proof state after:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val

case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval