internlm/Lean-Github huggingface dataset:
Theorem: SciLean.IsContinuousLinearMap.starRingEnd.arg_a.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.262135
inst✝⁴¹ : Semiring R✝¹
X✝² : Type ?u.262141
inst✝⁴⁰ : TopologicalSpace X✝²
inst✝³⁹ : AddCommMonoid X✝²
inst✝³⁸ : Module R✝¹ X✝²
Y✝² : Type ?u.262175
inst✝³⁷ : TopologicalSpace Y✝²
inst✝³⁶ : AddCommMonoid Y✝²
inst✝³⁵ : Module R✝¹ Y✝²
R✝ : Type ?u.262207
inst✝³⁴ : Semiring R✝
X✝¹ : Type ?u.262213
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝ X✝¹
Y✝¹ : Type ?u.262247
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝ Y✝¹
Z✝ : Type ?u.262279
inst✝²⁷ : TopologicalSpace Z✝
inst✝²⁶ : AddCommMonoid Z✝
inst✝²⁵ : Module R✝ Z✝
ι✝ : Type ?u.262311
inst✝²⁴ : Fintype ι✝
E✝ : ι✝ → Type ?u.262319
inst✝²³ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²² : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²¹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.262369
inst✝²⁰ : Semiring R
X✝ : Type ?u.262375
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R X✝
Y✝ : Type ?u.262410
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R Y✝
Z : Type ?u.262443
inst✝¹³ : TopologicalSpace Z
inst✝¹² : AddCommMonoid Z
inst✝¹¹ : Module R Z
ι : Type ?u.262476
inst✝¹⁰ : Fintype ι
E : ι → Type ?u.262484
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommMonoid (E i)
inst✝⁷ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁶ : RCLike K
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module K X
Y : Type ?u.262741
inst✝² : NormedAddCommGroup Y
inst✝¹ : InnerProductSpace K Y
inst✝ : CompleteSpace Y
f : X → K
x✝ : IsContinuousLinearMap K f
⊢ IsContinuousLinearMap K fun x => (starRingEnd K) (f x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsAffineMap.IsAffineMap_id
Proof state before:
R : Type u_1
X : Type u_2
Y : Type ?u.18385
Z : Type ?u.18388
ι : Type ?u.18391
E : ι → Type ?u.18396
inst✝¹¹ : CommRing 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)
⊢ IsAffineMap R fun x => x
Tactic:
constructor
Proof state after:
case is_affine
R : Type u_1
X : Type u_2
Y : Type ?u.18385
Z : Type ?u.18388
ι : Type ?u.18391
E : ι → Type ?u.18396
inst✝¹¹ : CommRing 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)
⊢ IsLinearMap R fun x => x - 0
Theorem: IsAffineMap.IsAffineMap_id
Proof state before:
case is_affine
R : Type u_1
X : Type u_2
Y : Type ?u.18385
Z : Type ?u.18388
ι : Type ?u.18391
E : ι → Type ?u.18396
inst✝¹¹ : CommRing 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)
⊢ IsLinearMap R fun x => x - 0
Tactic:
simp
Proof state after:
case is_affine
R : Type u_1
X : Type u_2
Y : Type ?u.18385
Z : Type ?u.18388
ι : Type ?u.18391
E : ι → Type ?u.18396
inst✝¹¹ : CommRing 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)
⊢ IsLinearMap R fun x => x
Theorem: IsAffineMap.IsAffineMap_id
Proof state before:
case is_affine
R : Type u_1
X : Type u_2
Y : Type ?u.18385
Z : Type ?u.18388
ι : Type ?u.18391
E : ι → Type ?u.18396
inst✝¹¹ : CommRing 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)
⊢ IsLinearMap R fun x => x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: IsAffineMap.IsAffineMap_const
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.23389
ι : Type ?u.23392
E : ι → Type ?u.23397
inst✝¹¹ : CommRing 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)
y : Y
⊢ IsAffineMap R fun x => y
Tactic:
constructor
Proof state after:
case is_affine
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.23389
ι : Type ?u.23392
E : ι → Type ?u.23397
inst✝¹¹ : CommRing 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)
y : Y
⊢ IsLinearMap R fun x => y - y
Theorem: IsAffineMap.IsAffineMap_const
Proof state before:
case is_affine
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.23389
ι : Type ?u.23392
E : ι → Type ?u.23397
inst✝¹¹ : CommRing 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)
y : Y
⊢ IsLinearMap R fun x => y - y
Tactic:
simp
Proof state after:
case is_affine
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.23389
ι : Type ?u.23392
E : ι → Type ?u.23397
inst✝¹¹ : CommRing 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)
y : Y
⊢ IsLinearMap R fun x => 0
Theorem: IsAffineMap.IsAffineMap_const
Proof state before:
case is_affine
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.23389
ι : Type ?u.23392
E : ι → Type ?u.23397
inst✝¹¹ : CommRing 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)
y : Y
⊢ IsLinearMap R fun x => 0
Tactic:
apply IsLinearMap.isLinearMap_const_zero
Proof state after:
no goals
Theorem: IsAffineMap.IsAffineMap_comp
Proof state before:
R : Type u_1
X : Type u_4
Y : Type u_2
Z : Type u_3
ι : Type ?u.27997
E : ι → Type ?u.28002
inst✝¹¹ : CommRing 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)
f : Y → Z
g : X → Y
hf : IsAffineMap R f
hg : IsAffineMap R g
⊢ IsAffineMap R fun x => f (g x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsAffineMap.IsAffineMap_apply
Proof state before:
R : Type u_1
X : Type ?u.31360
Y : Type ?u.31363
Z : Type ?u.31366
ι : Type u_2
E : ι → Type u_3
inst✝¹¹ : CommRing 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)
i : ι
⊢ IsAffineMap R fun f => f i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsAffineMap.IsAffineMap_pi
Proof state before:
R : Type u_1
X : Type u_2
Y : Type ?u.36139
Z : Type ?u.36142
ι : Type u_4
E : ι → Type u_3
inst✝¹¹ : CommRing 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)
f : X → (i : ι) → E i
hf : ∀ (i : ι), IsAffineMap R fun x => f x i
⊢ IsAffineMap R fun x i => f x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IndexType.sum.arg_f.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.102849
ι : Type u_4
E : ι → Type ?u.102857
inst✝¹¹ : CommRing 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)
f : X → ι → Y
hf : ∀ (i : ι), IsAffineMap R fun x => f x i
⊢ IsAffineMap R fun x =>  ∑ i, f x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: ite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
⊢ IsAffineMap 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.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h✝ : ¬c
⊢ IsAffineMap 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.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h✝ : c
⊢ IsAffineMap R fun x => if c then t x else e x
Theorem: ite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : c
⊢ IsAffineMap 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.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : ¬c
⊢ IsAffineMap 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.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : c
⊢ IsAffineMap 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.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : c
⊢ IsAffineMap R fun x => t x
Theorem: ite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : c
⊢ IsAffineMap R fun x => t x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : ¬c
⊢ IsAffineMap 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.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : ¬c
⊢ IsAffineMap R fun x => e x
Theorem: ite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.107591
ι : Type ?u.107594
E : ι → Type ?u.107599
inst✝¹¹ : CommRing 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 : IsAffineMap R t
he : IsAffineMap R e
h : ¬c
⊢ IsAffineMap R fun x => e x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: dite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
⊢ IsAffineMap 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.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h✝ : ¬c
⊢ IsAffineMap 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.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h✝ : c
⊢ IsAffineMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Theorem: dite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : c
⊢ IsAffineMap 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.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : ¬c
⊢ IsAffineMap 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.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : c
⊢ IsAffineMap 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.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : c
⊢ IsAffineMap R fun x => t ⋯ x
Theorem: dite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : c
⊢ IsAffineMap R fun x => t ⋯ x
Tactic:
apply ht
Proof state after:
no goals
Theorem: dite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : ¬c
⊢ IsAffineMap 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.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : ¬c
⊢ IsAffineMap R fun x => e ⋯ x
Theorem: dite.arg_te.IsAffineMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.111146
ι : Type ?u.111149
E : ι → Type ?u.111154
inst✝¹¹ : CommRing 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), IsAffineMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsAffineMap R (e p)
h : ¬c
⊢ IsAffineMap R fun x => e ⋯ x
Tactic:
apply he
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.IsAffineMap_rule
Proof state before:
R : Type ?u.118169
X✝ : Type ?u.118172
Y✝ : Type ?u.118175
Z✝ : Type ?u.118178
ι : Type ?u.118181
E : ι → Type ?u.118186
inst✝²⁴ : CommRing 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)
K : Type u_1
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.121438
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.121525
inst✝ : FinVec IZ K Z
i : IX
⊢ IsAffineMap K fun x => ℼ i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DualBasis.dualProj.arg_x.IsAffineMap_rule
Proof state before:
R : Type ?u.122715
X✝ : Type ?u.122718
Y✝ : Type ?u.122721
Z✝ : Type ?u.122724
ι : Type ?u.122727
E : ι → Type ?u.122732
inst✝²⁴ : CommRing 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)
K : Type u_1
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.125984
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.126071
inst✝ : FinVec IZ K Z
i : IX
⊢ IsAffineMap K fun x => ℼ' i x
Tactic:
sorry_proof
Proof state after:
no goals