internlm/Lean-Github huggingface dataset:
Theorem: SciLean.comp_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.45874
E : κ → Type ?u.45879
ME : κ → Type ?u.45884
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : Y → Z
⊢ (broadcast tag R ι fun x => f (g x)) = fun mx => broadcast tag R ι f (broadcast tag R ι g mx)
Tactic:
unfold broadcast
Proof state after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.45874
E : κ → Type ?u.45879
ME : κ → Type ?u.45884
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : Y → Z
⊢ (fun mx =>
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f (g x)) ((BroadcastType.equiv tag) mx i)) =
    fun mx =>
    (LinearEquiv.symm (BroadcastType.equiv tag)) fun i =>
      f
        ((BroadcastType.equiv tag)
          ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)) i)
Theorem: SciLean.comp_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.45874
E : κ → Type ?u.45879
ME : κ → Type ?u.45884
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : Y → Z
⊢ (fun mx =>
      (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => f (g x)) ((BroadcastType.equiv tag) mx i)) =
    fun mx =>
    (LinearEquiv.symm (BroadcastType.equiv tag)) fun i =>
      f
        ((BroadcastType.equiv tag)
          ((LinearEquiv.symm (BroadcastType.equiv tag)) fun i => g ((BroadcastType.equiv tag) mx i)) i)
Tactic:
simp[broadcast]
Proof state after:
no goals
Theorem: SciLean.let_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (broadcast tag R ι fun x =>
      let y := g x;
      f x y) =
    fun mx =>
    let my := broadcast tag R ι g mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Tactic:
rw[show (fun x => let y := g x; f x y)
        =
        fun x => (fun (xy : X×Y) => f xy.1 xy.2) ((fun x' => (x', g x')) x) by rfl]
Proof state after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (broadcast tag R ι fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) = fun mx =>
    let my := broadcast tag R ι g mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Theorem: SciLean.let_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (broadcast tag R ι fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) = fun mx =>
    let my := broadcast tag R ι g mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Tactic:
rw[comp_rule _ _]
Proof state after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (broadcast tag R ι fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) = fun mx =>
    let my := (fun mx => broadcast tag R ι g (broadcast tag R ι (fun x => x) mx)) mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Theorem: SciLean.let_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (broadcast tag R ι fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) = fun mx =>
    let my := (fun mx => broadcast tag R ι g (broadcast tag R ι (fun x => x) mx)) mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Tactic:
funext mx
Proof state after:
case h
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
mx : MX
⊢ broadcast tag R ι (fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) mx =
    let my := (fun mx => broadcast tag R ι g (broadcast tag R ι (fun x => x) mx)) mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Theorem: SciLean.let_rule
Proof state before:
case h
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
mx : MX
⊢ broadcast tag R ι (fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)) mx =
    let my := (fun mx => broadcast tag R ι g (broadcast tag R ι (fun x => x) mx)) mx;
    let mz := broadcast tag R ι (fun xy => f xy.1 xy.2) (mx, my);
    mz
Tactic:
simp[broadcast, BroadcastType.equiv]
Proof state after:
no goals
Theorem: SciLean.let_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_7
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type u_6
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_8
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_2
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.63075
E : κ → Type ?u.63080
ME : κ → Type ?u.63085
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Y → Z
⊢ (fun x =>
      let y := g x;
      f x y) =
    fun x => (fun xy => f xy.1 xy.2) ((fun x' => (x', g x')) x)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.apply_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
j : κ
⊢ (broadcast tag R ι fun x => x j) = fun mx => mx j
Tactic:
unfold broadcast
Proof state after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
j : κ
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x j) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx j
Theorem: SciLean.apply_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type ?u.90750
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.91543
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.92277
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type ?u.93011
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.93809
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.94607
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_1
E : κ → Type u_5
ME : κ → Type u_2
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
j : κ
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x j) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx j
Tactic:
simp[broadcastIntro, BroadcastType.equiv]
Proof state after:
no goals
Theorem: SciLean.pi_rule
Proof state before:
tag : Lean.Name
R : Type u_4
inst✝²⁰ : Ring R
ι : Type u_5
X : Type u_6
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.109410
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.110144
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.111676
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.112474
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_2
E : κ → Type u_7
ME : κ → Type u_3
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
f : X → (j : κ) → E j
⊢ (broadcast tag R ι fun x j => f x j) = fun mx j => broadcast tag R ι (fun x => f x j) mx
Tactic:
funext mx j
Proof state after:
case h.h
tag : Lean.Name
R : Type u_4
inst✝²⁰ : Ring R
ι : Type u_5
X : Type u_6
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.109410
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.110144
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.111676
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.112474
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_2
E : κ → Type u_7
ME : κ → Type u_3
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
f : X → (j : κ) → E j
mx : MX
j : κ
⊢ broadcast tag R ι (fun x j => f x j) mx j = broadcast tag R ι (fun x => f x j) mx
Theorem: SciLean.pi_rule
Proof state before:
case h.h
tag : Lean.Name
R : Type u_4
inst✝²⁰ : Ring R
ι : Type u_5
X : Type u_6
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.109410
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.110144
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.111676
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.112474
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type u_2
E : κ → Type u_7
ME : κ → Type u_3
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
f : X → (j : κ) → E j
mx : MX
j : κ
⊢ broadcast tag R ι (fun x j => f x j) mx j = broadcast tag R ι (fun x => f x j) mx
Tactic:
simp[broadcast,BroadcastType.equiv]
Proof state after:
no goals
Theorem: Prod.mk.arg_fstsnd.broadcast_rule
Proof state before:
R : Type u_4
inst✝²³ : Ring R
X : Type u_6
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_8
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_7
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_5
tag : Lean.Name
MR : Type ?u.140645
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_3
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.144585
E : κ → Type ?u.144590
ME : κ → Type ?u.144595
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Z
⊢ (broadcast tag R ι fun x => (g x, f x)) = fun mx => (broadcast tag R ι g mx, broadcast tag R ι f mx)
Tactic:
funext mx
Proof state after:
case h
R : Type u_4
inst✝²³ : Ring R
X : Type u_6
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_8
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_7
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_5
tag : Lean.Name
MR : Type ?u.140645
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_3
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.144585
E : κ → Type ?u.144590
ME : κ → Type ?u.144595
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Z
mx : MX
⊢ broadcast tag R ι (fun x => (g x, f x)) mx = (broadcast tag R ι g mx, broadcast tag R ι f mx)
Theorem: Prod.mk.arg_fstsnd.broadcast_rule
Proof state before:
case h
R : Type u_4
inst✝²³ : Ring R
X : Type u_6
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_8
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_7
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_5
tag : Lean.Name
MR : Type ?u.140645
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_3
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.144585
E : κ → Type ?u.144590
ME : κ → Type ?u.144595
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
g : X → Y
f : X → Z
mx : MX
⊢ broadcast tag R ι (fun x => (g x, f x)) mx = (broadcast tag R ι g mx, broadcast tag R ι f mx)
Tactic:
simp[broadcast, BroadcastType.equiv]
Proof state after:
no goals
Theorem: Prod.fst.arg_self.broadcast_rule
Proof state before:
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.166233
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_4
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_8
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.170173
E : κ → Type ?u.170178
ME : κ → Type ?u.170183
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
f : X → Y × Z
⊢ (broadcast tag R ι fun x => (f x).1) = fun mx => (broadcast tag R ι f mx).1
Tactic:
funext mx
Proof state after:
case h
R : Type u_5
inst✝²³ : Ring R
X : Type u_7
inst✝²² : AddCommGroup X
inst✝²¹ : Module R X
Y : Type u_1
inst✝²⁰ : AddCommGroup Y
inst✝¹⁹ : Module R Y
Z : Type u_2
inst✝¹⁸ : AddCommGroup Z
inst✝¹⁷ : Module R Z
ι : Type u_6
tag : Lean.Name
MR : Type ?u.166233
inst✝¹⁶ : AddCommGroup MR
inst✝¹⁵ : Module R MR
inst✝¹⁴ : BroadcastType tag R ι R MR
MX : Type u_3
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_4
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type u_8
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.170173
E : κ → Type ?u.170178
ME : κ → Type ?u.170183
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
f : X → Y × Z
mx : MX
⊢ broadcast tag R ι (fun x => (f x).1) mx = (broadcast tag R ι f mx).1