harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/Ergodic/Conservative.lean
theorem exists_mem_iterate_mem (hf : Conservative f μ)
    (hsm : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) :
    ∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
x : α
hxt : x ∈ t
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ t
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
exact ⟨x, hsub hxt, m, hm₀, hsub hmt⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
⊢ μ t ≠ 0

Tactic:
rwa [measure_congr hts]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hf.exists_mem_iterate_mem' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
x : α
hxt : x ∈ t
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ t
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_subset (s : Set (Set α)) (i : Ordinal) :
    generateMeasurableRec s i ⊆ { t | GenerateMeasurable s t }

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ generateMeasurableRec s i ⊆ {t | GenerateMeasurable s t}

Tactic:
apply WellFoundedLT.induction i

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∀ (x : Ordinal.{u_1}),
    (∀ y < x, generateMeasurableRec s y ⊆ {t | GenerateMeasurable s t}) →
      generateMeasurableRec s x ⊆ {t | GenerateMeasurable s t}

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∀ (x : Ordinal.{u_1}),
    (∀ y < x, generateMeasurableRec s y ⊆ {t | GenerateMeasurable s t}) →
      generateMeasurableRec s x ⊆ {t | GenerateMeasurable s t}

Tactic:
exact fun i IH t ht => generateMeasurableRec_induction .basic .empty
  (fun u _ ⟨j, hj, hj'⟩ => .compl _ (IH j hj hj')) (fun f H => .iUnion _ fun n => (H n).1) ht

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra/Equiv.lean
theorem comp_coe (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :
    e₂.toAlgHom.comp e₁.toAlgHom = e₁.trans e₂

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑(e₁.trans e₂)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / (twoPow w k) = x >>> k

Proof state:
w : Nat
x : BitVec w
k : Nat
hk : k < w
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
w : Nat
x : BitVec w
k : Nat
hk : k < w
this : 2 ^ k < 2 ^ w
⊢ x / twoPow w k = x >>> k

Tactic:
simp [bv_toNat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
k : Nat
hk : k < w
⊢ x / twoPow w k = x >>> k

Tactic:
have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk

Result:
w : Nat
x : BitVec w
k : Nat
hk : k < w
this : 2 ^ k < 2 ^ w
⊢ x / twoPow w k = x >>> k
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊤) : x + z = y + z ↔ x = y

Proof state:
case intro
α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsRightCancelAdd α
hz : z ≠ ⊤
⊢ x + z = y + z ↔ x = y

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_iff_eq_of_div_eq_div (H : a / b = c / d) : a = b ↔ c = d

Proof state:
G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ a = b ↔ c = d

Tactic:
rw [← div_eq_one, H, div_eq_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_X_sub_C [Nontrivial R] [DecidableEq R] {x y : R} :
    rootMultiplicity x (X - C y) = if x = y then 1 else 0

Proof state:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0

Tactic:
exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))

Result:
no goals

Proof state:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - C y) = 1

Tactic:
rw [hxy]

Result:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity y (X - C y) = 1

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
⊢ rootMultiplicity x (X - C y) = if x = y then 1 else 0

Tactic:
split_ifs with hxy

Result:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - C y) = 1

case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0

Proof state:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity y (X - C y) = 1

Tactic:
exact rootMultiplicity_X_sub_C_self

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma lift_fst [Full F] : F.map (hf.lift i h hi) ≫ hf.fst g = i

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝ : F.Full
⊢ F.map (hf.lift i h hi) ≫ hf.fst g = i

Tactic:
simpa [lift] using PullbackCone.IsLimit.lift_fst _ _ _ _

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem OrderIso.map_covBy {α β : Type*} [Preorder α] [Preorder β]
    (f : α ≃o β) {x y : α} : f x ⋖ f y ↔ x ⋖ y

Proof state:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f.symm (f x) ⋖ f.symm (f y) → f x ⋖ f y

Tactic:
exact f.symm.toOrderEmbedding.covBy_of_apply

Result:
no goals

Proof state:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ x ⋖ y → f x ⋖ f y

Tactic:
conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]

Result:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f.symm (f x) ⋖ f.symm (f y) → f x ⋖ f y

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f x ⋖ f y ↔ x ⋖ y

Tactic:
use f.toOrderEmbedding.covBy_of_apply

Result:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ x ⋖ y → f x ⋖ f y
-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem span_single_image (s : Set M) (a : α) :
    Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = map (lsingle a) (span R s)

Tactic:
rw [← span_image]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_bool : #Bool = 2

Proof state:
⊢ #Bool = 2

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FullSubcategory.lean
theorem closedUnderLimitsOfShape_of_limit [P.IsClosedUnderIsomorphisms]
    (h : ∀ {F : J ⥤ C} [HasLimit F], (∀ j, P (F.obj j)) → P (limit F)) :
    ClosedUnderLimitsOfShape J P

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)
⊢ ClosedUnderLimitsOfShape J P

Tactic:
intros F c hc hF

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)
F : J ⥤ C
c : Cone F
hc : IsLimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)
F : J ⥤ C
c : Cone F
hc : IsLimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt

Tactic:
have : HasLimit F := ⟨_, hc⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)
F : J ⥤ C
c : Cone F
hc : IsLimit c
hF : ∀ (j : J), P (F.obj j)
this : HasLimit F
⊢ P c.pt

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)
F : J ⥤ C
c : Cone F
hc : IsLimit c
hF : ∀ (j : J), P (F.obj j)
this : HasLimit F
⊢ P c.pt

Tactic:
exact P.prop_of_iso ((limit.isLimit _).conePointUniqueUpToIso hc) (h hF)

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
lemma AddSubgroup.closure_singleton_int_one_eq_top : closure ({1} : Set ℤ) = ⊤

Proof state:
⊢ closure {1} = ⊤

Tactic:
ext

Result:
case h
x✝ : ℤ
⊢ x✝ ∈ closure {1} ↔ x✝ ∈ ⊤

Proof state:
case h
x✝ : ℤ
⊢ x✝ ∈ closure {1} ↔ x✝ ∈ ⊤

Tactic:
simp [mem_closure_singleton]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem Int.zmultiples_natAbs (a : ℤ) :
    AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a

Proof state:
a : ℤ
⊢ AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a

Tactic:
simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Over.lean
theorem ne_bot_of_liesOver_of_ne_bot (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] : P ≠ ⊥

Proof state:
A : Type u_2
inst✝⁵ : CommRing A
B : Type u_3
inst✝⁴ : Ring B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ p = ⊥

Tactic:
rw [over_def P p, hp, under_bot]

Result:
no goals

Proof state:
A : Type u_2
inst✝⁵ : CommRing A
B : Type u_3
inst✝⁴ : Ring B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
p : Ideal A
hp : p ≠ ⊥
P : Ideal B
inst✝ : P.LiesOver p
⊢ P ≠ ⊥

Tactic:
contrapose! hp

Result:
A : Type u_2
inst✝⁵ : CommRing A
B : Type u_3
inst✝⁴ : Ring B
inst✝³ : Nontrivial B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ p = ⊥
-- Mathlib/Order/WithBot.lean
theorem coe_le_iff : a ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b

Proof state:
α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
⊢ ↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem SpecMap_ΓSpecIso_hom (R : CommRingCat.{u}) :
    Spec.map ((Scheme.ΓSpecIso R).hom) = (Spec R).toSpecΓ

Proof state:
R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this

Result:
no goals

Proof state:
R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
have := ΓSpec.adjunction.right_triangle_components (op R)

Result:
R : CommRingCat
this :
  ΓSpec.adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (ΓSpec.adjunction.counit.app (op R)) =
    𝟙 (Scheme.Spec.obj (op R))
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Proof state:
R : CommRingCat
this :
  ΓSpec.adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (ΓSpec.adjunction.counit.app (op R)) =
    𝟙 (Scheme.Spec.obj (op R))
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
dsimp at this

Result:
R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive (attr := simp)]
lemma mem_smul_set_inv {s : Set α} : a ∈ b • s⁻¹ ↔ b ∈ a • s

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
s : Set α
⊢ a ∈ b • s⁻¹ ↔ b ∈ a • s

Tactic:
simp [mem_smul_set_iff_inv_smul_mem]

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem isCoprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ Nat.Coprime a.natAbs b.natAbs

Proof state:
a b : ℤ
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

Tactic:
rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_eval₂Hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂)
    (p : MvPolynomial σ R) : φ (eval₂Hom f g p) = eval₂Hom (φ.comp f) (fun i => φ (g i)) p

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (φ.comp (eval₂Hom f g)) p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (eval₂Hom (φ.comp f) fun i => φ (g i)) p

Tactic:
rw [← comp_eval₂Hom]

Result:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (φ.comp (eval₂Hom f g)) p
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem Nat.measurable_ceil : Measurable (Nat.ceil : R → ℕ) :=
  measurable_to_countable fun n => by
    rcases eq_or_ne ⌈n⌉₊ 0 with h | h <;> simp_all [h, Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
n : R
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})

Tactic:
rcases eq_or_ne ⌈n⌉₊ 0 with h | h <;> simp_all [h, Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem add_tsub_eq_max : a + (b - a) = max a b

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = a ⊔ b

Tactic:
rw [add_comm, max_comm, tsub_add_eq_max]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1

Proof state:
a b : ℝ≥0
h : a < b
⊢ a / b < 1

Tactic:
rwa [div_lt_iff₀ h.bot_lt, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem insertP_loop (a : α) (l r : List α) :
    insertP.loop p a l r = reverseAux r (insertP p a l)

Proof state:
case cons
α : Type u_1
p : α → Bool
a b : α
l : List α
ih : ∀ (r : List α), insertP.loop p a l r = r.reverseAux (insertP p a l)
r : List α
⊢ (match p b with
    | true => r.reverse ++ a :: b :: l
    | false => (b :: r).reverseAux (insertP p a l)) =
    r.reverse ++
      match p b with
      | true => a :: b :: l
      | false => [b].reverseAux (insertP p a l)

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l r : List α
⊢ insertP.loop p a l r = r.reverseAux (insertP p a l)

Tactic:
induction l generalizing r with simp [insertP, insertP.loop, cond]
| cons b l ih => rw [ih (b :: r), ih [b]]; split <;> simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a b : α
l : List α
ih : ∀ (r : List α), insertP.loop p a l r = r.reverseAux (insertP p a l)
r : List α
⊢ (match p b with
    | true => r.reverse ++ a :: b :: l
    | false => insertP.loop p a l (b :: r)) =
    r.reverse ++
      match p b with
      | true => a :: b :: l
      | false => insertP.loop p a l [b]

Tactic:
rw [ih (b :: r), ih [b]]

Result:
case cons
α : Type u_1
p : α → Bool
a b : α
l : List α
ih : ∀ (r : List α), insertP.loop p a l r = r.reverseAux (insertP p a l)
r : List α
⊢ (match p b with
    | true => r.reverse ++ a :: b :: l
    | false => (b :: r).reverseAux (insertP p a l)) =
    r.reverse ++
      match p b with
      | true => a :: b :: l
      | false => [b].reverseAux (insertP p a l)
-- Mathlib/Data/Option/NAry.lean
theorem map₂_map_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
    (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) : map₂ f (a.map g) b = (map₂ f' a b).map g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' a b)

Tactic:
cases a <;> cases b <;> simp [h_left_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem nhds_eq_update : (𝓝 : Γ₀ → Filter Γ₀) = update pure 0 (⨅ γ ≠ 0, 𝓟 (Iio γ))

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
rw [nhds_nhdsAdjoint, sup_of_le_right]

Result:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ pure 0 ≤ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ pure 0 ≤ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Tactic:
exact le_iInf₂ fun γ hγ ↦ le_principal_iff.2 <| zero_lt_iff.2 hγ

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive]
lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
gcongr

Result:
case h'
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Proof state:
case h'
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
exact subset_pow hs hn

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_le_degrees_card (p : MvPolynomial σ R) :
    p.totalDegree ≤ Multiset.card p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
rw [totalDegree_eq]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun m => (toMultiset m).card) ≤ p.degrees.card

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
classical
rw [totalDegree_eq]
exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun m => (toMultiset m).card) ≤ p.degrees.card

Tactic:
exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_nonneg_iff {z : ℂ} : 0 ≤ arg z ↔ 0 ≤ z.im

Proof state:
case inl

⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
calc
  0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
    ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩, by
      contrapose!
      intro h
      exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
  _ ↔ _ := by rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

Result:
no goals

Proof state:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg

Tactic:
contrapose!

Result:
z : ℂ
h₀ : z ≠ 0
⊢ z.arg < 0 → Real.sin z.arg < 0

Proof state:
z : ℂ
h₀ : z ≠ 0
⊢ z.arg < 0 → Real.sin z.arg < 0

Tactic:
intro h

Result:
z : ℂ
h₀ : z ≠ 0
h : z.arg < 0
⊢ Real.sin z.arg < 0

Proof state:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im

Tactic:
rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

Result:
no goals

Proof state:
z : ℂ
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

Result:
case inl

⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Proof state:
z : ℂ
h₀ : z ≠ 0
h : z.arg < 0
⊢ Real.sin z.arg < 0

Tactic:
exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/WithAbs.lean
theorem isometry_of_comp (h : ∀ x, ‖f x‖ = v x) : Isometry f :=
  Isometry.of_dist_eq <| fun x y => by simp only [‹NormedField L›.dist_eq, ← f.map_sub, h]; rfl

Proof state:
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : WithAbs v
⊢ v (x - y) = dist x y

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : WithAbs v
⊢ dist (f x) (f y) = dist x y

Tactic:
simp only [‹NormedField L›.dist_eq, ← f.map_sub, h]

Result:
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x y : WithAbs v
⊢ v (x - y) = dist x y
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_le_one_iff_mul_self_le_one : |a| ≤ 1 ↔ a * a ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1

Tactic:
simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem has_both (b : Bool) : hasAssignment b both = true

Proof state:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true

Tactic:
split <;> decide

Result:
no goals

Proof state:
b : Bool
⊢ hasAssignment b both = true

Tactic:
rw [hasAssignment]

Result:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true