harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma le_collapse_of_mem (ha : a ∉ s) (hf : 0 ≤ f) (hts : t = s) (ht : t ∈ 𝒜) :
    f t ≤ collapse 𝒜 a f s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ collapse 𝒜 a f t

Tactic:
rw [collapse_eq ha, if_pos ht]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
subst hts

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ collapse 𝒜 a f t

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

Tactic:
exact le_add_of_nonneg_right <| hf _

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem congr_iff_nhdsWithin {s : Set H} {x : H} {f g : H → H'} (h1 : f =ᶠ[𝓝[s] x] g)
    (h2 : f x = g x) : P f s x ↔ P g s x

Proof state:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x

Tactic:
exact ⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩

Result:
no goals

Proof state:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f s x ↔ P g s x

Tactic:
simp_rw [hG.is_local_nhds h1]

Result:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_image_frobenius [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) = f.roots.toFinset

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset = f.roots.toFinset

Tactic:
rw [Finset.image_toFinset, roots_expand_map_frobenius,
    (roots f).toFinset_nsmul _ (expChar_pos R p).ne']

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem char_conj (V : FDRep k G) (g : G) (h : G) : V.character (h * g * h⁻¹) = V.character g

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V : FDRep k G
g h : G
⊢ V.character (h * g * h⁻¹) = V.character g

Tactic:
rw [char_mul_comm, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Topology/Bornology/BoundedOperation.lean
lemma mul_bounded_of_bounded_of_bounded {X : Type*} [PseudoMetricSpace R] [Mul R] [BoundedMul R]
    {f g : X → R} (f_bdd : ∃ C, ∀ x y, dist (f x) (f y) ≤ C)
    (g_bdd : ∃ C, ∀ x y, dist (g x) (g y) ≤ C) :
    ∃ C, ∀ x y, dist ((f * g) x) ((f * g) y) ≤ C

Proof state:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
intro x y

Result:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
x y : X
⊢ dist ((f * g) x) ((f * g) y) ≤ C

Proof state:
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <|
  isBounded_mul (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)

Result:
case intro
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Proof state:
case intro
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
use C

Result:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Proof state:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
x y : X
⊢ dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
exact hC (Set.mul_mem_mul (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
         (Set.mul_mem_mul (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem filter_of_true {p : Box ι → Prop} (hp : ∀ J ∈ π, p J) : π.filter p = π

Proof state:
case h
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
J : Box ι
⊢ J ∈ π.filter p ↔ J ∈ π

Tactic:
simpa using hp J

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
⊢ π.filter p = π

Tactic:
ext J

Result:
case h
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
J : Box ι
⊢ J ∈ π.filter p ↔ J ∈ π
-- Mathlib/Probability/Distributions/Uniform.lean
/-- Alternative way of writing the uniformPDF. -/
lemma uniformPDF_ite {s : Set E} {x : E} :
    uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ (if x ∈ s then ((μ s)⁻¹ • 1) x else 0) = if x ∈ s then (μ s)⁻¹ else 0

Tactic:
simp only [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ s.indicator ((μ s)⁻¹ • 1) x = if x ∈ s then (μ s)⁻¹ else 0

Tactic:
unfold Set.indicator

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ (if x ∈ s then ((μ s)⁻¹ • 1) x else 0) = if x ∈ s then (μ s)⁻¹ else 0

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0

Tactic:
unfold uniformPDF

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ s.indicator ((μ s)⁻¹ • 1) x = if x ∈ s then (μ s)⁻¹ else 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey! k' (modifyKey k f l) =
      if k == k' then
        if containsKey k l then k else default
      else
        getKey! k' l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey! k' (modifyKey k f l) =
    if (k == k') = true then if containsKey k l = true then k else default else getKey! k' l

Tactic:
simp [modifyKey_eq_alterKey, getKey!_alterKey, containsKey_eq_isSome_getValue?, hl]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem two_lt_card : 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Proof state:
α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [two_lt_card_iff, exists_and_left]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem mem_center_iff {R} [NonUnitalSemiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ z ∈ Set.center R

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ ∀ (g : R), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Result:
R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ z ∈ Set.center R
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Proof state:
α : Type u_1
xs : List α
a : α
⊢ xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Tactic:
rw [getLast?_eq_head?_reverse, head?_eq_some_iff]

Result:
α : Type u_1
xs : List α
a : α
⊢ (∃ ys, xs.reverse = a :: ys) ↔ ∃ ys, xs = ys ++ [a]

Proof state:
α : Type u_1
xs : List α
a : α
⊢ (∃ ys, xs = ys.reverse ++ [a]) ↔ ∃ ys, xs = ys ++ [a]

Tactic:
exact ⟨fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩, fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩⟩

Result:
no goals

Proof state:
α : Type u_1
xs : List α
a : α
⊢ (∃ ys, xs.reverse = a :: ys) ↔ ∃ ys, xs = ys ++ [a]

Tactic:
simp only [reverse_eq_cons_iff]

Result:
α : Type u_1
xs : List α
a : α
⊢ (∃ ys, xs = ys.reverse ++ [a]) ↔ ∃ ys, xs = ys ++ [a]

Proof state:
α : Type u_1
xs : List α
a : α
x✝ : ∃ ys, xs = ys ++ [a]
ys : List α
h : xs = ys ++ [a]
⊢ xs = ys.reverse.reverse ++ [a]

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
xs : List α
a : α
x✝ : ∃ ys, xs = ys.reverse ++ [a]
ys : List α
h : xs = ys.reverse ++ [a]
⊢ xs = ys.reverse ++ [a]

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) :
    2 * a + y - x < x

Proof state:
a x y : Nat
h : a < x
hy : y < 2
⊢ 2 * a + y - x < x

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem C_inv (r : k) : (C σ k r)⁻¹ = C σ k r⁻¹

Proof state:
case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ ((C σ k) 0)⁻¹ = (C σ k) 0⁻¹

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
⊢ ((C σ k) r)⁻¹ = (C σ k) r⁻¹

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Result:
case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ ((C σ k) 0)⁻¹ = (C σ k) 0⁻¹

case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ ((C σ k) r)⁻¹ = (C σ k) r⁻¹

Proof state:
case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ ((C σ k) r)⁻¹ = (C σ k) r⁻¹

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel₀ hr, map_one]

Result:
case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (constantCoeff σ k) ((C σ k) r) ≠ 0

Proof state:
case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (constantCoeff σ k) ((C σ k) r) ≠ 0

Tactic:
simpa using hr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
    getKeyD (m.insertIfNew k v) a fallback =
      if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getKeyD a fallback

Tactic:
simp [mem_iff_contains, contains_insertIfNew]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

Tactic:
exact Raw₀.getKeyD_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
lemma one_lt_two [AddLeftStrictMono α] : (1 : α) < 2

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 2

Tactic:
rw [← one_add_one_eq_two]

Result:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 1 + 1

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 1 + 1

Tactic:
exact lt_add_one _

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem one_lt_omega0 : 1 < ω

Proof state:
⊢ 1 < ω

Tactic:
simpa only [Nat.cast_one] using nat_lt_omega0 1

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem elim_comp (h : α → β) {f : γ → α} {x : α} {i : Option γ} :
    (i.elim (h x) fun j => h (f j)) = h (i.elim x f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
⊢ (i.elim (h x) fun j => h (f j)) = h (i.elim x f)

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Infinite.ncard (hs : s.Infinite) : s.ncard = 0

Proof state:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
rw [← Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_eq :
    LinearMap.ker (Finsupp.linearCombination S (KaehlerDifferential.D R S)) =
      KaehlerDifferential.kerTotal R S

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤ LinearMap.ker (kerTotal R S).mkQ

Tactic:
rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤
    LinearMap.ker ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) = kerTotal R S

Tactic:
apply le_antisymm

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤ kerTotal R S

case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ kerTotal R S ≤ LinearMap.ker (linearCombination S ⇑(D R S))

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤ kerTotal R S

Tactic:
conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤ LinearMap.ker (kerTotal R S).mkQ

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ kerTotal R S ≤ LinearMap.ker (linearCombination S ⇑(D R S))

Tactic:
rw [KaehlerDifferential.kerTotal, Submodule.span_le]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (((Set.range fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x => single ((algebraMap R S) x) 1) ⊆
    ↑(LinearMap.ker (linearCombination S ⇑(D R S)))

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ LinearMap.ker (linearCombination S ⇑(D R S)) ≤
    LinearMap.ker ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S))

Tactic:
exact LinearMap.ker_le_ker_comp _ _

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (((Set.range fun x => single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x => single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x => single ((algebraMap R S) x) 1) ⊆
    ↑(LinearMap.ker (linearCombination S ⇑(D R S)))

Tactic:
rintro _ ((⟨⟨x, y⟩, rfl⟩ | ⟨⟨x, y⟩, rfl⟩) | ⟨x, rfl⟩) <;> dsimp <;> simp [LinearMap.mem_ker]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_negg {α} [AddCommGroup α] (a ta t : α)
    (pra : a = ta) (prt : -ta = t) : -a = t

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t

Tactic:
simp [pra, prt]

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem hasDerivAt_tsum (hu : Summable u) (hg : ∀ n y, HasDerivAt (g n) (g' n y) y)
    (hg' : ∀ n y, ‖g' n y‖ ≤ u n) (hg0 : Summable fun n => g n y₀) (y : 𝕜) :
    HasDerivAt (fun z => ∑' n, g n z) (∑' n, g' n y) y

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n => g n y₀
y : 𝕜
⊢ HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
exact hasDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
  (fun n y _ => hg n y) (fun n y _ => hg' n y) (mem_univ _) hg0 (mem_univ _)

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_cancel_left : a ∆ (a ∆ b) = b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ (a ∆ b) = b

Tactic:
simp [← symmDiff_assoc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
/-- Post-composition by an isometry does not change the Lipschitz-property of a function. -/
lemma Isometry.lipschitzWith_iff {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : ℝ≥0) (h : Isometry g) :
    LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
g : β → γ
K : ℝ≥0
h : Isometry g
⊢ LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Tactic:
simp [LipschitzWith, h.edist_eq]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_tsub_one_le_encard_diff_singleton (s : Set α) (x : α) :
    s.encard - 1 ≤ (s \ {x}).encard

Proof state:
α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard

Tactic:
apply tsub_encard_le_encard_diff

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x : α
⊢ s.encard - 1 ≤ (s \ {x}).encard

Tactic:
rw [← encard_singleton x]

Result:
α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard
-- Mathlib/RingTheory/Ideal/Maps.lean
lemma _root_.Pi.ker_ringHom {ι : Type*} {R : ι → Type*} [∀ i, Semiring (R i)]
    (φ : ∀ i, S →+* R i) : ker (Pi.ringHom φ) = ⨅ i, ker (φ i)

Proof state:
S : Type v
inst✝¹ : Semiring S
ι : Type u_3
R : ι → Type u_4
inst✝ : (i : ι) → Semiring (R i)
φ : (i : ι) → S →+* R i
⊢ ker (Pi.ringHom φ) = ⨅ i, ker (φ i)

Tactic:
ext x

Result:
case h
S : Type v
inst✝¹ : Semiring S
ι : Type u_3
R : ι → Type u_4
inst✝ : (i : ι) → Semiring (R i)
φ : (i : ι) → S →+* R i
x : S
⊢ x ∈ ker (Pi.ringHom φ) ↔ x ∈ ⨅ i, ker (φ i)

Proof state:
case h
S : Type v
inst✝¹ : Semiring S
ι : Type u_3
R : ι → Type u_4
inst✝ : (i : ι) → Semiring (R i)
φ : (i : ι) → S →+* R i
x : S
⊢ x ∈ ker (Pi.ringHom φ) ↔ x ∈ ⨅ i, ker (φ i)

Tactic:
simp [mem_ker, Ideal.mem_iInf, funext_iff]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_or_distrib_right {f : Filter α} [NeBot f] {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x ∨ q) ↔ (∃ᶠ x in f, p x) ∨ q

Proof state:
α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Prime.pow_dvd_of_dvd_mul_right [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p)
    (n : ℕ) (h : ¬p ∣ b) (h' : p ^ n ∣ a * b) : p ^ n ∣ a

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a

Tactic:
exact hp.pow_dvd_of_dvd_mul_left n h h'

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a

Tactic:
rw [mul_comm] at h'

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem id_comp (f : A →ₑ+[φ] B) : comp (DistribMulActionHom.id N) f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f : A →ₑ+[φ] B
x : A
⊢ ((DistribMulActionHom.id N).comp f) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals