harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/NhdsSet.lean
theorem hasBasis_nhdsSet_Iic_Iio (a : α) [h : Nonempty (Ioi a)] :
    HasBasis (𝓝ˢ (Iic a)) (a < ·) Iio

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩

Result:
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Tactic:
rw [nhdsSet_Iic, mem_sup, mem_principal] at hs

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Proof state:
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Tactic:
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iio

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ ∃ i, a < i ∧ Iio i ⊆ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem inductionOn₃
    {s₃ : Setoid φ}
    {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
    (q₁ : Quotient s₁)
    (q₂ : Quotient s₂)
    (q₃ : Quotient s₃)
    (h : (a : α) → (b : β) → (c : φ) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c))
    : motive q₁ q₂ q₃

Proof state:
case a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂ q₃

Tactic:
induction q₂ using Quotient.ind

Result:
case a.a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝) q₃

Proof state:
case a.a.a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝² : α
a✝¹ : β
a✝ : φ
⊢ motive (Quotient.mk s₁ a✝²) (Quotient.mk s₂ a✝¹) (Quotient.mk s₃ a✝)

Tactic:
apply h

Result:
no goals

Proof state:
case a.a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝) q₃

Tactic:
induction q₃ using Quotient.ind

Result:
case a.a.a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝² : α
a✝¹ : β
a✝ : φ
⊢ motive (Quotient.mk s₁ a✝²) (Quotient.mk s₂ a✝¹) (Quotient.mk s₃ a✝)

Proof state:
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₁ : Quotient s₁
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
⊢ motive q₁ q₂ q₃

Tactic:
induction q₁ using Quotient.ind

Result:
case a
α : Sort uA
β : Sort uB
φ : Sort uC
s₁ : Setoid α
s₂ : Setoid β
s₃ : Setoid φ
motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop
q₂ : Quotient s₂
q₃ : Quotient s₃
h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂ q₃
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_filterM
    {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type}
    (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) :
    monotone (fun x => xs.filterM (f x))

Proof state:
case hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x as => pure as.reverse

Tactic:
apply monotone_const

Result:
no goals

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x => List.filterM (f x) xs

Tactic:
apply monotone_bind

Result:
case hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x => List.filterAuxM (f x) xs []

case hmono₂
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x as => pure as.reverse

Proof state:
case hmono₁
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x => List.filterAuxM (f x) xs []

Tactic:
exact monotone_filterAuxM f xs [] hmono

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem Integrable.add {f g : α →ₘ[μ] β} : Integrable f → Integrable g → Integrable (f + g)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : (mk f hf).Integrable
hgi : (mk g hg).Integrable
⊢ (mk f hf + mk g hg).Integrable

Tactic:
simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : MeasureTheory.Integrable f μ
hgi : MeasureTheory.Integrable g μ
⊢ MeasureTheory.Integrable (f + g) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : MeasureTheory.Integrable f μ
hgi : MeasureTheory.Integrable g μ
⊢ MeasureTheory.Integrable (f + g) μ

Tactic:
exact hfi.add hgi

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α →ₘ[μ] β
⊢ f.Integrable → g.Integrable → (f + g).Integrable

Tactic:
refine induction_on₂ f g fun f hf g hg hfi hgi => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : (mk f hf).Integrable
hgi : (mk g hg).Integrable
⊢ (mk f hf + mk g hg).Integrable
-- Mathlib/Topology/Order/Rolle.lean
theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
    ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Proof state:
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩

Result:
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
x : X
hx : x ∈ Icc a b
⊢ x ∈ {x | (fun x => f c' ≤ f x) x}

Proof state:
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩

Result:
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : a = C
⊢ f C = f a

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_sub (f g : N →ₗ[R] P) : (f - g).lTensor M = f.lTensor M - g.lTensor M

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ lTensor M (f - g) = lTensor M f - lTensor M g

Tactic:
simp_rw [← coe_lTensorHom]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g

Tactic:
exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem tendsto_nhds_right {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)

Tactic:
rw [nhds_eq_comap_uniformity, tendsto_comap_iff]

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem lipschitz_comp {G : β → γ} {C : ℝ≥0} (H : LipschitzWith C G) :
    LipschitzWith C (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
  LipschitzWith.of_dist_le_mul fun f g =>
    (dist_le (mul_nonneg C.2 dist_nonneg)).2 fun x =>
      calc
        dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) := H.dist_le_mul _ _
        _ ≤ C * dist f g

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ ↑C * dist (f x) (g x) ≤ ↑C * dist f g

Tactic:
gcongr

Result:
case h
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ dist (f x) (g x) ≤ dist f g

Proof state:
case h
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ dist (f x) (g x) ≤ dist f g

Tactic:
apply dist_coe_le_dist

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_div_norm_mul_norm_eq_neg_one_iff (x y : F) :
    ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r : ℝ, r < 0 ∧ y = r • x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_div, ← inner_neg_right, ← norm_neg y,
  real_inner_div_norm_mul_norm_eq_one_iff, (@neg_surjective ℝ _).exists]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ x_1, 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x

Tactic:
rw [neg_pos, neg_smul, neg_inj]

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ x_1, 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
refine Iff.rfl.and (exists_congr fun r => ?_)

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem span_singleton_sup_orthogonal_eq_top {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
    (K ∙ x) ⊔ B.orthogonal (K ∙ x) = ⊤

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x}) = ⊤

Tactic:
rw [orthogonal_span_singleton_eq_toLin_ker]

Result:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ ker (B.toLinHomAux₁ x) = ⊤

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ ker (B.toLinHomAux₁ x) = ⊤

Tactic:
exact LinearMap.span_singleton_sup_ker_eq_top _ hx

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem deterministic_apply' {f : α → β} (hf : Measurable f) (a : α) {s : Set β}
    (hs : MeasurableSet s) : deterministic f hf a s = s.indicator (fun _ => 1) (f a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (Measure.dirac (f a)) s = s.indicator 1 (f a)

Tactic:
simp_rw [Measure.dirac_apply' _ hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((deterministic f hf) a) s = s.indicator (fun x => 1) (f a)

Tactic:
rw [deterministic]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ({ toFun := fun a => Measure.dirac (f a), measurable' := ⋯ } a) s = s.indicator (fun x => 1) (f a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ({ toFun := fun a => Measure.dirac (f a), measurable' := ⋯ } a) s = s.indicator (fun x => 1) (f a)

Tactic:
change Measure.dirac (f a) s = s.indicator 1 (f a)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (Measure.dirac (f a)) s = s.indicator 1 (f a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_or {x y : BitVec w} : (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)

Proof state:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x ||| y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) || decide (i < w) && y.getLsbD (w - 1 - i))

Tactic:
by_cases h : i < w <;> simp [h]

Result:
no goals

Proof state:
w i : Nat
x y : BitVec w
⊢ (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)

Tactic:
simp only [getMsbD]

Result:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x ||| y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) || decide (i < w) && y.getLsbD (w - 1 - i))
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract.go₂_append_left : ∀ (s t : List Char) (i e : Nat),
    e = utf8Len s + i → go₂ (s ++ t) ⟨i⟩ ⟨e⟩ = s
| [], t, i, _, rfl => by cases t <;> simp [go₂]
| c :: cs, t, i, _, rfl => by
  simp only [List.cons_append, utf8Len_cons, go₂, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte,
    Pos.addChar_eq, List.cons.injEq, true_and]
  apply go₂_append_left; rw [Nat.add_right_comm, Nat.add_assoc]

Proof state:
t : List Char
i : Nat
⊢ go₂ ([] ++ t) { byteIdx := i } { byteIdx := utf8Len [] + i } = []

Tactic:
cases t <;> simp [go₂]

Result:
no goals

Proof state:
c : Char
cs t : List Char
i : Nat
⊢ go₂ (c :: cs ++ t) { byteIdx := i } { byteIdx := utf8Len (c :: cs) + i } = c :: cs

Tactic:
simp only [List.cons_append, utf8Len_cons, go₂, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte,
  Pos.addChar_eq, List.cons.injEq, true_and]

Result:
c : Char
cs t : List Char
i : Nat
⊢ go₂ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } = cs

Proof state:
case a
c : Char
cs t : List Char
i : Nat
⊢ utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]

Result:
no goals

Proof state:
c : Char
cs t : List Char
i : Nat
⊢ go₂ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } = cs

Tactic:
apply go₂_append_left

Result:
case a
c : Char
cs t : List Char
i : Nat
⊢ utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem dist_same (i : ι) (x y : E i) : dist (Sigma.mk i x) ⟨i, y⟩ = dist x y

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist ⟨i, x⟩ ⟨i, y⟩ = dist x y

Tactic:
simp [Dist.dist, Sigma.dist]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
/-- A variant of `eq_mul_inv_iff_mul_eq₀` that moves the nonzero hypothesis to another variable. -/
lemma mul_eq_of_eq_mul_inv₀ (ha : a ≠ 0) (h : a = c * b⁻¹) : a * b = c

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ a * b = c

Tactic:
rwa [← eq_mul_inv_iff_mul_eq₀]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False

Tactic:
simp [ha] at h

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma disjoint_genWeightSpaceOf [NoZeroSMulDivisors R M] {x : L} {φ₁ φ₂ : R} (h : φ₁ ≠ φ₂) :
    Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)

Proof state:
R : Type u_2
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)

Tactic:
rw [LieSubmodule.disjoint_iff_toSubmodule]

Result:
R : Type u_2
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint ↑(genWeightSpaceOf M φ₁ x) ↑(genWeightSpaceOf M φ₂ x)

Proof state:
R : Type u_2
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (((toEnd R L M) x).maxGenEigenspace φ₁) (((toEnd R L M) x).maxGenEigenspace φ₂)

Tactic:
exact Module.End.disjoint_genEigenspace _ h _ _

Result:
no goals

Proof state:
R : Type u_2
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint ↑(genWeightSpaceOf M φ₁ x) ↑(genWeightSpaceOf M φ₂ x)

Tactic:
dsimp [genWeightSpaceOf]

Result:
R : Type u_2
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (((toEnd R L M) x).maxGenEigenspace φ₁) (((toEnd R L M) x).maxGenEigenspace φ₂)