harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Sign.lean
lemma ofSign_disjUnion :
    (ofSign 1).disjUnion (ofSign (-1)) ofSign_disjoint = (univ : Finset (Perm α))

Proof state:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯ ↔ σ ∈ univ

Tactic:
simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (ofSign 1).disjUnion (ofSign (-1)) ⋯ = univ

Tactic:
ext σ

Result:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯ ↔ σ ∈ univ
-- Mathlib/Topology/Separation/Basic.lean
theorem isOpen_setOf_eventually_nhdsWithin [T1Space X] {p : X → Prop} :
    IsOpen { x | ∀ᶠ y in 𝓝[≠] x, p y }

Proof state:
case h.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
exact hb.filter_mono nhdsWithin_le_nhds

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
rcases eq_or_ne a b with rfl | h

Result:
case h.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

case h.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
⊢ IsOpen {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}

Tactic:
refine isOpen_iff_mem_nhds.mpr fun a ha => ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
⊢ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a

Proof state:
case h.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
rw [h.symm.nhdsWithin_compl_singleton] at hb

Result:
case h.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Proof state:
case h.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

Tactic:
exact hb

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
⊢ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a

Tactic:
filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem map_C (r : R) : map f (C _ r) = C _ (f r)

Proof state:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (map f) ((C R) r) = (C S) (f r)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
r : R
n✝ : ℕ
⊢ (coeff S n✝) ((map f) ((C R) r)) = (coeff S n✝) ((C S) (f r))

Proof state:
case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
r : R
n✝ : ℕ
⊢ (coeff S n✝) ((map f) ((C R) r)) = (coeff S n✝) ((C S) (f r))

Tactic:
simp [coeff_C, apply_ite f]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size

Proof state:
α : Type u_1
a : Array α
v : α
i : USize
h : i.toNat < a.size
⊢ (a.uset i v h).size = a.size

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Lemmas.lean
theorem lt_irrefl (a : Char) : ¬ a < a

Proof state:
a : Char
⊢ ¬a < a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_neg_same' (hf : Integrable (fun x ↦ exp (f x)) μ) :
    (μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ

Tactic:
rw [tilted_tilted hf]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
⊢ μ.tilted (f + -f) = (μ Set.univ)⁻¹ • μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
⊢ μ.tilted (f + -f) = (μ Set.univ)⁻¹ • μ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem shiftRightNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
    x' >>> n = x >>> n

Proof state:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x' >>> n = x >>> n

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem comap_map_eq_self {f : R →+* S} {s : Subring R}
    (h : f ⁻¹' {0} ⊆ s) : (s.map f).comap f = s

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ comap f (map f s) = s

Tactic:
convert comap_map_eq f s

Result:
case h.e'_3
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ s = s ⊔ closure (⇑f ⁻¹' {0})

Proof state:
case h.e'_3
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ s = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rwa [left_eq_sup, closure_le]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem OneOneReducible.trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop}
    {q : β → Prop} {r : γ → Prop} : p ≤₁ q → q ≤₁ r → p ≤₁ r
  | ⟨f, c₁, i₁, h₁⟩, ⟨g, c₂, i₂, h₂⟩ =>
    ⟨g ∘ f, c₂.comp c₁, i₂.comp i₁, fun a =>
      ⟨fun h => by erw [← h₂, ← h₁]; assumption, fun h => by rwa [h₁, h₂]⟩⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r ((g ∘ f) a)

Tactic:
erw [← h₂, ← h₁]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a

Tactic:
rwa [h₁, h₂]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_inter_Ioc : Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]

Result:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_eq_of_subset_left (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) :
    t.ite s₁ s₂ = s₁ ∪ (s₂ \ t)

Proof state:
case h
α : Type u
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_right_of_imp (@h x)]

Result:
no goals

Proof state:
α : Type u
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
⊢ t.ite s₁ s₂ = s₁ ∪ s₂ \ t

Tactic:
ext x

Result:
case h
α : Type u
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) :
    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l)

Proof state:
case cons.zero
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, l.length ≤ k → (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
hk : (x :: l).length ≤ 0
⊢ (x :: l ++ l').eraseIdx 0 = x :: l ++ l'.eraseIdx (0 - (x :: l).length)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, l.length ≤ k → (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
k : Nat
hk : (x :: l).length ≤ k
⊢ (x :: l ++ l').eraseIdx k = x :: l ++ l'.eraseIdx (k - (x :: l).length)

Tactic:
cases k with
| zero => simp_all
| succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, l.length ≤ k → (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
k : Nat
hk : (x :: l).length ≤ k + 1
⊢ (x :: l ++ l').eraseIdx (k + 1) = x :: l ++ l'.eraseIdx (k + 1 - (x :: l).length)

Tactic:
simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]

Result:
no goals

Proof state:
case nil
α : Type u_1
l' : List α
k : Nat
hk : [].length ≤ k
⊢ ([] ++ l').eraseIdx k = [] ++ l'.eraseIdx (k - [].length)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
k : Nat
hk : l.length ≤ k
l' : List α
⊢ (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)

Tactic:
induction l generalizing k with
| nil => simp_all
| cons x l ih =>
  cases k with
  | zero => simp_all
  | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem mem_permutationsAux2' {t : α} {ts : List α} {ys : List α} {l : List α} :
    l ∈ (permutationsAux2 t ts [] ys id).2 ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

Proof state:
case h
α : Type u_1
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
t : α
ts ys l : List α
⊢ id = fun x => [] ++ x

Tactic:
funext _

Result:
case h
α : Type u_1
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝

Proof state:
α : Type u_1
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
apply mem_permutationsAux2

Result:
no goals
-- Mathlib/AlgebraicGeometry/Properties.lean
theorem basicOpen_eq_bot_iff {X : Scheme} [IsReduced X] {U : X.Opens}
    (s : Γ(X, U)) : X.basicOpen s = ⊥ ↔ s = 0

Proof state:
X : Scheme
inst✝ : IsReduced X
U : X.Opens
⊢ X.basicOpen 0 = ⊥

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
inst✝ : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
⊢ s = 0 → X.basicOpen s = ⊥

Tactic:
rintro rfl

Result:
X : Scheme
inst✝ : IsReduced X
U : X.Opens
⊢ X.basicOpen 0 = ⊥

Proof state:
X : Scheme
inst✝ : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
⊢ X.basicOpen s = ⊥ ↔ s = 0

Tactic:
refine ⟨eq_zero_of_basicOpen_eq_bot s, ?_⟩

Result:
X : Scheme
inst✝ : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
⊢ s = 0 → X.basicOpen s = ⊥
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem Monic.normalize_eq_self {p : R[X]} (hp : p.Monic) : normalize p = p

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
hp : p.Monic
⊢ normalize p = p

Tactic:
simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
  Units.val_one, Polynomial.C.map_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem multiset_prod_mem {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M)
    (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S

Proof state:
case intro
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ (Multiset.map Subtype.val m).prod ∈ S

Tactic:
rw [← coe_multiset_prod]

Result:
case intro
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Proof state:
case intro
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Tactic:
exact m.prod.coe_prop

Result:
no goals

Proof state:
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S

Tactic:
lift m to Multiset S using hm

Result:
case intro
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ (Multiset.map Subtype.val m).prod ∈ S
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_castPred (i : Fin (n + 1)) (h : i ≠ last n) :
    castSucc (i.castPred h) = i

Proof state:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
⊢ (i.castPred h).castSucc = i

Tactic:
rcases exists_castSucc_eq.mpr h with ⟨y, rfl⟩

Result:
case intro
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc

Proof state:
case intro
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc

Tactic:
rw [castPred_castSucc]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_div : (a / b)⁻¹ = b / a

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a / b)⁻¹ = b / a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_inv_div_inv : (a⁻¹ / b⁻¹)⁻¹ = a / b

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a⁻¹ / b⁻¹)⁻¹ = a / b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem const (b : β) : LipschitzWith 0 fun _ : α => b := fun x y => by
  simp only [edist_self, zero_le]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
x y : α
⊢ edist ((fun x => b) x) ((fun x => b) y) ≤ ↑0 * edist x y

Tactic:
simp only [edist_self, zero_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_cons_div_left : (gcd (x::xs) : Int) ∣ x

Proof state:
x : Int
xs : List Int
⊢ x.natAbs.gcd (List.foldr (fun x g => x.natAbs.gcd g) 0 xs) ∣ x.natAbs

Tactic:
apply Nat.gcd_dvd_left

Result:
no goals

Proof state:
x : Int
xs : List Int
⊢ ↑(gcd (x :: xs)) ∣ x

Tactic:
simp only [gcd, List.foldr_cons, Int.ofNat_dvd_left]

Result:
x : Int
xs : List Int
⊢ x.natAbs.gcd (List.foldr (fun x g => x.natAbs.gcd g) 0 xs) ∣ x.natAbs
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε :=
  (atTop_basis.tendsto_iff nhds_basis_eball).trans <| by
    simp only [exists_prop, true_and, mem_Ici, mem_ball]

Proof state:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε

Tactic:
simp only [exists_prop, true_and, mem_Ici, mem_ball]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mk_mem_graph_iff {a : α} {m : M} {f : α →₀ M} : (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Proof state:
case mp.intro.intro.refl
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ f a = f a ∧ f a ≠ 0

Tactic:
exact ⟨rfl, ha⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_2 = (a, m)

Tactic:
rintro ⟨rfl, ha⟩

Result:
case mpr.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ ∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, f a)

Proof state:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, m)) → f a = m ∧ m ≠ 0

Tactic:
rintro ⟨b, ha, rfl, -⟩

Result:
case mp.intro.intro.refl
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ f a = f a ∧ f a ≠ 0

Proof state:
case mpr.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α →₀ M
ha : f a ≠ 0
⊢ ∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, f a)

Tactic:
exact ⟨a, ha, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, m)) → f a = m ∧ m ≠ 0

case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_2 = (a, m)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Tactic:
simp_rw [graph, mem_map, mem_support_iff]

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@[simp] lemma mass_prod : (μ.prod ν).mass = μ.mass * ν.mass

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ).toNNReal * (↑ν univ).toNNReal

Tactic:
rw [← ENNReal.toNNReal_mul]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal

Tactic:
exact congr_arg ENNReal.toNNReal (Measure.prod_prod univ univ)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).mass = μ.mass * ν.mass

Tactic:
simp only [coeFn_def, mass, univ_prod_univ.symm, toMeasure_prod]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ).toNNReal * (↑ν univ).toNNReal
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem atEnd : ∀ {s}, ValidFor l m r s → (s.atEnd ⟨p⟩ ↔ p = utf8Len m)
  | _, ⟨⟩ => by simp [Substring.atEnd, Pos.ext_iff, Nat.add_left_cancel_iff]

Proof state:
l m r : List Char
p : Nat
⊢ { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.atEnd
        { byteIdx := p } =
      true ↔
    p = utf8Len m

Tactic:
simp [Substring.atEnd, Pos.ext_iff, Nat.add_left_cancel_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem map_restrict_of_zero [Zero γ] {g : β → γ} (hg : g 0 = 0) (f : α →ₛ β) (s : Set α) :
    (f.restrict s).map g = (f.map g).restrict s :=
  ext fun x =>
    if hs : MeasurableSet s then by simp [hs, Set.indicator_comp_of_zero hg]
    else by simp [restrict_of_not_measurable hs, hg]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : MeasurableSet s
⊢ (map g (f.restrict s)) x = ((map g f).restrict s) x

Tactic:
simp [hs, Set.indicator_comp_of_zero hg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : ¬MeasurableSet s
⊢ (map g (f.restrict s)) x = ((map g f).restrict s) x

Tactic:
simp [restrict_of_not_measurable hs, hg]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem add_mul_right_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + z * y) y

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y

Tactic:
exact h.add_mul_left_left z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Compiler/LCNF/PassManager.lean
theorem Phase.le_refl (p : Phase) : p ≤ p

Proof state:
p : Phase
⊢ p ≤ p

Tactic:
cases p <;> decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
    @Fin.succRecOn (n + 1) 0 motive zero succ = zero n

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

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_equiv_eq_zero_iff_lift_ne : #(α ≃ β') = 0 ↔ lift.{v} #α ≠ lift.{u} #β'

Proof state:
α : Type u
β' : Type v
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma cauchy_map_iff_tendsto (𝓕 : Filter ι) (f : ι → G) :
    Cauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Proof state:
ι : Type u_3
G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝓕 : Filter ι
f : ι → G
⊢ Cauchy (map f 𝓕) ↔ 𝓕.NeBot ∧ Tendsto (fun p => f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [cauchy_map_iff, uniformity_eq_comap_nhds_one_swapped, Function.comp_def]

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem IsMaxFilter.sub (hf : IsMaxFilter f l a) (hg : IsMinFilter g l a) :
    IsMaxFilter (fun x => f x - g x) l a

Proof state:
α : Type u
β : Type v
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x => f x - g x) l a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_zero_apply {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') :
    setToSimpleFunc T (0 : α →ₛ F) = 0

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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
⊢ setToSimpleFunc T 0 = 0

Tactic:
cases isEmpty_or_nonempty α <;> simp [setToSimpleFunc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_lt_iff_lt_log (hx : 0 < x) (hy : 0 < y) : x ^ z < y ↔ z * log x < log y

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ^ z < y ↔ z * log x < log y

Tactic:
rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

Result:
no goals