harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
    (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i)

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x <<< (w - r)).getLsbD i = false

Tactic:
simp only [getLsbD_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
  Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ i < w → w - r ≤ i → x.getLsbD (i - (w - r)) = false

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ i < w → w - r ≤ i → x.getLsbD (i - (w - r)) = false

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i)

Tactic:
rw [rotateRightAux, getLsbD_or, getLsbD_ushiftRight]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x.getLsbD (r + i) || (x <<< (w - r)).getLsbD i) = x.getLsbD (r + i)

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x.getLsbD (r + i) || (x <<< (w - r)).getLsbD i) = x.getLsbD (r + i)

Tactic:
suffices (x <<< (w - r)).getLsbD i = false by
  simp only [this, Bool.or_false]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
⊢ (x <<< (w - r)).getLsbD i = false

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < w - r
this : (x <<< (w - r)).getLsbD i = false
⊢ (x.getLsbD (r + i) || (x <<< (w - r)).getLsbD i) = x.getLsbD (r + i)

Tactic:
simp only [this, Bool.or_false]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
/-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`. -/
lemma tendsto_setIntegral_of_L1' {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G}
    {l : Filter ι}
    (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0))
    (s : Set α) :
    Tendsto (fun i ↦ ∫ x in s, F i x ∂μ) l (𝓝 (∫ x in s, f x ∂μ))

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
exact hF

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))

Tactic:
refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitUncurryIsoLimitCompLim_hom_π_π {j} {k} :
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ limit.lift (F ⋙ lim) (coneOfConeUncurry (fun j => limit.isLimit (F.obj j)) (limit.cone (uncurry.obj F))) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (uncurry.obj F) (j, k)

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k = limit.π (uncurry.obj F) (j, k)

Tactic:
dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ limit.lift (F ⋙ lim) (coneOfConeUncurry (fun j => limit.isLimit (F.obj j)) (limit.cone (uncurry.obj F))) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (uncurry.obj F) (j, k)
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem leftAdjointUniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (adj3 : F'' ⊣ G) (x : C) :
    (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
      (leftAdjointUniq adj1 adj3).hom.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
    ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x

Tactic:
rw [← leftAdjointUniq_trans adj1 adj2 adj3]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
    ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
    UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / (n : α → ℝ)) p μ

Proof state:
case h.e'_6.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
⊢ (∑ i ∈ Finset.range n, f i) / ↑n = (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i

Tactic:
ext x

Result:
case h.e'_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
x : α
⊢ ((∑ i ∈ Finset.range n, f i) / ↑n) x = ((↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) x

Proof state:
case h.e'_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
x : α
⊢ ((∑ i ∈ Finset.range n, f i) / ↑n) x = ((↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) x

Tactic:
simp [div_eq_inv_mul]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
⊢ UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / ↑n) p μ

Tactic:
convert uniformIntegrable_average hp hf using 2 with n

Result:
case h.e'_6.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
⊢ (∑ i ∈ Finset.range n, f i) / ↑n = (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[simp]
lemma curry'_id (X : C) [Closed X] : curry' (𝟙 X) = id X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry ((ρ_ X).hom ≫ 𝟙 X) = id X

Tactic:
rw [Category.comp_id]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry' (𝟙 X) = id X

Tactic:
dsimp [curry']

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry ((ρ_ X).hom ≫ 𝟙 X) = id X
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem congr_zpow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) :
    congr f g ^ n = congr (f ^ n) (g ^ n)

Proof state:
case ofNat
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)

Tactic:
exact congr_pow _ _ _

Result:
no goals

Proof state:
case negSucc
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Tactic:
exact congr_symm _ _

Result:
no goals

Proof state:
case negSucc
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)

Tactic:
simp_rw [zpow_negSucc, congr_pow]

Result:
case negSucc
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℤ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
cases n with
| ofNat n => exact congr_pow _ _ _
| negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
    {X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
    IsIso (E.hom.app X)

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso (E.hom.app X)

Tactic:
simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal

Result:
no goals
-- Mathlib/Data/Tree/Basic.lean
theorem comp_map {β γ : Type*} (f : α → β) (g : β → γ) (t : Tree α) :
    t.map (g ∘ f) = (t.map f).map g

Proof state:
case node
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ map (g ∘ f) (node v l r) = map g (map f (node v l r))

Tactic:
rw [map, map, map, hl, hr, Function.comp_apply]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
⊢ map (g ∘ f) nil = map g (map f nil)

Tactic:
rw [map, map, map]

Result:
no goals

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : Tree α
⊢ map (g ∘ f) t = map g (map f t)

Tactic:
induction t with
| nil => rw [map, map, map]
| node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsRadical.inf (hI : IsRadical I) (hJ : IsRadical J) : IsRadical (I ⊓ J)

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J

Tactic:
exact inf_le_inf hI hJ

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).IsRadical

Tactic:
rw [IsRadical, radical_inf]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_push_self {a : α} {xs : Array α} : xs ≠ xs.push a

Proof state:
α : Type u_1
a : α
xs : Array α
⊢ xs ≠ xs.push a

Tactic:
rw [ne_eq, eq_comm]

Result:
α : Type u_1
a : α
xs : Array α
⊢ ¬xs.push a = xs

Proof state:
α : Type u_1
a : α
xs : Array α
⊢ ¬xs.push a = xs

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Category/Quiv.lean
lemma hom_map_inv_map_of_iso {V W : Quiv} (e : V ≅ W) {X Y : W} (f : X ⟶ Y) :
    e.hom.map (e.inv.map f) = Quiver.homOfEq f (by simp) (by simp)

Proof state:
V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ Y = e.hom.obj (e.inv.obj Y)

Tactic:
simp

Result:
no goals

Proof state:
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯

Tactic:
exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

Result:
no goals

Proof state:
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
rw [← Prefunctor.comp_map]

Result:
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯

Proof state:
V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ X = e.hom.obj (e.inv.obj X)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
lemma traceForm_apply_eq_zero_of_mem_lcs_of_mem_center {x y : L}
    (hx : x ∈ lowerCentralSeries R L L 1) (hy : y ∈ LieAlgebra.center R L) :
    traceForm R L M x y = 0

Proof state:
case hy
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ y ∈ LieSubmodule.ucs 1 ⊥

Tactic:
simpa using hy

Result:
no goals

Proof state:
case hx
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ x ∈ ⊤.lcs L 1

Tactic:
simpa using hx

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ ((traceForm R L M) x) y = 0

Tactic:
apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1

Result:
case hx
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ x ∈ ⊤.lcs L 1

case hy
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ y ∈ LieSubmodule.ucs 1 ⊥
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem degree_le_zero_iff_eq_one (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p.degree ≤ 0 ↔ p = 1

Tactic:
rw [← hp.natDegree_eq_zero_iff_eq_one, natDegree_eq_zero_iff_degree_le_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_clm_apply (hc : DifferentiableWithinAt 𝕜 c s x)
    (hu : DifferentiableWithinAt 𝕜 u s x) :
    derivWithin (fun y => (c y) (u y)) s x = derivWithin c s x (u x) + c x (derivWithin u s x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
⊢ derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Proof state:
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Tactic:
exact (hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
protected lemma IsDiameter.sbtw (h : s.IsDiameter p₁ p₂) (hr : s.radius ≠ 0) :
    Sbtw ℝ p₁ s.center p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
exact sbtw_midpoint_of_ne _ (h.left_ne_right_iff_radius_ne_zero.2 hr)

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mul_one : M * 1 = M

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ span R (↑M * {1}) = M

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ M * 1 = M

Tactic:
conv_lhs => rw [one_eq_span, ← span_eq M]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ span R ↑M * span R {1} = M

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ span R ↑M * span R {1} = M

Tactic:
rw [span_mul_span]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
⊢ span R (↑M * {1}) = M
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_neg_I : log (-I) = -(π / 2) * I

Proof state:
⊢ log (-I) = -(↑π / 2) * I

Tactic:
simp [log]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_add_of_omega0_le {o} (h : ω ≤ o) (n : ℕ) : n + o = o

Proof state:
o : Ordinal.{u_1}
h : ω ≤ o
n : ℕ
⊢ ↑n + o = o

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]

Result:
no goals