internlm/Lean-Github huggingface dataset:
Theorem: circleParam.arg_θ.jacobian_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let dg := ∂ (θ:=x), (cos θ, sin θ);
      let dg' := semiAdjoint R dg;
      sqrt (det R (dg' ∘ dg))) =
    1
Tactic:
autodiff
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      let dg' := semiAdjoint R fun dx => (dx * s, dx * c);
      sqrt ((dg' ∘ fun dx => (dx * s, dx * c)) 1)) =
    1
Theorem: circleParam.arg_θ.jacobian_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      let dg' := semiAdjoint R fun dx => (dx * s, dx * c);
      sqrt ((dg' ∘ fun dx => (dx * s, dx * c)) 1)) =
    1
Tactic:
autodiff
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      sqrt
        (((fun yz =>
              let x₁ := s * yz.1;
              let x₂ := c * yz.2;
              x₁ + x₂) ∘
            fun dx => (dx * s, dx * c))
          1)) =
    1
Theorem: circleParam.arg_θ.jacobian_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      sqrt
        (((fun yz =>
              let x₁ := s * yz.1;
              let x₂ := c * yz.2;
              x₁ + x₂) ∘
            fun dx => (dx * s, dx * c))
          1)) =
    1
Tactic:
simp
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x => sqrt (sin x * sin x + cos x * cos x)) = 1
Theorem: circleParam.arg_θ.jacobian_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x => sqrt (sin x * sin x + cos x * cos x)) = 1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: circle_parametric_inverse_polar
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
⊢ ParametricInverseAt (fun x => x.1 ^ 2 + x.2 ^ 2 - r ^ 2 - 0) 0 (fun x θ s => s • circleParam θ) (fun x x => r)
    fun x => Ico 0 (2 * RealScalar.pi)
Tactic:
simp[ParametricInverseAt]
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
⊢ ∀ (x₁ : R), 0 ≤ x₁ → x₁ < 2 * RealScalar.pi → (r * (circleParam x₁).1) ^ 2 + (r * (circleParam x₁).2) ^ 2 - r ^ 2 = 0
Theorem: circle_parametric_inverse_polar
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
⊢ ∀ (x₁ : R), 0 ≤ x₁ → x₁ < 2 * RealScalar.pi → (r * (circleParam x₁).1) ^ 2 + (r * (circleParam x₁).2) ^ 2 - r ^ 2 = 0
Tactic:
intros
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
x₁✝ : R
a✝¹ : 0 ≤ x₁✝
a✝ : x₁✝ < 2 * RealScalar.pi
⊢ (r * (circleParam x₁✝).1) ^ 2 + (r * (circleParam x₁✝).2) ^ 2 - r ^ 2 = 0
Theorem: circle_parametric_inverse_polar
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
x₁✝ : R
a✝¹ : 0 ≤ x₁✝
a✝ : x₁✝ < 2 * RealScalar.pi
⊢ (r * (circleParam x₁✝).1) ^ 2 + (r * (circleParam x₁✝).2) ^ 2 - r ^ 2 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun_comp'
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ invFun f (f x) = x
Tactic:
suffices (f.invFun ∘ f) x = x by assumption
Proof state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ (invFun f ∘ f) x = x
Theorem: Function.invFun_comp'
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ (invFun f ∘ f) x = x
Tactic:
rw[Function.invFun_comp hf]
Proof state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ id x = x
Theorem: Function.invFun_comp'
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ id x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.invFun_comp'
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
this : (invFun f ∘ f) x = x
⊢ invFun f (f x) = x
Tactic:
assumption
Proof state after:
no goals
Theorem: Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule_simple
Proof state before:
X✝ : Type ?u.362
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.368
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.374
inst✝⁵ : Nonempty Z✝
X : Type u_1
inst✝⁴ : Nonempty X
X₁ : Type ?u.386
inst✝³ : Nonempty X₁
X₂ : Type ?u.392
inst✝² : Nonempty X₂
Y : Type u_2
inst✝¹ : Nonempty Y
Z : Type ?u.404
inst✝ : Nonempty Z
⊢ Bijective fun xy => (xy.1, xy.2)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule_simple'
Proof state before:
X✝ : Type ?u.475
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.481
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.487
inst✝⁵ : Nonempty Z✝
X : Type u_1
inst✝⁴ : Nonempty X
X₁ : Type ?u.499
inst✝³ : Nonempty X₁
X₂ : Type ?u.505
inst✝² : Nonempty X₂
Y : Type u_2
inst✝¹ : Nonempty Y
Z : Type ?u.517
inst✝ : Nonempty Z
⊢ Bijective fun xy => (xy.2, xy.1)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule
Proof state before:
X✝ : Type ?u.593
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.599
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.605
inst✝⁵ : Nonempty Z✝
X : Type u_5
inst✝⁴ : Nonempty X
X₁ : Type u_1
inst✝³ : Nonempty X₁
X₂ : Type u_3
inst✝² : Nonempty X₂
Y : Type u_2
inst✝¹ : Nonempty Y
Z : Type u_4
inst✝ : Nonempty Z
f : X₁ → Y
g : X₂ → Z
p₁ : X → X₁
p₂ : X → X₂
hf : Bijective f
hg : Bijective g
hp : Bijective fun x => (p₁ x, p₂ x)
⊢ Bijective fun x => (f (p₁ x), g (p₂ x))
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Neg.neg.arg_a0.Bijective_rule
Proof state before:
X✝ : Type ?u.785
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.791
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.797
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.809
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.815
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.827
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
hf : Bijective f
⊢ Bijective fun x => -f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Inv.inv.arg_a0.Bijective_rule_group
Proof state before:
X✝ : Type ?u.1145
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1151
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1157
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.1169
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.1175
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1187
inst✝¹ : Nonempty Z
inst✝ : Group Y
f : X → Y
hf : Bijective f
⊢ Bijective fun x => (f x)⁻¹
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Inv.inv.arg_a0.Bijective_rule_field
Proof state before:
X✝ : Type ?u.1349
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1355
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1361
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.1373
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.1379
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1391
inst✝¹ : Nonempty Z
inst✝ : Field Y
f : X → Y
hf : Bijective f
hf' : ∀ (x : X), f x ≠ 0
⊢ Bijective fun x => (f x)⁻¹
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HAdd.hAdd.arg_a0.Bijective_rule
Proof state before:
X✝ : Type ?u.1550
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1556
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1562
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.1574
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.1580
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1592
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
y : Y
hf : Bijective f
⊢ Bijective fun x => f x + y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HAdd.hAdd.arg_a1.Bijective_rule
Proof state before:
X✝ : Type ?u.2144
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.2150
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.2156
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.2168
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.2174
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.2186
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
y : Y
f : X → Y
hf : Bijective f
⊢ Bijective fun x => y + f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HSub.hSub.arg_a0.Bijective_rule
Proof state before:
X✝ : Type ?u.2738
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.2744
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.2750
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.2762
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.2768
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.2780
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
y : Y
hf : Bijective f
⊢ Bijective fun x => f x - y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HSub.hSub.arg_a1.Bijective_rule
Proof state before:
X✝ : Type ?u.2982
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.2988
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.2994
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.3006
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.3012
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.3024
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
y : Y
f : X → Y
hf : Bijective f
⊢ Bijective fun x => y - f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HMul.hMul.arg_a0.Bijective_rule_group
Proof state before:
X✝ : Type ?u.3226
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.3232
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.3238
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.3250
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.3256
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.3268
inst✝¹ : Nonempty Z
inst✝ : Group Y
f : X → Y
y : Y
hf : Bijective f
⊢ Bijective fun x => f x * y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HMul.hMul.arg_a1.Bijective_rule_group
Proof state before:
X✝ : Type ?u.3828
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.3834
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.3840
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.3852
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.3858
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.3870
inst✝¹ : Nonempty Z
inst✝ : Group Y
y : Y
f : X → Y
hf : Bijective f
⊢ Bijective fun x => y * f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HMul.hMul.arg_a0.Bijective_rule_field
Proof state before:
X✝ : Type ?u.4430
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.4436
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.4442
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.4454
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.4460
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.4472
inst✝¹ : Nonempty Z
inst✝ : Field Y
f : X → Y
y : Y
hf : Bijective f
hy : y ≠ 0
⊢ Bijective fun x => f x * y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HMul.hMul.arg_a1.Bijective_rule_field
Proof state before:
X✝ : Type ?u.4680
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.4686
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.4692
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.4704
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.4710
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.4722
inst✝¹ : Nonempty Z
inst✝ : Field Y
y : Y
f : X → Y
hf : Bijective f
hy : y ≠ 0
⊢ Bijective fun x => y * f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HSMul.hSMul.arg_a1.Bijective_rule_group
Proof state before:
X✝ : Type ?u.4930
inst✝⁹ : Nonempty X✝
Y✝ : Type ?u.4936
inst✝⁸ : Nonempty Y✝
Z✝ : Type ?u.4942
inst✝⁷ : Nonempty Z✝
X : Type u_3
inst✝⁶ : Nonempty X
X₁ : Type ?u.4954
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.4960
inst✝⁴ : Nonempty X₂
Y : Type u_2
inst✝³ : Nonempty Y
Z : Type ?u.4972
inst✝² : Nonempty Z
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G Y
g : G
f : X → Y
hf : Bijective f
⊢ Bijective fun x => g • f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HSMul.hSMul.arg_a1.Bijective_rule_field
Proof state before:
X✝ : Type ?u.5742
inst✝⁹ : Nonempty X✝
Y✝ : Type ?u.5748
inst✝⁸ : Nonempty Y✝
Z✝ : Type ?u.5754
inst✝⁷ : Nonempty Z✝
X : Type u_3
inst✝⁶ : Nonempty X
X₁ : Type ?u.5766
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.5772
inst✝⁴ : Nonempty X₂
Y : Type u_2
inst✝³ : Nonempty Y
Z : Type ?u.5784
inst✝² : Nonempty Z
R : Type u_1
inst✝¹ : Field R
inst✝ : MulAction R Y
r : R
f : X → Y
hf : Bijective f
hr : r ≠ 0
⊢ Bijective fun x => r • f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HVAdd.hVAdd.arg_a1.Bijective_rule_group
Proof state before:
X✝ : Type ?u.6453
inst✝⁹ : Nonempty X✝
Y✝ : Type ?u.6459
inst✝⁸ : Nonempty Y✝
Z✝ : Type ?u.6465
inst✝⁷ : Nonempty Z✝
X : Type u_3
inst✝⁶ : Nonempty X
X₁ : Type ?u.6477
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.6483
inst✝⁴ : Nonempty X₂
Y : Type u_2
inst✝³ : Nonempty Y
Z : Type ?u.6495
inst✝² : Nonempty Z
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : AddAction G Y
g : G
f : X → Y
hf : Bijective f
⊢ Bijective fun x => g +ᵥ f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HDiv.hDiv.arg_a0.Bijective_rule_group
Proof state before:
X✝ : Type ?u.6832
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.6838
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.6844
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.6856
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.6862
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.6874
inst✝¹ : Nonempty Z
inst✝ : Group Y
f : X → Y
y : Y
hf : Bijective f
⊢ Bijective fun x => f x / y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.HDiv.hDiv.arg_a0.Bijective_rule_field
Proof state before:
X✝ : Type ?u.7096
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.7102
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.7108
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.7120
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.7126
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.7138
inst✝¹ : Nonempty Z
inst✝ : Field Y
f : X → Y
y : Y
hf : Bijective f
hy : y ≠ 0
⊢ Bijective fun x => f x / y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Equiv.toFun.arg_a0.Bijective_rule
Proof state before:
X✝ : Type ?u.7310
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.7316
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.7322
inst✝⁵ : Nonempty Z✝
X : Type u_3
inst✝⁴ : Nonempty X
X₁ : Type ?u.7334
inst✝³ : Nonempty X₁
X₂ : Type ?u.7340
inst✝² : Nonempty X₂
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Y
hf : Bijective g
⊢ Bijective fun x => f (g x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.Bijective.Equiv.invFun.arg_a0.Bijective_rule
Proof state before:
X✝ : Type ?u.7486
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.7492
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.7498
inst✝⁵ : Nonempty Z✝
X : Type u_3
inst✝⁴ : Nonempty X
X₁ : Type ?u.7510
inst✝³ : Nonempty X₁
X₂ : Type ?u.7516
inst✝² : Nonempty X₂
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Z
hf : Bijective g
⊢ Bijective fun x => f.invFun (g x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Scalar.sin.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fwdDeriv C fun w => sin (x w)) = fun w dw =>
    let xdx := fwdDeriv C x w dw;
    let s := sin xdx.1;
    let c := cos xdx.1;
    (s, xdx.2 * c)
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => sin (x w)) x_1, cderiv C (fun w => sin (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let s := sin xdx.1;
    let c := cos xdx.1;
    (s, xdx.2 * c)
Theorem: SciLean.Scalar.sin.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => sin (x w)) x_1, cderiv C (fun w => sin (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let s := sin xdx.1;
    let c := cos xdx.1;
    (s, xdx.2 * c)
Tactic:
fun_trans
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (sin (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * cos (fwdDeriv C (fun w => x w) x_1 dx).1)) =
    fun w dw => (sin (x w), cderiv C x w dw * cos (x w))
Theorem: SciLean.Scalar.sin.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (sin (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * cos (fwdDeriv C (fun w => x w) x_1 dx).1)) =
    fun w dw => (sin (x w), cderiv C x w dw * cos (x w))
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Scalar.sin.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ HasAdjDiff C fun u => sin (x u)
Tactic:
intro x
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => sin (x✝ u)) x
Theorem: SciLean.Scalar.sin.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => sin (x✝ u)) x
Tactic:
constructor
Proof state after:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => sin (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => sin (x✝ u)) x)
Theorem: SciLean.Scalar.sin.arg_x.HasAdjDiff_rule
Proof state before:
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => sin (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => sin (x✝ u)) x)
Tactic:
fun_prop
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => sin (x✝ u)) x)
Theorem: SciLean.Scalar.sin.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => sin (x✝ u)) x)
Tactic:
fun_trans [fwdDeriv]
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * cos (x✝ x)
Theorem: SciLean.Scalar.sin.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * cos (x✝ x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.sin.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.5074
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (revDeriv C fun u => sin (x u)) = fun u =>
    let xdx := revDeriv C x u;
    (sin xdx.1, fun dy => xdx.2 ((starRingEnd C) (cos xdx.1) * dy))
Tactic:
unfold revDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.5074
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => sin (x u)) x_1, semiAdjoint C (cderiv C (fun u => sin (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (sin xdx.1, fun dy => xdx.2 ((starRingEnd C) (cos xdx.1) * dy))
Theorem: SciLean.Scalar.sin.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.5074
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => sin (x u)) x_1, semiAdjoint C (cderiv C (fun u => sin (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (sin xdx.1, fun dy => xdx.2 ((starRingEnd C) (cos xdx.1) * dy))
Tactic:
fun_trans only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Scalar.cos.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fwdDeriv C fun w => cos (x w)) = fun w dw =>
    let xdx := fwdDeriv C x w dw;
    let s := sin xdx.1;
    let c := cos xdx.1;
    (c, xdx.2 * -s)
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => cos (x w)) x_1, cderiv C (fun w => cos (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let s := sin xdx.1;
    let c := cos xdx.1;
    (c, xdx.2 * -s)
Theorem: SciLean.Scalar.cos.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => cos (x w)) x_1, cderiv C (fun w => cos (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let s := sin xdx.1;
    let c := cos xdx.1;
    (c, xdx.2 * -s)
Tactic:
fun_trans
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (cos (x x_1), -((fwdDeriv C (fun w => x w) x_1 dx).2 * sin (fwdDeriv C (fun w => x w) x_1 dx).1))) =
    fun w dw => (cos (x w), -(cderiv C x w dw * sin (x w)))
Theorem: SciLean.Scalar.cos.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (cos (x x_1), -((fwdDeriv C (fun w => x w) x_1 dx).2 * sin (fwdDeriv C (fun w => x w) x_1 dx).1))) =
    fun w dw => (cos (x w), -(cderiv C x w dw * sin (x w)))
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Scalar.cos.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ HasAdjDiff C fun u => cos (x u)
Tactic:
intro x
Proof state after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.11071
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => cos (x✝ u)) x