harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Lattice.lean
theorem exists_set_mem_of_union_eq_top {ι : Type*} (t : Set ι) (s : ι → Set β)
    (w : ⋃ i ∈ t, s i = ⊤) (x : β) : ∃ i ∈ t, x ∈ s i

Proof state:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
have p : x ∈ ⊤ := Set.mem_univ x

Result:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⊤
⊢ ∃ i ∈ t, x ∈ s i

Proof state:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
simpa using p

Result:
no goals

Proof state:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⊤
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
rw [← w, Set.mem_iUnion] at p

Result:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_add' : Even (m + n) ↔ (Odd m ↔ Odd n)

Proof state:
m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
rw [even_add, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictAnti.map_isGreatest (hf : StrictAnti f) : IsGreatest (f '' s) (f a) ↔ IsLeast s a

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsGreatest (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inr_mul [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] (a₁ a₂ : A) :
    (↑(a₁ * a₂) : Unitization R A) = a₁ * a₂ :=
  ext (mul_zero _).symm <|
    show a₁ * a₂ = (0 : R) • a₂ + (0 : R) • a₁ + a₁ * a₂ by simp only [zero_smul, zero_add]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
a₁ a₂ : A
⊢ a₁ * a₂ = 0 • a₂ + 0 • a₁ + a₁ * a₂

Tactic:
simp only [zero_smul, zero_add]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_left_comm (s t u : Set E) :
    convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

Tactic:
simp_rw [← convexJoin_assoc, convexJoin_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_xor (x y i : Nat) :
    (x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i))

Proof state:
x y i : Nat
⊢ (x ^^^ y).testBit i = (x.testBit i ^^ y.testBit i)

Tactic:
simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_modifyKey_self [EquivBEq α] [Inhabited α] {k fallback : α} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback

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

Tactic:
simp [getKeyD_modifyKey, hl]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem disjoint_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
    ∃ U ∈ 𝓝[≠] x, Disjoint U s :=
  let ⟨V, h, h'⟩ := nhds_inter_eq_singleton_of_mem_discrete hx
  ⟨{x}ᶜ ∩ V, inter_mem_nhdsWithin _ h,
    disjoint_iff_inter_eq_empty.mpr (by rw [inter_assoc, h', compl_inter_self])⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
V : Set X
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
⊢ {x}ᶜ ∩ V ∩ s = ∅

Tactic:
rw [inter_assoc, h', compl_inter_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a

Proof state:
case mk
α : Type u
p : α → Prop
val✝ : α
property✝ : p val✝
h : p ⟨val✝, property✝⟩.val
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ = ⟨val✝, property✝⟩

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Type u
p : α → Prop
a : Subtype fun x => p x
h : p a.val
⊢ ⟨a.val, h⟩ = a

Tactic:
cases a

Result:
case mk
α : Type u
p : α → Prop
val✝ : α
property✝ : p val✝
h : p ⟨val✝, property✝⟩.val
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ = ⟨val✝, property✝⟩
-- Mathlib/Analysis/MellinInversion.lean
theorem rexp_neg_image_aux : rexp ∘ Neg.neg '' univ = Ioi 0

Proof state:
⊢ rexp ∘ Neg.neg '' univ = Ioi 0

Tactic:
rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem generateFrom_insert_univ (S : Set (Set α)) :
    generateFrom (insert Set.univ S) = generateFrom S

Proof state:
α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert univ S) = generateFrom S

Tactic:
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_mul_rpow_neg {a : A} (x : ℝ) (ha : 0 ∉ spectrum ℝ≥0 a)
    (ha' : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
ha' : autoParam (0 ≤ a) _auto✝
⊢ a ^ x * a ^ (-x) = 1

Tactic:
rw [← rpow_add ha, add_neg_cancel, rpow_zero a]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lsub_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → Ordinal.lsub f < c.ord :=
  lsub_lt_ord (by rwa [hc.cof_eq])

Proof state:
ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.map_mk' {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (L R : ListBlank Γ) :
    (Tape.mk' L R).map f = Tape.mk' (L.map f) (R.map f)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
L R : ListBlank Γ
⊢ map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)

Tactic:
simp only [Tape.mk', Tape.map, ListBlank.head_map, eq_self_iff_true, and_self_iff,
  ListBlank.tail_map]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift.principalSeg_top' : lift.principalSeg.{u, u + 1}.top = typeLT Ordinal

Proof state:
⊢ principalSeg.top = type fun x1 x2 => x1 < x2

Tactic:
simp only [lift.principalSeg_top, univ_id]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_one : a / b = 1 ↔ a = b :=
  ⟨eq_of_div_eq_one, fun h ↦ by rw [h, div_self']⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
h : a = b
⊢ a / b = 1

Tactic:
rw [h, div_self']

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- If each function in a finite family has a power series within a ball, then so does the
family as a whole. Note that the positivity assumption on the radius is only needed when
the family is empty. -/
lemma HasFPowerSeriesWithinOnBall.pi
    (hf : ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r) (hr : 0 < r) :
    HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r where
  r_le

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius

Tactic:
exact (hf i).r_le

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
⊢ r ≤ (FormalMultilinearSeries.pi p).radius

Tactic:
apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_false_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : b = False

Proof state:
a b : Prop
h : (a → b) = False
⊢ b = False

Tactic:
simp_all

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem image_interior (h : X ≃ₜ Y) (s : Set X) : h '' interior s = interior (h '' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' interior s = interior (⇑h '' s)

Tactic:
rw [← preimage_symm, preimage_interior]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem zero_comp : comp (0 : R[X]) p = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ comp 0 p = 0

Tactic:
rw [← C_0, C_comp]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem IsLeast.union [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsLeast s a)
    (hb : IsLeast t b) : IsLeast (s ∪ t) (min a b) :=
  ⟨by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1], (ha.isGLB.union hb.isGLB).1⟩

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ a ⊓ b ∈ s ∪ t

Tactic:
rcases le_total a b with h | h <;> simp [h, ha.1, hb.1]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobjectCompIso_inv_arrow (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
    (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow =
      (imageSubobject f).arrow ≫ h

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ h

Tactic:
simp [imageSubobjectCompIso]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem find?_eq_none_iff {p : Fin n → Bool} : find? p = none ↔ ∀ i, ¬ p i

Proof state:
n : Nat
p : Fin n → Bool
⊢ find? p = none ↔ ∀ (i : Fin n), ¬p i = true

Tactic:
rw [← find?_isNone_iff, Option.isNone_iff_eq_none]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
    (as.push a).any p = (as.any p || p a) :=
  any_push' (by simp)

Proof state:
α : Type u_1
inst✝ : BEq α
as : Array α
a : α
p : α → Bool
⊢ (as.push a).size = as.size + 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
/-- Multiplying with `swap R i j` on the left swaps the `i`-th row with the `j`-th row. -/
@[simp]
lemma swap_mul_apply_left (i j : n) (a : m) (g : Matrix n m R) :
    (swap R i j * g) i a = g j a

Proof state:
R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix n m R
⊢ (swap R i j * g) i a = g j a

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mul]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem insert_comm (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s) :=
  ext fun x => by simp only [mem_insert, or_left_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
x : α
⊢ x ∈ insert a (insert b s) ↔ x ∈ insert b (insert a s)

Tactic:
simp only [mem_insert, or_left_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_pair : ({x, y} : Set α).infsep = dist x y

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ {x, y}.infsep = dist x y

Tactic:
rw [infsep_pair_eq_toReal, edist_dist]

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y

Tactic:
exact ENNReal.toReal_ofReal dist_nonneg

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
K : Subgroup N
⊢ H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

Tactic:
simpa only [← Subgroup.toSubmonoid_inj] using Submonoid.prod_eq_bot_iff

Result:
no goals
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_mkRat : {a na n : ℤ} → {b nb d : ℕ} → IsInt a na → IsNat b nb →
    IsRat (na / nb : ℚ) n d → IsRat (mkRat a b) n d
  | _, _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, ⟨_, h⟩ => by rw [Rat.mkRat_eq_div]; exact ⟨_, h⟩

Proof state:
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
rw [Rat.mkRat_eq_div]

Result:
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝

Proof state:
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝

Tactic:
exact ⟨_, h⟩

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.weaken (h : IsBigOWith c l f g') (hc : c ≤ c') : IsBigOWith c' l f g' :=
  IsBigOWith.of_bound <|
    mem_of_superset h.bound fun x hx =>
      calc
        ‖f x‖ ≤ c * ‖g' x‖ := hx
        _ ≤ _

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : x ∈ {x | (fun x => ‖f x‖ ≤ c * ‖g' x‖) x}
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖

Tactic:
gcongr

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
lemma pairwiseDisjoint_iff {ι : Type*} {s : Set ι} {f : ι → Finset α} :
    s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Proof state:
α : Type u_1
inst✝ : DecidableEq α
ι : Type u_4
s : Set ι
f : ι → Finset α
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
  not_disjoint_iff_nonempty_inter]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_succ {x : α} {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i = (x * ∑ i ∈ range n, x ^ i) + 1

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i = x * ∑ i ∈ range n, x ^ i + 1

Tactic:
simp only [mul_sum, ← pow_succ', sum_range_succ', pow_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_le_left_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c

Proof state:
a b c : Int
h : a ≤ b + c
⊢ -b + a ≤ c

Tactic:
rw [Int.add_comm]

Result:
a b c : Int
h : a ≤ b + c
⊢ a + -b ≤ c

Proof state:
a b c : Int
h : a ≤ b + c
⊢ a + -b ≤ c

Tactic:
exact Int.sub_left_le_of_le_add h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem biInter_gt_ball (x : α) (r : ℝ) : ⋂ r' > r, ball x r' = closedBall x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), ball x r' ↔ x✝ ∈ closedBall x r

Tactic:
simp [forall_lt_iff_le']

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), ball x r' = closedBall x r

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), ball x r' ↔ x✝ ∈ closedBall x r
-- Mathlib/Data/ENNReal/Operations.lean
theorem exists_le_of_sum_le {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞}
    (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle

Result:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∀ i ∈ s, g i < f i
⊢ ∑ i ∈ s, g i < ∑ i ∈ s, f i

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∀ i ∈ s, g i < f i
⊢ ∑ i ∈ s, g i < ∑ i ∈ s, f i

Tactic:
apply ENNReal.sum_lt_sum_of_nonempty hs Hle

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_self : Ico a a = 0

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ico a a = 0

Tactic:
rw [Ico, Finset.Ico_self, Finset.empty_val]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
lemma finsuppScalarRight_apply (t : M ⊗[R] (ι →₀ R)) (i : ι) :
    finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
t : M ⊗[R] (ι →₀ R)
i : ι
⊢ ((finsuppScalarRight R M ι) t) i = (TensorProduct.rid R M) ((lTensor M (Finsupp.lapply i)) t)

Tactic:
simp [finsuppScalarRight, finsuppRight_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_of_analyticOn_of_fderivWithin (hf : AnalyticOn 𝕜 f s)
    (h : ContDiffOn 𝕜 ω (fun y ↦ fderivWithin 𝕜 f s y) s) : ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ω (fun y => fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (ω + 1) f s

Tactic:
exact contDiffOn_succ_of_fderivWithin hf.differentiableOn (fun _ ↦ hf) h

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ω (fun y => fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 n f s

Tactic:
suffices ContDiffOn 𝕜 (ω + 1) f s from this.of_le le_top

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ω (fun y => fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (ω + 1) f s
-- Mathlib/Order/Filter/Bases.lean
protected lemma HasBasis.congr (hl : l.HasBasis p s) {p' s'} (hp : ∀ i, p i ↔ p' i)
    (hs : ∀ i, p i → s i = s' i) : l.HasBasis p' s' :=
  ⟨fun t ↦ by simp only [hl.mem_iff, ← hp]; exact exists_congr fun i ↦
    and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl⟩

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s' i ⊆ t

Tactic:
exact exists_congr fun i ↦
and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ t ∈ l ↔ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
simp only [hl.mem_iff, ← hp]

Result:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s' i ⊆ t
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_X_pow_sub_C {n : ℕ} {r : R} : (X ^ n - C r).natDegree = n

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ (X ^ n - C r).natDegree = n

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_filter_mul_prod_filter_not
    (s : Finset α) (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] (f : α → β) :
    (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
⊢ (∏ x ∈ filter (fun x => p x) s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, f x = ∏ x ∈ s, f x

Tactic:
have := Classical.decEq α

Result:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
this : DecidableEq α
⊢ (∏ x ∈ filter (fun x => p x) s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
this : DecidableEq α
⊢ (∏ x ∈ filter (fun x => p x) s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, f x = ∏ x ∈ s, f x

Tactic:
rw [← prod_union (disjoint_filter_filter_neg s s p), filter_union_filter_neg_eq]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_rat_div_iff : Irrational (q / x) ↔ q ≠ 0 ∧ Irrational x

Proof state:
q : ℚ
x : ℝ
⊢ Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Logic/Embedding/Basic.lean
theorem Equiv.toEmbedding_injective : Function.Injective (Equiv.toEmbedding : (α ≃ β) → (α ↪ β)) :=
  fun _ _ h ↦ by rwa [DFunLike.ext'_iff] at h ⊢

Proof state:
α : Sort u
β : Sort v
x✝¹ x✝ : α ≃ β
h : x✝¹.toEmbedding = x✝.toEmbedding
⊢ x✝¹ = x✝

Tactic:
rwa [DFunLike.ext'_iff] at h ⊢

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_subgraphOfAdj [DecidableEq V] {u v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).neighborSet u =
    (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

Tactic:
split_ifs <;> subst_vars <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean
theorem conts_recurrenceAux {gp ppred pred : Pair K} (nth_s_eq : g.s.get? n = some gp)
    (nth_contsAux_eq : g.contsAux n = ppred)
    (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) :
    g.conts (n + 1) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
simp [nth_cont_eq_succ_nth_contAux,
  contsAux_recurrence nth_s_eq nth_contsAux_eq succ_nth_contsAux_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem inl_comp_pushoutObjIso_hom (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    (pushout.inl f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inl (f.app d) (g.app d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ (pushout.inl f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inl (f.app d) (g.app d)

Tactic:
simp [pushoutObjIso]

Result:
no goals