harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem someExistsOneDivLT_measurableSet : MeasurableSet (someExistsOneDivLT s i)

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet ∅

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

Tactic:
exact
  let ⟨_, h, _⟩ := someExistsOneDivLT_spec hi
  h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet ∅

Tactic:
exact MeasurableSet.empty

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

Tactic:
by_cases hi : ¬s ≤[i] 0

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_eq_sInf_moveRight (G : PGame) [G.Impartial] :
    grundyValue G = sInf (Set.range (grundyValue ∘ G.moveRight))ᶜ

Proof state:
case mk.h.h.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
i : (-mk l r L R).LeftMoves
⊢ (grundyValue ∘ (-mk l r L R).moveLeft) i = (grundyValue ∘ (mk l r L R).moveRight) i

Tactic:
exact @grundyValue_neg _ (@Impartial.moveRight_impartial ⟨l, r, L, R⟩ _ _)

Result:
no goals

Proof state:
case mk
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ (mk l r L R).grundyValue = sInf (Set.range (grundyValue ∘ (mk l r L R).moveRight))ᶜ

Tactic:
rw [← grundyValue_neg, grundyValue_eq_sInf_moveLeft]

Result:
case mk
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ sInf (Set.range (grundyValue ∘ (-mk l r L R).moveLeft))ᶜ = sInf (Set.range (grundyValue ∘ (mk l r L R).moveRight))ᶜ

Proof state:
case mk.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ Set.range (grundyValue ∘ (-mk l r L R).moveLeft) = Set.range (grundyValue ∘ (mk l r L R).moveRight)

Tactic:
apply congr_arg

Result:
case mk.h.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ grundyValue ∘ (-mk l r L R).moveLeft = grundyValue ∘ (mk l r L R).moveRight

Proof state:
case mk.h.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ grundyValue ∘ (-mk l r L R).moveLeft = grundyValue ∘ (mk l r L R).moveRight

Tactic:
ext i

Result:
case mk.h.h.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
i : (-mk l r L R).LeftMoves
⊢ (grundyValue ∘ (-mk l r L R).moveLeft) i = (grundyValue ∘ (mk l r L R).moveRight) i

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G.grundyValue = sInf (Set.range (grundyValue ∘ G.moveRight))ᶜ

Tactic:
obtain ⟨l, r, L, R⟩ := G

Result:
case mk
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ (mk l r L R).grundyValue = sInf (Set.range (grundyValue ∘ (mk l r L R).moveRight))ᶜ

Proof state:
case mk
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ sInf (Set.range (grundyValue ∘ (-mk l r L R).moveLeft))ᶜ = sInf (Set.range (grundyValue ∘ (mk l r L R).moveRight))ᶜ

Tactic:
iterate 3 apply congr_arg

Result:
case mk.h.h.h
l r : Type u_1
L : l → PGame
R : r → PGame
inst✝ : (mk l r L R).Impartial
⊢ grundyValue ∘ (-mk l r L R).moveLeft = grundyValue ∘ (mk l r L R).moveRight
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_const' [Nonempty α] (T : Set α → F →L[ℝ] F') (x : F)
    {m : MeasurableSpace α} : SimpleFunc.setToSimpleFunc T (SimpleFunc.const α x) = T univ x

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : Nonempty α
T : Set α → F →L[ℝ] F'
x : F
m : MeasurableSpace α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
simp only [setToSimpleFunc, range_const, Set.mem_singleton, preimage_const_of_mem,
  sum_singleton, ← Function.const_def, coe_const]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma IsStableUnderBaseChange.mk (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
    (H : ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
      P g → P (pullback.fst f g)) : P.IsStableUnderBaseChange

Proof state:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (pullback.fst f g)

Tactic:
exact H f g hg

Result:
no goals

Proof state:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P g'

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_fst]

Result:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (pullback.fst f g)

Proof state:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
⊢ P.IsStableUnderBaseChange

Tactic:
intros Z X Y S _ _ f g f' g' h hg

Result:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P g'
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ↑(chartAt H x).symm ⁻¹' (s ∩ t) =ᶠ[𝓝 (↑(chartAt H x) x)] ↑(chartAt H x).symm ⁻¹' s

Tactic:
simp_rw [eventuallyEq_set, mem_preimage,
  (chartAt _ x).eventually_nhds' (fun x ↦ x ∈ s ∩ t ↔ x ∈ s) (mem_chart_source _ x)]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s

Tactic:
exact (mem_nhdsWithin_iff_eventuallyEq.mp ht).symm.mem_iff

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x

Tactic:
rw [liftPropWithinAt_iff', liftPropWithinAt_iff', continuousWithinAt_inter' ht, hG.congr_set]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ↑(chartAt H x).symm ⁻¹' (s ∩ t) =ᶠ[𝓝 (↑(chartAt H x) x)] ↑(chartAt H x).symm ⁻¹' s
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- Key lemma for Mahler's theorem: for `f` a continuous function on `ℤ_[p]`, the sequence
`n ↦ Δ^[n] f 0` tends to 0. See `PadicInt.fwdDiff_iter_le_of_forall_le` for an explicit
estimate of the decay rate. -/
lemma fwdDiff_tendsto_zero (f : C(ℤ_[p], E)) : Tendsto (Δ_[1]^[·] f 0) atTop (𝓝 0)

Proof state:
case inr.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos

Result:
case inr.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
t : ℕ
ht : ↑p ^ (-↑t) < δ
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Tactic:
obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this

Result:
case inr.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
-- Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
lemma tsum_set_one : ∑' _ : s, (1 : ℝ≥0∞) = s.encard

Proof state:
case inl.intro
α : Type u_1
s : Finset α
⊢ ∑' (x : ↑↑s), 1 = ↑(↑s).encard

Tactic:
simp [tsum_fintype]

Result:
no goals

Proof state:
case inr
α : Type u_1
s : Set α
hinf : s.Infinite
this : Infinite ↑s
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
obtain (hfin | hinf) := Set.finite_or_infinite s

Result:
case inl
α : Type u_1
s : Set α
hfin : s.Finite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

case inr
α : Type u_1
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Proof state:
case inl
α : Type u_1
s : Set α
hfin : s.Finite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
lift s to Finset α using hfin

Result:
case inl.intro
α : Type u_1
s : Finset α
⊢ ∑' (x : ↑↑s), 1 = ↑(↑s).encard

Proof state:
case inr
α : Type u_1
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
have : Infinite s := infinite_coe_iff.mpr hinf

Result:
case inr
α : Type u_1
s : Set α
hinf : s.Infinite
this : Infinite ↑s
⊢ ∑' (x : ↑s), 1 = ↑s.encard
-- Mathlib/Data/ENNReal/Basic.lean
theorem iInter_Ici_coe_nat : ⋂ n : ℕ, Ici (n : ℝ≥0∞) = {∞}

Proof state:
⊢ ⋂ n, Ici ↑n = {⊤}

Tactic:
simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Radical.lean
theorem Ideal.IsHomogeneous.radical {I : Ideal A} (h : I.IsHomogeneous 𝒜) :
    I.radical.IsHomogeneous 𝒜

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
exact Ideal.IsHomogeneous.sInf fun _ => And.left

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 I.radical

Tactic:
rw [h.radical_eq]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enum_eq_append_iff {l : List α} :
    l.enum = l₁ ++ l₂ ↔
      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = l₂'.enumFrom l₁'.length

Proof state:
α : Type u_1
l₁ l₂ : List (Nat × α)
l : List α
⊢ l.enum = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = enumFrom l₁'.length l₂'

Tactic:
simp [enum, enumFrom_eq_append_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_one_zero : coeff (1 : R[X]) 0 = 1

Proof state:
R : Type u
inst✝ : Semiring R
⊢ coeff 1 0 = 1

Tactic:
simp [coeff_one]

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem fermatNumber_succ (n : ℕ) : fermatNumber (n + 1) = (fermatNumber n - 1) ^ 2 + 1

Proof state:
n : ℕ
⊢ (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1

Tactic:
rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem continuous_uncurry [LocallyCompactSpace X] [LocallyCompactSpace Y] :
    Continuous (uncurry : C(X, C(Y, Z)) → C(X × Y, Z))

Proof state:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous fun x =>
    Function.uncurry (fun x y => Function.uncurry (fun x_1 y => (x x_1) y) y)
      ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y) x)

Tactic:
exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous uncurry

Tactic:
apply continuous_of_continuous_uncurry

Result:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous (Function.uncurry fun x y => x.uncurry y)

Proof state:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous (Function.uncurry fun x y => x.uncurry y)

Tactic:
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']

Result:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous ((Function.uncurry fun x y => x.uncurry y) ∘ ⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y))

Proof state:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous ((Function.uncurry fun x y => x.uncurry y) ∘ ⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y))

Tactic:
dsimp [Function.comp_def]

Result:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous fun x =>
    Function.uncurry (fun x y => Function.uncurry (fun x_1 y => (x x_1) y) y)
      ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y) x)
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : Cᵒᵖ ⥤ D` preserves finite products, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
    coproducts. -/
lemma preservesFiniteCoproducts_rightOp (F : Cᵒᵖ ⥤ D) [PreservesFiniteProducts F] :
    PreservesFiniteCoproducts F.rightOp where
  preserves _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_rightOp

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂'_undef (z : ℂ) {τ : ℂ} (hτ : im τ ≤ 0) : jacobiTheta₂' z τ = 0

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂'_term b z τ

Tactic:
rw [summable_jacobiTheta₂'_term_iff]

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Proof state:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂'_term b z τ

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Tactic:
exact not_lt.mpr hτ

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_rpow_of_exponent_ge {x : ℝ≥0∞} {y z : ℝ} (hx1 : x ≤ 1) (hyz : z ≤ y) :
    x ^ y ≤ x ^ z

Proof state:
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rw [coe_le_one_iff] at hx1

Result:
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Proof state:
case intro
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
by_cases h : x = 0

Result:
case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Proof state:
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero h,
  NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

Result:
no goals

Proof state:
x : ℝ≥0∞
y z : ℝ
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)

Result:
case intro
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
⊢ ↑x ^ y ≤ ↑x ^ z

Proof state:
case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl] <;>
linarith

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma tensorCongr_trans {x y z : Triplet f g} (e : x = y) (e' : y = z) :
    tensorCongr e ≪≫ tensorCongr e' =
      tensorCongr (e.trans e')

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯

Tactic:
subst e e'

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ tensorCongr ⋯ ≪≫ tensorCongr ⋯ = tensorCongr ⋯

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : Triplet f g
⊢ tensorCongr ⋯ ≪≫ tensorCongr ⋯ = tensorCongr ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem coe_sup : ↑(p ⊔ p') = (p + p' : Set M)

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ x✝ ∈ ↑(p ⊔ p') ↔ x✝ ∈ ↑p + ↑p'

Tactic:
rw [SetLike.mem_coe, mem_sup, Set.mem_add]

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ ↑(p ⊔ p') = ↑p + ↑p'

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x✝ : M
⊢ x✝ ∈ ↑(p ⊔ p') ↔ x✝ ∈ ↑p + ↑p'
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive IsAddUnit.exists_neg']
lemma IsUnit.exists_left_inv {a : M} (h : IsUnit a) : ∃ b, b * a = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, b * a = 1

Tactic:
rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩

Result:
case intro.mk
M : Type u_1
inst✝ : Monoid M
a b : M
val_inv✝ : a * b = 1
hba : b * a = 1
⊢ ∃ b_1, b_1 * ↑{ val := a, inv := b, val_inv := val_inv✝, inv_val := hba } = 1

Proof state:
case intro.mk
M : Type u_1
inst✝ : Monoid M
a b : M
val_inv✝ : a * b = 1
hba : b * a = 1
⊢ ∃ b_1, b_1 * ↑{ val := a, inv := b, val_inv := val_inv✝, inv_val := hba } = 1

Tactic:
exact ⟨b, hba⟩

Result:
no goals