harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/LieTheorem.lean
theorem exists_nontrivial_weightSpace_of_lieIdeal [LieModule.IsTriangularizable k L V]
    (A : LieIdeal k L) (hA : IsCoatom A.toSubmodule)
    (χ₀ : Module.Dual k A) [Nontrivial (weightSpace V χ₀)] :
    ∃ (χ : Module.Dual k L), Nontrivial (weightSpace V χ)

Proof state:
case intro.intro.intro.intro.mk
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
have hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v := by
  simpa [W, weightSpaceOfIsLieTower, mem_weightSpace] using hv

Result:
case intro.intro.intro.intro.mk
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
-- Mathlib/Data/Set/Subset.lean
@[simp]
lemma image_val_compl : ↑(Dᶜ) = A \ ↑D

Proof state:
α : Type u_2
A : Set α
D : Set ↑A
⊢ Subtype.val '' Dᶜ = A \ Subtype.val '' D

Tactic:
rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem isUnit_iff : IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}

Tactic:
rw [← singleton_mul_singleton, ← ha, ← hb]

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}

Proof state:
case mpr.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Tactic:
exact ha.set

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩

Result:
case mp.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Proof state:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
rintro ⟨a, rfl, ha⟩

Result:
case mpr.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Proof state:
case mp.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}

Tactic:
exact u.inv_mul

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem mul_left_dvd : ↑u * a ∣ b ↔ a ∣ b

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b

Tactic:
apply mul_right_dvd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
rw [mul_comm]

Result:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem nonarchimedean (q r : ℚ_[p]) : ‖q + r‖ ≤ max ‖q‖ ‖r‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q + r‖ ≤ ‖q‖ ⊔ ‖r‖

Tactic:
dsimp [norm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ↑(padicNormE (q + r)) ≤ ↑(padicNormE q) ⊔ ↑(padicNormE r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ↑(padicNormE (q + r)) ≤ ↑(padicNormE q) ⊔ ↑(padicNormE r)

Tactic:
exact mod_cast nonarchimedean' _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem unsat_nil_cons {g : CNF α} : Unsat ([] :: g)

Proof state:
α : Type u_1
g : CNF α
⊢ Unsat ([] :: g)

Tactic:
simp [unsat_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_modByMonic_lt [Nontrivial R] :
    ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), degree (p %ₘ q) < degree q
  | p, q, hq =>
    letI := Classical.decEq R
    if h : degree q ≤ degree p ∧ p ≠ 0 then by
      have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
      have :=
        degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
      unfold modByMonic at this ⊢
      unfold divModByMonicAux
      dsimp
      rw [dif_pos hq] at this ⊢
      rw [if_pos h]
      exact this
    else
      Or.casesOn (not_and_or.1 h)
        (by
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h]
          exact lt_of_not_ge)
        (by
          intro hp
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
          exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero)))
  termination_by p => p

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2.degree < q.degree
⊢ (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2.degree <
    q.degree

Tactic:
rw [if_pos h]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2.degree < q.degree
⊢ (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
          ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2).2.degree <
    q.degree

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (p %ₘ q).degree < q.degree

Tactic:
have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
⊢ (p %ₘ q).degree < q.degree
-- Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean
theorem finrank_quotient_eq_sum {ι} [Fintype ι] (b : Basis ι R S) [Nontrivial F]
    [∀ i, Module.Free F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))]
    [∀ i, Module.Finite F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))] :
    Module.finrank F (S ⧸ I) =
      ∑ i, Module.finrank F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))

Proof state:
R : Type u_2
S : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsDomain R
inst✝⁹ : IsPrincipalIdealRing R
inst✝⁸ : IsDomain S
F : Type u_4
inst✝⁷ : CommRing F
inst✝⁶ : Algebra F R
inst✝⁵ : Algebra F S
inst✝⁴ : IsScalarTower F R S
I : Ideal S
hI : I ≠ ⊥
ι : Type u_5
inst✝³ : Fintype ι
b : Basis ι R S
inst✝² : Nontrivial F
inst✝¹ : ∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})
⊢ Module.finrank F (S ⧸ I) = ∑ i : ι, Module.finrank F (R ⧸ span {smithCoeffs b I hI i})

Tactic:
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, Module.finrank_directSum]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma span_relation_le_ker_π :
    Submodule.span A (Set.range relations.relation) ≤ LinearMap.ker solution.π

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Submodule.span A (Set.range relations.relation) ≤ LinearMap.ker solution.π

Tactic:
rw [Submodule.span_le]

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Set.range relations.relation ⊆ ↑(LinearMap.ker solution.π)

Proof state:
case intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
r : relations.R
⊢ relations.relation r ∈ ↑(LinearMap.ker solution.π)

Tactic:
simp only [SetLike.mem_coe, LinearMap.mem_ker, π_relation]

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Set.range relations.relation ⊆ ↑(LinearMap.ker solution.π)

Tactic:
rintro _ ⟨r, rfl⟩

Result:
case intro
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
r : relations.R
⊢ relations.relation r ∈ ↑(LinearMap.ker solution.π)
-- Mathlib/Data/List/AList.lean
theorem insert_insert {a} {b b' : β a} (s : AList β) :
    (s.insert a b).insert a b' = s.insert a b'

Proof state:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries

Tactic:
simp only [AList.entries_insert, List.kerase_cons_eq]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ insert a b' (insert a b s) = insert a b' s

Tactic:
ext : 1

Result:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
-- Mathlib/FieldTheory/Isaacs.lean
theorem nonempty_algHom_of_exist_roots (h : ∀ x : E, ∃ y : K, aeval y (minpoly F x) = 0) :
    Nonempty (E →ₐ[F] K)

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let FS := adjoin F (S : Set E)

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, Splits (algebraMap F K') (minpoly F s)
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
⊢ ↥(adjoin F ↑S) →ₐ[F] K
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem Away.eventually_smul_mem {m} (hf : f ∈ 𝒜 m) (z : Away 𝒜 f) :
    ∀ᶠ n in Filter.atTop, f ^ n • z.val ∈ algebraMap _ _ '' (𝒜 (n • m) : Set A)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))

Tactic:
obtain ⟨k, hk : f ^ k = _⟩ := z.den_mem

Result:
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldr_eq (f : Char → α → α) (s a) : foldr f a s = s.1.foldr f a

Proof state:
α : Type u_1
f : Char → α → α
s : String
a : α
⊢ foldr f a s = List.foldr f a s.data

Tactic:
simpa using foldrAux_of_valid f [] s.1 [] a

Result:
no goals
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem toLp_denseRange [CompactSpace α] [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) :
    DenseRange (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)

Proof state:
α : Type u_1
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : NormalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
f : α →ᵇ E
⊢ (BoundedContinuousFunction.toLp p μ 𝕜) f ∈ range ⇑(toLp p μ 𝕜)

Tactic:
exact ⟨f.toContinuousMap, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : NormalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
⊢ range ⇑(BoundedContinuousFunction.toLp p μ 𝕜) ⊆ range ⇑(toLp p μ 𝕜)

Tactic:
refine range_subset_iff.2 fun f ↦ ?_

Result:
α : Type u_1
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : NormalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
f : α →ᵇ E
⊢ (BoundedContinuousFunction.toLp p μ 𝕜) f ∈ range ⇑(toLp p μ 𝕜)

Proof state:
α : Type u_1
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : NormalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
⊢ DenseRange ⇑(toLp p μ 𝕜)

Tactic:
refine (BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_

Result:
α : Type u_1
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : NormalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
⊢ range ⇑(BoundedContinuousFunction.toLp p μ 𝕜) ⊆ range ⇑(toLp p μ 𝕜)
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_integrand_isLittleO (s : ℝ) :
    (fun x : ℝ => exp (-x) * x ^ s) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x)

Proof state:
case refine_2
s : ℝ
this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Tactic:
rw [this]

Result:
case refine_2
s : ℝ
this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)

Proof state:
case h.h
s x : ℝ
⊢ x = x * 2 + -x

Tactic:
ring

Result:
no goals

Proof state:
case refine_2
s : ℝ
this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)

Tactic:
exact (tendsto_exp_mul_div_rpow_atTop s (1 / 2) one_half_pos).inv_tendsto_atTop

Result:
no goals

Proof state:
s : ℝ
⊢ (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹

Tactic:
ext1 x

Result:
case h
s x : ℝ
⊢ rexp (-x) * x ^ s / rexp (-(1 / 2) * x) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹ x

Proof state:
case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0

Tactic:
exfalso

Result:
case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ False

Proof state:
case h
s x : ℝ
⊢ rexp (-x) * x ^ s / rexp (-(1 / 2) * x) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹ x

Tactic:
field_simp [exp_ne_zero, exp_neg, ← Real.exp_add]

Result:
case h
s x : ℝ
⊢ x = x * 2 + -x ∨ x ^ s = 0

Proof state:
case refine_2
s : ℝ
⊢ Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Tactic:
have : (fun x : ℝ => exp (-x) * x ^ s / exp (-(1 / 2) * x)) =
    (fun x : ℝ => exp (1 / 2 * x) / x ^ s)⁻¹ := by
  ext1 x
  field_simp [exp_ne_zero, exp_neg, ← Real.exp_add]
  left
  ring

Result:
case refine_2
s : ℝ
this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹
⊢ Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Proof state:
s : ℝ
⊢ (fun x => rexp (-x) * x ^ s) =o[atTop] fun x => rexp (-(1 / 2) * x)

Tactic:
refine isLittleO_of_tendsto (fun x hx => ?_) ?_

Result:
case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0

case refine_2
s : ℝ
⊢ Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Proof state:
case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ False

Tactic:
exact (exp_pos (-(1 / 2) * x)).ne' hx

Result:
no goals

Proof state:
case h
s x : ℝ
⊢ x = x * 2 + -x ∨ x ^ s = 0

Tactic:
left

Result:
case h.h
s x : ℝ
⊢ x = x * 2 + -x
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem norm_domDomCongr (σ : ι ≃ ι') (f : ContinuousMultilinearMap 𝕜 (fun _ : ι => G) G') :
    ‖domDomCongr σ f‖ = ‖f‖

Proof state:
𝕜 : Type u
ι : Type v
ι' : Type v'
G : Type wG
G' : Type wG'
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 (fun x => G) G'
⊢ ‖domDomCongr σ f‖ = ‖f‖

Tactic:
simp only [norm_def, LinearEquiv.coe_mk, ← σ.prod_comp,
  (σ.arrowCongr (Equiv.refl G)).surjective.forall, domDomCongr_apply, Equiv.arrowCongr_apply,
  Equiv.coe_refl, id_comp, comp_apply, Equiv.symm_apply_apply, id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem fold_le_size {aig : AIG α} (target : FoldTarget aig) :
    aig.decls.size ≤ (fold aig target).1.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤
    (let res := aig.mkConstCached true;
          let aig_1 := res.aig;
          let acc := res.ref;
          let input := target.vec.cast ⋯;
          fold.go aig_1 acc 0 target.len input target.func).aig.decls.size

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤
    (fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 target.len (target.vec.cast ⋯)
            target.func).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ ?m.12308 ≤
    (fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 target.len (target.vec.cast ⋯)
            target.func).aig.decls.size

Tactic:
apply fold.go_le_size

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤
    (fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 target.len (target.vec.cast ⋯)
            target.func).aig.decls.size

Tactic:
refine Nat.le_trans ?_ (by apply fold.go_le_size)

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤ (fold aig target).aig.decls.size

Tactic:
unfold fold

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤
    (let res := aig.mkConstCached true;
          let aig_1 := res.aig;
          let acc := res.ref;
          let input := target.vec.cast ⋯;
          fold.go aig_1 acc 0 target.len input target.func).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size

Tactic:
apply LawfulOperator.le_size (f := mkConstCached)

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem count_roots_le_one [DecidableEq R] {p : R[X]} (hsep : Separable p) (x : R) :
    p.roots.count x ≤ 1

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
exact rootMultiplicity_le_one_of_separable hsep x

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ Multiset.count x p.roots ≤ 1

Tactic:
rw [count_roots p]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1