harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem toSimpleFunc_toLp (f : α →ₛ E) (hfi : MemLp f p μ) : toSimpleFunc (toLp f hfi) =ᵐ[μ] f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ ⇑(toSimpleFunc (toLp f hfi)) =ᶠ[ae μ] ⇑f

Tactic:
rw [← AEEqFun.mk_eq_mk]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEEqFun.mk ⇑(toSimpleFunc (toLp f hfi)) ?m.234584 = AEEqFun.mk ⇑f ?m.234585

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑(toSimpleFunc (toLp f hfi))) μ

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑f) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEEqFun.mk ⇑(toSimpleFunc (toLp f hfi)) ?m.234584 = AEEqFun.mk ⇑f ?m.234585

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑(toSimpleFunc (toLp f hfi))) μ

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑f) μ

Tactic:
exact Classical.choose_spec (toLp f hfi).2

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem ExplicitCoker.map_desc {A B C D B' D' : SemiNormedGrp.{u}}
    {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D} {h : fab ≫ fbd = fac ≫ fcd}
    {fbb' : B ⟶ B'} {fdd' : D ⟶ D'} {condb : fab ≫ fbb' = 0} {condd : fcd ≫ fdd' = 0} {g : B' ⟶ D'}
    (h' : fbb' ≫ g = fbd ≫ fdd') :
    explicitCokernelDesc condb ≫ g = explicitCokernel.map h ≫ explicitCokernelDesc condd

Proof state:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ (explicitCokernelπ fab ≫ explicitCokernelDesc condb) ≫ g =
    (explicitCokernelπ fab ≫ explicitCokernelDesc ⋯) ≫ explicitCokernelDesc condd

Tactic:
simp [Category.assoc, explicitCokernelπ_desc, h']

Result:
no goals

Proof state:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernel.map h ≫ explicitCokernelDesc condd

Tactic:
delta explicitCokernel.map

Result:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernelDesc ⋯ ≫ explicitCokernelDesc condd

Proof state:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernelDesc ⋯ ≫ explicitCokernelDesc condd

Tactic:
simp only [← Category.assoc, ← cancel_epi (explicitCokernelπ fab)]

Result:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ (explicitCokernelπ fab ≫ explicitCokernelDesc condb) ≫ g =
    (explicitCokernelπ fab ≫ explicitCokernelDesc ⋯) ≫ explicitCokernelDesc condd
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_eq_top_of_nonneg (x : ℝ≥0∞) {y : ℝ} (hy0 : 0 ≤ y) : x ^ y = ⊤ → x = ⊤

Proof state:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ False

Tactic:
rw [lt_iff_not_ge] at h

Result:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ ¬y ≥ 0
⊢ False

Proof state:
case inr
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = ⊤ ∧ 0 < y
⊢ x = ⊤

Tactic:
exact h.left

Result:
no goals

Proof state:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ x = ⊤

Tactic:
exfalso

Result:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ False

Proof state:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ ¬y ≥ 0
⊢ False

Tactic:
exact h.right hy0

Result:
no goals

Proof state:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → x = ⊤

Tactic:
rintro (h|h)

Result:
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ x = ⊤

case inr
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = ⊤ ∧ 0 < y
⊢ x = ⊤

Proof state:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x ^ y = ⊤ → x = ⊤

Tactic:
rw [ENNReal.rpow_eq_top_iff]

Result:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → x = ⊤
-- Mathlib/Data/Set/Prod.lean
theorem piMap_image_pi {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective (f i)) (t : ∀ i, Set (α i)) :
    Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
⊢ (s.pi fun i => f i '' t i) ⊆ Pi.map f '' s.pi t

Tactic:
intro b hb

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
⊢ b ∈ Pi.map f '' s.pi t

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
⊢ ∀ (i : ι), ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
intro i

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
i : ι
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
i : ι
hi : i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
⊢ Pi.map f '' s.pi t = s.pi fun i => f i '' t i

Tactic:
refine Subset.antisymm (image_subset_iff.2 fun a ha i hi ↦ mem_image_of_mem _ (ha _ hi)) ?_

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
⊢ (s.pi fun i => f i '' t i) ⊆ Pi.map f '' s.pi t

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ i ∈ s, a i ∈ t i
⊢ b ∈ Pi.map f '' s.pi t

Tactic:
exact ⟨a, hat, funext hab⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
this : ∀ (i : ι), ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ b ∈ Pi.map f '' s.pi t

Tactic:
choose a hab hat using this

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ i ∉ s, Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i => f i '' t i
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ i ∈ s, a i ∈ t i
⊢ b ∈ Pi.map f '' s.pi t
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁)
    (hr₂ : r₂ ≤ 0) : Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)

Tactic:
exact wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
rw [wbtw_comm]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma tensorHom_app_snd {F₁ F₁' F₂ F₂' : J ⥤ C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) :
    (f ⊗ g).app j ≫ snd _ _ = snd _ _ ≫ g.app j

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (snd F₁ F₂).app j ≫ g.app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ snd (F₁'.obj j) (F₂'.obj j) = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Tactic:
change (f ⊗ g).app j ≫ (snd F₁' F₂').app j = _

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ (snd F₁' F₂').app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ (snd F₁' F₂').app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Tactic:
rw [← NatTrans.comp_app, tensorHom_snd, NatTrans.comp_app]

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (snd F₁ F₂).app j ≫ g.app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem mul_inv_cancel {x : tsze R M} (hx : fst x ≠ 0) : x * x⁻¹ = 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
have : Invertible x.fst := Units.invertible (.mk0 _ hx)

Result:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this : Invertible x.fst
⊢ x * x⁻¹ = 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this : Invertible x.fst
⊢ x * x⁻¹ = 1

Tactic:
have := invertibleOfInvertibleFst x

Result:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this✝ : Invertible x.fst
this : Invertible x
⊢ x * x⁻¹ = 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
this✝ : Invertible x.fst
this : Invertible x
⊢ x * x⁻¹ = 1

Tactic:
rw [← invOf_eq_inv, mul_invOf_self]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem length_mul_left_ne (w : W) : ℓ (w * t) ≠ ℓ w

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w✝ w : W
i : B
⊢ cs.lengthParity (w✝ * (w * cs.simple i * w⁻¹)) ≠ cs.lengthParity w✝

Tactic:
simp [lengthParity_simple]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by
  contrapose! this
  simp only [lengthParity_eq_ofAdd_length, this]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.lengthParity (w * t) ≠ cs.lengthParity w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.lengthParity (w * t) ≠ cs.lengthParity w
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
contrapose! this

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.length (w * t) = cs.length w
⊢ cs.lengthParity (w * t) = cs.lengthParity w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.length (w * t) = cs.length w
⊢ cs.lengthParity (w * t) = cs.lengthParity w

Tactic:
simp only [lengthParity_eq_ofAdd_length, this]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.lengthParity (w * t) ≠ cs.lengthParity w

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w✝ w : W
i : B
⊢ cs.lengthParity (w✝ * (w * cs.simple i * w⁻¹)) ≠ cs.lengthParity w✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Depth.lean
theorem size_lt_depth : ∀ t : RBNode α, t.size < 2 ^ t.depth
  | .nil => (by decide : 0 < 1)
  | .node _ a _ b => by
    rw [size, depth, Nat.add_right_comm, Nat.pow_succ, Nat.mul_two]
    refine Nat.add_le_add
      (Nat.lt_of_lt_of_le a.size_lt_depth ?_) (Nat.lt_of_lt_of_le b.size_lt_depth ?_)
    · exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_left ..)
    · exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_right ..)

Proof state:
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ a.size + 1 + b.size < 2 ^ max a.depth b.depth + 2 ^ max a.depth b.depth

Tactic:
refine Nat.add_le_add
  (Nat.lt_of_lt_of_le a.size_lt_depth ?_) (Nat.lt_of_lt_of_le b.size_lt_depth ?_)

Result:
case refine_1
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ a.depth ≤ 2 ^ max a.depth b.depth

case refine_2
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ b.depth ≤ 2 ^ max a.depth b.depth

Proof state:
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 > 0

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
case refine_1
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ a.depth ≤ 2 ^ max a.depth b.depth

Tactic:
exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_left ..)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ 2 ^ b.depth ≤ 2 ^ max a.depth b.depth

Tactic:
exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_right ..)

Result:
no goals

Proof state:
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ (node c✝ a v✝ b).size < 2 ^ (node c✝ a v✝ b).depth

Tactic:
rw [size, depth, Nat.add_right_comm, Nat.pow_succ, Nat.mul_two]

Result:
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
⊢ a.size + 1 + b.size < 2 ^ max a.depth b.depth + 2 ^ max a.depth b.depth
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_mono_right (hb : b ≤ b') (hr : 0 ≤ r) : lineMap a b r ≤ lineMap a b' r

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'

Tactic:
exact add_le_add_left (smul_le_smul_of_nonneg_left hb hr) _

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (lineMap a b) r ≤ (lineMap a b') r

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α} :
    (m.insertMany l).1.contains k → (l.map Sigma.fst).contains k = false → m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k : α
⊢ (m.insertMany l).val.contains k = true → (List.map Sigma.fst l).contains k = false → m.contains k = true

Tactic:
simp_to_model [insertMany] using List.containsKey_of_containsKey_insertList

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
lemma opENorm_comp_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) : ‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : SeminormedAddCommGroup G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
⊢ ‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_mul] using opNNNorm_comp_le h f

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
theorem rank_le_spanRank [StrongRankCondition R] :
    Module.rank R M ≤ (⊤ : Submodule R M).spanRank

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
⊢ #↑↑ι ≤ #↑↑s

Tactic:
have := linearIndependent_le_span'' ι.2 s.1 s.2

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
this : #↑↑ι ≤ #↑↑s
⊢ #↑↑ι ≤ #↑↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M ≤ ⊤.spanRank

Tactic:
rw [Module.rank, Submodule.spanRank]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ ⨆ ι, #↑↑ι ≤ ⨅ s, #↑↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
this : #↑↑ι ≤ #↑↑s
⊢ #↑↑ι ≤ #↑↑s

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ ⨆ ι, #↑↑ι ≤ ⨅ s, #↑↑s

Tactic:
refine ciSup_le' (fun ι ↦ (le_ciInf fun s ↦ ?_))

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
⊢ #↑↑ι ≤ #↑↑s
-- Mathlib/Analysis/RCLike/Basic.lean
theorem re_eq_norm_of_mul_conj (x : K) : re (x * conj x) = ‖x * conj x‖

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖

Tactic:
rw [mul_conj, ← ofReal_pow]

Result:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖

Tactic:
simp [-map_pow]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Function.lean
theorem ae_eq_const_of_ae_eq_comp_ae {g : α → X} (h : QuasiErgodic f μ)
    (hgm : AEStronglyMeasurable g μ) (hg_eq : g ∘ f =ᵐ[μ] g) : ∃ c, g =ᵐ[μ] const α c

Proof state:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᶠ[ae μ] const α c

Tactic:
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩

Result:
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ c, g =ᶠ[ae μ] const α c

Proof state:
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology ↑t
⊢ ∃ c, g =ᶠ[ae μ] const α c

Tactic:
exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq

Result:
no goals

Proof state:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ c, g =ᶠ[ae μ] const α c

Tactic:
borelize X

Result:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᶠ[ae μ] const α c

Proof state:
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ c, g =ᶠ[ae μ] const α c

Tactic:
haveI := ht.secondCountableTopology

Result:
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology ↑t
⊢ ∃ c, g =ᶠ[ae μ] const α c