harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.Transcendental.of_ringHom_of_comp_eq [H : Algebra.Transcendental S B]
    (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental R A

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ¬Algebra.IsAlgebraic S B
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ¬Algebra.IsAlgebraic R A

Tactic:
exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)

Result:
no goals

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental S B
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental R A

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢

Result:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ¬Algebra.IsAlgebraic S B
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ¬Algebra.IsAlgebraic R A
-- Mathlib/Data/Nat/Prime/Infinite.lean
theorem not_bddAbove_setOf_prime : ¬BddAbove { p | Prime p }

Proof state:
⊢ ¬BddAbove {p | Prime p}

Tactic:
rw [not_bddAbove_iff]

Result:
⊢ ∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y

Proof state:
case intro.intro
n p : ℕ
hi : n.succ ≤ p
hp : Prime p
⊢ ∃ y ∈ {p | Prime p}, n < y

Tactic:
exact ⟨p, hp, hi⟩

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ y ∈ {p | Prime p}, n < y

Tactic:
obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ

Result:
case intro.intro
n p : ℕ
hi : n.succ ≤ p
hp : Prime p
⊢ ∃ y ∈ {p | Prime p}, n < y

Proof state:
⊢ ∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y

Tactic:
intro n

Result:
n : ℕ
⊢ ∃ y ∈ {p | Prime p}, n < y
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_neg {f : MvPolynomial σ R} :
    m.degree (-f) = m.degree f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm ((-f).support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)

Tactic:
rw [support_neg]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.degree (-f) = m.degree f

Tactic:
unfold degree

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm ((-f).support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_mem_card_add`. -/
lemma mem_shadow_iterate_iff_exists_sdiff : t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ #((t ∪ u) \ t) = #u

Tactic:
rw [union_sdiff_cancel_left htu]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
rw [mem_shadow_iterate_iff_exists_card]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Proof state:
case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
rintro ⟨u, rfl, htu, hsuA⟩

Result:
case mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = #u

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ t ∪ s \ t ∈ 𝒜

Tactic:
rwa [union_sdiff_self_eq_union, union_eq_right.2 hts]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
rintro ⟨s, hs, hts, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ ∃ u, #u = #(s \ t) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ ∃ u, #u = #(s \ t) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
refine ⟨s \ t, rfl, disjoint_sdiff, ?_⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hts : t ⊆ s
⊢ t ∪ s \ t ∈ 𝒜

Proof state:
case mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t u : Finset α
htu : Disjoint t u
hsuA : t ∪ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = #u

Tactic:
exact ⟨_, hsuA, subset_union_left, by rw [union_sdiff_cancel_left htu]⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense. -/
lemma contMDiffOn_vectorSpace_iff_contDiffOn
    {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {n : ℕ∞} {s : Set E} :
    ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) s ↔
      ContDiffOn 𝕜 n V s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
s : Set E
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) s ↔ ContDiffOn 𝕜 (↑n) V s

Tactic:
simp only [ContMDiffOn, ContDiffOn, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem _root_.SimpleGraph.induce_eq_coe_induce_top (s : Set V) :
    G.induce s = ((⊤ : G.Subgraph).induce s).coe

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ (SimpleGraph.induce s G).Adj x✝¹ x✝ ↔ (⊤.induce s).coe.Adj x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s : Set V
⊢ SimpleGraph.induce s G = (⊤.induce s).coe

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ (SimpleGraph.induce s G).Adj x✝¹ x✝ ↔ (⊤.induce s).coe.Adj x✝¹ x✝
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_torsion_smul {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
    logMap (ζ • x) = logMap x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ logMap (ζ • x) = logMap x

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ logMap (ζ • x) x✝ = logMap x x✝

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ logMap (ζ • x) x✝ = logMap x x✝

Tactic:
simp_rw [logMap_apply, unitSMul_smul, map_mul, norm_eq_norm, Units.norm, Rat.cast_one, one_mul,
  normAtPlace_apply, (mem_torsion K).mp hζ, one_mul]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem exists_simple_submodule [Nontrivial M] : ∃ m : Submodule R M, IsSimpleModule R m

Proof state:
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
⊢ ∃ m, IsSimpleModule R ↥m

Tactic:
simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
lemma centralizer_tensorProduct_eq_center_tensorProduct_right [Module.Free R A] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    centralizer R ↑includeRight.range

Tactic:
simp [Algebra.TensorProduct.map_range]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
rw [← centralizer_range_includeRight_eq_center_tensorProduct]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    centralizer R ↑includeRight.range
-- Mathlib/Logic/Function/Basic.lean
theorem surjective_comp_left_iff [Nonempty α] {g : β → γ} :
    Surjective (g ∘ · : (α → β) → α → γ) ↔ Surjective g

Proof state:
α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
h : Surjective fun x => g ∘ x
c : γ
a : α
⊢ ∃ a, g a = c

Tactic:
have ⟨f, hf⟩ := h fun _ ↦ c

Result:
α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
h : Surjective fun x => g ∘ x
c : γ
a : α
f : α → β
hf : (fun x => g ∘ x) f = fun x => c
⊢ ∃ a, g a = c

Proof state:
α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
h : Surjective fun x => g ∘ x
c : γ
a : α
f : α → β
hf : (fun x => g ∘ x) f = fun x => c
⊢ ∃ a, g a = c

Tactic:
exact ⟨f a, congr_fun hf _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
      succ i (reverseInduction zero succ i.succ)

Proof state:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
i : Fin n
⊢ (let j := ⟨↑i.castSucc, ⋯⟩;
    succ j (reverseInduction zero succ j.succ)) =
    succ i (reverseInduction zero succ i.succ)

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
i : Fin n
⊢ reverseInduction zero succ i.castSucc = succ i (reverseInduction zero succ i.succ)

Tactic:
rw [reverseInduction, dif_neg (Fin.ne_of_lt (Fin.castSucc_lt_last i))]

Result:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
i : Fin n
⊢ (let j := ⟨↑i.castSucc, ⋯⟩;
    succ j (reverseInduction zero succ j.succ)) =
    succ i (reverseInduction zero succ i.succ)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_add_const (r : R) (f : R → R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x + r) a = cfc f a + (algebraMap R A) r

Tactic:
rw [add_comm (cfc f a)]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x + r) a = (algebraMap R A) r + cfc f a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x + r) a = (algebraMap R A) r + cfc f a

Tactic:
conv_lhs => simp only [add_comm]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a

Tactic:
exact cfc_const_add r f a hf ha

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
@[to_additive]
lemma mul_self (x : G) : x * x = 1

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ x * x = 1

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_eq_self]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem _root_.HasCompactSupport.memLp_of_bound {f : X → E} (hf : HasCompactSupport f)
    (h2f : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : MemLp f p μ

Proof state:
E : Type u_4
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
this : MemLp f ⊤ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
  (fun x ↦ image_eq_zero_of_nmem_tsupport) (hf.measure_lt_top.ne) le_top

Result:
no goals

Proof state:
E : Type u_4
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f p μ

Tactic:
have := memLp_top_of_bound h2f C hfC

Result:
E : Type u_4
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
this : MemLp f ⊤ μ
⊢ MemLp f p μ
-- Mathlib/Data/Set/MemPartition.lean
lemma memPartitionSet_eq_iff {f : ℕ → Set α} {n : ℕ} (a : α) {s : Set α}
    (hs : s ∈ memPartition f n) :
    memPartitionSet f n a = s ↔ a ∈ s

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
⊢ False

Tactic:
have h_disj : Disjoint s (memPartitionSet f n a) :=
  disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ False

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty

Tactic:
exact ⟨a, h, mem_memPartitionSet f n a⟩

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ ¬Disjoint s (memPartitionSet f n a)

Tactic:
rw [not_disjoint_iff_nonempty_inter]

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
⊢ memPartitionSet f n a = s ↔ a ∈ s

Tactic:
refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
⊢ memPartitionSet f n a = s

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ False

Tactic:
refine absurd h_disj ?_

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ ¬Disjoint s (memPartitionSet f n a)

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
⊢ memPartitionSet f n a = s

Tactic:
by_contra h_ne

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
⊢ False
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
theorem semilength_outsidePart_lt : p.outsidePart.semilength < p.semilength

Proof state:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.outsidePart.semilength < p.semilength

Tactic:
omega

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
have := semilength_insidePart_add_semilength_outsidePart_add_one h

Result:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.outsidePart.semilength < p.semilength
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma strictConcaveOn_negMulLog : StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) negMulLog

Proof state:
⊢ StrictConcaveOn ℝ (Set.Ici 0) negMulLog

Tactic:
simpa only [negMulLog_eq_neg] using strictConvexOn_mul_log.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l

Proof state:
α : Type u_1
l : List α
⊢ foldr cons [] l = l

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
lemma eq_stalkwise :
    @SurjectiveOnStalks = stalkwise (Function.Surjective ·)

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ↔ stalkwise (fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x) x✝

Tactic:
exact surjectiveOnStalks_iff _

Result:
no goals

Proof state:
⊢ @SurjectiveOnStalks = stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ↔ stalkwise (fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x) x✝
-- Mathlib/Data/Seq/WSeq.lean
theorem join_cons (s : WSeq α) (S) : join (cons s S) = think (append s (join S))

Proof state:
α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ (Seq.map
        (fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s))
        (cons s S)).join =
    Seq.cons none
      (s.append
        (Seq.map
            (fun o =>
              match o with
              | none => Seq1.ret none
              | some s => (none, s))
            S).join)

Tactic:
simp [join, cons, append]

Result:
no goals

Proof state:
α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ (cons s S).join = (s.append S.join).think

Tactic:
simp only [join, think]

Result:
α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ ((fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s)) <$>
        cons s S).join =
    Seq.cons none
      (s.append
        ((fun o =>
              match o with
              | none => Seq1.ret none
              | some s => (none, s)) <$>
            S).join)
-- Mathlib/RingTheory/PowerBasis.lean
theorem constr_pow_algebraMap (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0)
    (x : A) : pb.basis.constr A (fun i => y ^ (i : ℕ)) (algebraMap A S x) = algebraMap A S' x

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x

Tactic:
convert pb.constr_pow_aeval hy (C x) <;> rw [aeval_C]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem AlgebraicIndependent.option_iff (hx : AlgebraicIndependent R x) (a : A) :
    (AlgebraicIndependent R fun o : Option ι => o.elim a x) ↔
      Transcendental (adjoin R (Set.range x)) a

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (AlgebraicIndependent R fun o => o.elim a x) ↔ Transcendental (↥(adjoin R (range x))) a

Tactic:
rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
  ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
  RingHom.coe_comp]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ Injective (⇑↑(Polynomial.aeval a) ∘ ⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) ↔
    Injective ⇑(Polynomial.aeval a)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ Injective (⇑↑(Polynomial.aeval a) ∘ ⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) ↔
    Injective ⇑(Polynomial.aeval a)

Tactic:
exact Injective.of_comp_iff' (Polynomial.aeval a)
  (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective

Result:
no goals