harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/ScottTopology.lean
/--
The closure of a singleton `{a}` in the Scott topology is the right-closed left-infinite interval
`(-∞,a]`.
-/
@[simp] lemma closure_singleton [IsScott α univ] : closure {a} = Iic a := le_antisymm
  (closure_minimal (by rw [singleton_subset_iff, mem_Iic]) isClosed_Iic) <| by
    rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]
    apply lowerClosure_subset_closure

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ Iic a ≤ closure {a}

Tactic:
rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure {a}) ≤ closure {a}

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ {a} ⊆ Iic a

Tactic:
rw [singleton_subset_iff, mem_Iic]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure {a}) ≤ closure {a}

Tactic:
apply lowerClosure_subset_closure

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem _root_.PrimrecPred.or {p q : α → Prop} [DecidablePred p] [DecidablePred q]
    (hp : PrimrecPred p) (hq : PrimrecPred q) : PrimrecPred fun a => p a ∨ q a :=
  (Primrec.or.comp hp hq).of_eq fun n => by simp

Proof state:
α : Type u_1
inst✝² : Primcodable α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : PrimrecPred p
hq : PrimrecPred q
n : α
⊢ (decide (p n) || decide (q n)) = decide ((fun a => p a ∨ q a) n)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem min_orderTop_le_orderTop_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} :
    min x.orderTop y.orderTop ≤ (x - y).orderTop

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
⊢ x.orderTop ⊓ y.orderTop ≤ (x - y).orderTop

Tactic:
rw [sub_eq_add_neg, ← orderTop_neg (x := y)]

Result:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
⊢ x.orderTop ⊓ (-y).orderTop ≤ (x + -y).orderTop

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
⊢ x.orderTop ⊓ (-y).orderTop ≤ (x + -y).orderTop

Tactic:
exact min_orderTop_le_orderTop_add

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma comp_le_comp : comp a ≤ comp b ↔ b ≤ a := ⟨by rintro ⟨_⟩; assumption, LE.comp⟩

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ≤ comp b → b ≤ a

Tactic:
rintro ⟨_⟩

Result:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b ≤ a
⊢ b ≤ a

Proof state:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b ≤ a
⊢ b ≤ a

Tactic:
assumption

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) :
    ((hST.equiv g).snd : G) = g ↔ g ∈ T

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ ↑(hST.equiv g).2 = g

Tactic:
rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h]

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ g ∈ T

Tactic:
rw [← h]

Result:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ ↑(hST.equiv g).2 ∈ T

Proof state:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).2 = g → g ∈ T

Tactic:
intro h

Result:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ g ∈ T

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).2 = g ↔ g ∈ T

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).2 = g → g ∈ T

case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g ∈ T → ↑(hST.equiv g).2 = g

Proof state:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ ↑(hST.equiv g).2 ∈ T

Tactic:
exact Subtype.prop _

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g ∈ T → ↑(hST.equiv g).2 = g

Tactic:
intro h

Result:
case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ ↑(hST.equiv g).2 = g
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem length_insertP (p : α → Bool) (a l) : (insertP p a l).length = l.length + 1

Proof state:
case cons
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : (insertP p a tail✝).length = tail✝.length + 1
⊢ (match p head✝ with
      | true => a :: head✝ :: tail✝
      | false => insertP.loop p a tail✝ [head✝]).length =
    tail✝.length + 1 + 1

Tactic:
split <;> simp [insertP_loop, ih]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (insertP p a l).length = l.length + 1

Tactic:
induction l with simp [insertP, insertP.loop, cond]
| cons _ _ ih => split <;> simp [insertP_loop, ih]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_inv (s : Set α) : r.inv.preimage s = r.image s

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.inv.preimage s = r.image s

Tactic:
rw [preimage, inv_inv]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem even_xor {m n : ℕ} : Even (m ^^^ n) ↔ (Even m ↔ Even n)

Proof state:
m n : ℕ
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)

Tactic:
omega

Result:
no goals

Proof state:
m n : ℕ
⊢ Even (m ^^^ n) ↔ (Even m ↔ Even n)

Tactic:
simp only [even_iff, xor_mod_two_eq]

Result:
m n : ℕ
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma le_algebraMap_of_spectrum_le {r : R} {a : A} (h : ∀ x ∈ spectrum R a, x ≤ r)
    (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.707655) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : autoParam (p a) _auto✝
⊢ cfc id a ≤ (algebraMap R A) r

Tactic:
exact cfc_le_algebraMap id r a h

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.707655) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : autoParam (p a) _auto✝
⊢ a ≤ (algebraMap R A) r

Tactic:
rw [← cfc_id R a]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.707655) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
h : ∀ x ∈ spectrum R a, x ≤ r
ha : autoParam (p a) _auto✝
⊢ cfc id a ≤ (algebraMap R A) r
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_div (ha : a ≠ 0) (hb : b ≠ 0) : logDeriv (a / b) = logDeriv a - logDeriv b

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (b * a′ - a * b′) * b * (a * b) = (a′ * b - a * b′) * (b ^ 2 * a)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a / b) = logDeriv a - logDeriv b

Tactic:
unfold logDeriv

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a / b)′ / (a / b) = a′ / a - b′ / b

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a / b)′ / (a / b) = a′ / a - b′ / b

Tactic:
field_simp [Derivation.leibniz_div, smul_sub]

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (b * a′ - a * b′) * b * (a * b) = (a′ * b - a * b′) * (b ^ 2 * a)
-- Mathlib/Data/Fintype/Card.lean
theorem card_eq_zero_iff : card α = 0 ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [card, Finset.card_eq_zero, univ_eq_empty_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem isCycleOn_support_cycleOf_aux [DecidableEq α] [Fintype α] (f : Perm α)
    [DecidableRel f.SameCycle] (x : α) : f.IsCycleOn (f.cycleOf x).support :=
  ⟨f.bijOn <| by
    refine fun _ ↦
        ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩
    · exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩
    · exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩
    , fun a ha b hb =>
      by
        rw [mem_coe, mem_support_cycleOf_iff_aux] at ha hb
        exact ha.1.symm.trans hb.1⟩

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ ∀ (a : α), f a ∈ ↑(f.cycleOf x).support ↔ a ∈ ↑(f.cycleOf x).support

Tactic:
refine fun _ ↦
    ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩

Result:
case refine_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : f x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x x✝ ∧ x ∈ f.support

case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support

Proof state:
case refine_2
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x (f x✝) ∧ x ∈ f.support

Tactic:
exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff_aux.1 h).1,
(mem_support_cycleOf_iff_aux.1 h).2⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b

Tactic:
exact ha.1.symm.trans hb.1

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : f x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x x✝ ∧ x ∈ f.support

Tactic:
exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff_aux.1 h).1,
(mem_support_cycleOf_iff_aux.1 h).2⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : a ∈ ↑(f.cycleOf x).support
b : α
hb : b ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle a b

Tactic:
rw [mem_coe, mem_support_cycleOf_iff_aux] at ha hb

Result:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_mono_measure {f : α → β} (hμν : ν ≪ μ) : essSup f ν ≤ essSup f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ essSup f ν ≤ essSup f μ

Tactic:
refine limsup_le_limsup_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae ν) f

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae ν) f

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

Tactic:
all_goals isBoundedDefault

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_one_add (a b : Ordinal) : a ^ (1 + b) = a * a ^ b

Proof state:
a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b

Tactic:
rw [opow_add, opow_one]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS'_two : preNormEDS' b c d 2 = 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS' b c d 2 = 1

Tactic:
rw [preNormEDS']

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_erase_comm : Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
simp_rw [erase_eq, disjoint_sdiff_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma range_two_mul (α) [Semiring α] : Set.range (fun x : α ↦ 2 * x) = {a | Even a}

Proof state:
α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x) = {a | Even a}

Tactic:
ext x

Result:
case h
α : Type u_4
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}

Proof state:
case h
α : Type u_4
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}

Tactic:
simp [eq_comm, two_mul, Even]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem adjoin_empty : adjoin R (∅ : Set A) = ⊥ :=
  show adjoin R ⊥ = ⊥ by apply GaloisConnection.l_bot; exact NonUnitalAlgebra.gc

Proof state:
case gc
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ GaloisConnection (adjoin R) ?u

case u
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ NonUnitalSubalgebra R A → Set A

Tactic:
exact NonUnitalAlgebra.gc

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ adjoin R ⊥ = ⊥

Tactic:
apply GaloisConnection.l_bot

Result:
case gc
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ GaloisConnection (adjoin R) ?u

case u
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ NonUnitalSubalgebra R A → Set A
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph0_le_aleph' {o : Ordinal} : ℵ₀ ≤ aleph' o ↔ ω ≤ o

Proof state:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ aleph' o ↔ ω ≤ o

Tactic:
rw [← aleph'_omega0, aleph'_le]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma zeroLocus_ideal_mem_irreducibleComponents {I : Ideal R} :
    zeroLocus I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R

Tactic:
conv_lhs => rw [← (isClosed_zeroLocus _).closure_eq]

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ closure (zeroLocus ↑I) ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ closure (zeroLocus ↑I) ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R

Tactic:
exact vanishingIdeal_mem_minimalPrimes.symm

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem disjoint_principal_right {f : Filter α} {s : Set α} : Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Proof state:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem piPremeasure_pi {s : ∀ i, Set (α i)} (hs : (pi univ s).Nonempty) :
    piPremeasure m (pi univ s) = ∏ i, m i (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
hs : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i : ι, (m i) (s i)

Tactic:
simp [hs, piPremeasure]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem aemeasurable_inv_iff {G : Type*} [Group G] [MeasurableSpace G] [MeasurableInv G]
    {f : α → G} : AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ :=
  ⟨fun h => by simpa only [inv_inv] using h.inv, fun h => h.inv⟩

Proof state:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
G : Type u_4
inst✝² : Group G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : AEMeasurable (fun x => (f x)⁻¹) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) :
    (K ∙ x) ⊔ ker f = ⊤ :=
  top_unique fun y _ =>
    Submodule.mem_sup.2
      ⟨(f y * (f x)⁻¹) • x, Submodule.mem_span_singleton.2 ⟨f y * (f x)⁻¹, rfl⟩,
        ⟨y - (f y * (f x)⁻¹) • x, by simp [hx]⟩⟩

Proof state:
K : Type u_3
V : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
x : V
hx : f x ≠ 0
y : V
x✝ : y ∈ ⊤
⊢ y - (f y * (f x)⁻¹) • x ∈ ker f ∧ (f y * (f x)⁻¹) • x + (y - (f y * (f x)⁻¹) • x) = y

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma counitBackward_counitForward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v)
    (s : CostructuredArrow yoneda A) : counitBackward F s ∘ counitForward F s = id :=
  funext fun x => by simp [counitBackward]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ (counitBackward F s ∘ counitForward F s) x = id x

Tactic:
simp [counitBackward]

Result:
no goals
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace [CompleteSpace F]
    (h : HasFPowerSeriesOnBall f p x r) {n : ℕ} (v : Fin n → E) :
    iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i))

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
exact h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
n : ℕ
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n f x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Ioc (e : α ≃o β) (a b : α) : e '' Ioc a b = Ioc (e a) (e b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Ioc a b = Ioc (e a) (e b)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Ioc, e.symm_symm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_iff_edist (f : α → β) :
    HasFiniteIntegral f μ ↔ (∫⁻ a, edist (f a) 0 ∂μ) < ∞

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤

Tactic:
simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem Finite.fin_embedding {s : Set α} (h : s.Finite) :
    ∃ (n : ℕ) (f : Fin n ↪ α), range f = s :=
  ⟨_, (Fintype.equivFin (h.toFinset : Set α)).symm.asEmbedding, by
    simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]⟩

Proof state:
α : Type u
s : Set α
h : s.Finite
⊢ range ⇑(Fintype.equivFin ↑↑h.toFinset).symm.asEmbedding = s

Tactic:
simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m

Proof state:
n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]

Result:
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m

Proof state:
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m

Tactic:
omega

Result:
no goals

Proof state:
n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
simp [Ico, this]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldr_subtype' {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) (h : start = l.size) :
    l.foldr f x start 0 = l.unattach.foldr g x

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x l.unattach

Tactic:
rwa [foldr_subtype]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
start : Nat
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
h : start = l.size
⊢ foldr f x l start = foldr g x l.unattach

Tactic:
subst h

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x l.unattach