harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
    x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)

Proof state:
n : Nat
x : BitVec n
i : Nat
⊢ x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)

Tactic:
apply BitVec.eq_of_toInt_eq

Result:
case a
n : Nat
x : BitVec n
i : Nat
⊢ (x.sshiftRight i).toInt = (BitVec.ofInt n (x.toInt >>> i)).toInt

Proof state:
case a
n : Nat
x : BitVec n
i : Nat
⊢ (x.sshiftRight i).toInt = (BitVec.ofInt n (x.toInt >>> i)).toInt

Tactic:
simp [BitVec.sshiftRight]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem nonempty (K : ProperCone 𝕜 E) : (K : Set E).Nonempty :=
  ⟨0, by { simp_rw [SetLike.mem_coe, ← ProperCone.mem_coe, Submodule.zero_mem] }⟩

Proof state:
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
K : ProperCone 𝕜 E
⊢ 0 ∈ ↑K

Tactic:
simp_rw [SetLike.mem_coe, ← ProperCone.mem_coe, Submodule.zero_mem]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_isEmpty [IsEmpty ι] (b : Basis ι R M) :
    b.orientation = positiveOrientation

Proof state:
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ b.orientation = positiveOrientation

Tactic:
rw [Basis.orientation]

Result:
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ rayOfNeZero R b.det ⋯ = positiveOrientation

Proof state:
case e_v
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ b.det = AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
exact b.det_isEmpty

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ rayOfNeZero R b.det ⋯ = positiveOrientation

Tactic:
congr

Result:
case e_v
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ b.det = AlternatingMap.constLinearEquivOfIsEmpty 1
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_left_Ioc (a b c : α) : (Ioc a b).map (c + ·) = Ioc (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
    ((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma IsSelfAdjoint.toReal_spectralRadius_eq_norm {a : A} (ha : IsSelfAdjoint a) :
    (spectralRadius ℝ a).toReal = ‖a‖

Proof state:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ (spectralRadius ℝ a).toReal = ‖a‖

Tactic:
simp [ha.spectrumRestricts.spectralRadius_eq, ha.spectralRadius_eq_nnnorm]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem divRadical_dvd_self (a : E) : divRadical a ∣ a

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ divRadical a ∣ a

Tactic:
exact Dvd.intro (radical a) (divRadical_mul_radical a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_cons_of_neg {a : α} {l : List α} (h : ¬ p a) :
    (a :: l).dropWhile p = a :: l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
h : ¬p a = true
⊢ dropWhile p (a :: l) = a :: l

Tactic:
simp [dropWhile_cons, h]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_strictMonoOn (hf : (setOf p).Finite) :
    StrictMonoOn (nth p) (Set.Iio #hf.toFinset)

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ (hf.toFinset.orderEmbOfFin ⋯) ⟨m, hm⟩ < (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
exact OrderEmbedding.strictMono _ h

Result:
no goals

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
⊢ StrictMonoOn (nth p) (Set.Iio #hf.toFinset)

Tactic:
rintro m (hm : m < _) n (hn : n < _) h

Result:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ nth p m < nth p n

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ nth p m < nth p n

Tactic:
simp only [nth_eq_orderEmbOfFin, *]

Result:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ (hf.toFinset.orderEmbOfFin ⋯) ⟨m, hm⟩ < (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_eq_iff_sq_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
exact natAbs_eq_iff_mul_self_eq

Result:
no goals

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Tactic:
rw [sq, sq]

Result:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem nnnorm_eq_zero' : ‖a‖₊ = 0 ↔ a = 1

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖₊ = 0 ↔ a = 1

Tactic:
rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
lemma succ_add_sub_one (n m : ℕ) : succ m + n - 1 = m + n

Proof state:
n m : ℕ
⊢ m.succ + n - 1 = m + n

Tactic:
rw [succ_add, Nat.add_one_sub_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pos_of_lt_mul_left {a b c : Nat} (h : a < b * c) : 0 < c

Proof state:
a b c : Nat
h : a < b * c
⊢ 0 < b * c

Tactic:
omega

Result:
no goals

Proof state:
a b c : Nat
h : 0 < b * c
⊢ 0 < c

Tactic:
exact Nat.pos_of_mul_pos_left h

Result:
no goals

Proof state:
a b c : Nat
h : a < b * c
⊢ 0 < c

Tactic:
replace h : 0 < b * c := by omega

Result:
a b c : Nat
h : 0 < b * c
⊢ 0 < c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
    (a :: l).modify f (n + 1) = a :: l.modify f n

Proof state:
α : Type u_1
f : α → α
a : α
l : List α
n : Nat
⊢ modify f (n + 1) (a :: l) = a :: modify f n l

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem holderOnWith_one {C : ℝ≥0} {f : X → Y} {s : Set X} :
    HolderOnWith C 1 f s ↔ LipschitzOnWith C f s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C : ℝ≥0
f : X → Y
s : Set X
⊢ HolderOnWith C 1 f s ↔ LipschitzOnWith C f s

Tactic:
simp only [HolderOnWith, LipschitzOnWith, NNReal.coe_one, ENNReal.rpow_one]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma head_drop (p : RelSeries r) (i : Fin (p.length + 1)) : (p.drop i).head = p.toFun i

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).head = p.toFun i

Tactic:
simp [drop, head]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_sub (a b c : Ordinal) : a - b - c = a - (b + c) :=
  eq_of_forall_ge_iff fun d => by rw [sub_le, sub_le, sub_le, add_assoc]

Proof state:
a b c d : Ordinal.{u_4}
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d

Tactic:
rw [sub_le, sub_le, sub_le, add_assoc]

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_image_def {n : ℕ} [DecidableEq α] (f : Fin n → α) :
    Finset.univ.image f = (List.ofFn f).toFinset

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
f : Fin n → α
⊢ image f univ = (List.ofFn f).toFinset

Tactic:
simp [Finset.image]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_insert (has : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
has : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
rw [insert_eq, union_comm, offDiag_union (disjoint_singleton_right.2 has), offDiag_singleton,
  union_empty, union_right_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/RArray.lean
theorem RArray.get_eq_def (a : RArray α) (n : Nat) :
  a.get n = match a with
    | .leaf x => x
    | .branch p l r => (Nat.ble p n).rec (l.get n) (r.get n)

Proof state:
α : Type
a : RArray α
n : Nat
⊢ a.get n =
    match a with
    | leaf x => x
    | branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)

Tactic:
conv => lhs; unfold RArray.get

Result:
α : Type
a : RArray α
n : Nat
⊢ rec (fun x => x) (fun p x x l r => Bool.rec l r (p.ble n)) a =
    match a with
    | leaf x => x
    | branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)

Proof state:
α : Type
a : RArray α
n : Nat
⊢ rec (fun x => x) (fun p x x l r => Bool.rec l r (p.ble n)) a =
    match a with
    | leaf x => x
    | branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
/-- This holds true for all `x : ℂ` because of the junk values `0 / 0 = 0` and `arg 0 = 0`. -/
@[simp] lemma arg_div_self (x : ℂ) : arg (x / x) = 0

Proof state:
x : ℂ
⊢ (x / x).arg = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {x : F} {r : ℝ} (hx : x ≠ 0)
    (hr : r < 0) : ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1

Tactic:
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
  mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0
-- Mathlib/Order/Filter/Prod.lean
theorem prod_assoc (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
  Function.comp_def, Equiv.prodAssoc_symm_apply]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iInter_subset_left (s : ι → Set α) (t : Set β) :
    image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t

Tactic:
exact fun x hx y hy i => mem_image2_of_mem (hx _) hy

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem mapIdxM_eq_mmap_enum [LawfulMonad m] {β} (f : ℕ → α → m β) (as : List α) :
    as.mapIdxM f = List.traverse (uncurry f) (enum as)

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
as : List α
⊢ mapIdxM f as = List.traverse (uncurry f) as.enum

Tactic:
simp only [mapIdxM, mapIdxMGo_eq_mapIdxMAuxSpec, Array.toList_toArray,
  nil_append, mapIdxMAuxSpec, Array.size_toArray, length_nil, id_map', enum]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem nat_lt_card {o} {n : ℕ} : (n : Cardinal) < card o ↔ (n : Ordinal) < o

Proof state:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n.succ ≤ o ↔ succ ↑n ≤ o

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
rw [← succ_le_iff, ← succ_le_iff, ← nat_succ, nat_le_card]

Result:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n.succ ≤ o ↔ succ ↑n ≤ o
-- Mathlib/GroupTheory/Schreier.lean
theorem closure_mul_image_eq_top (hR : IsComplement H R) (hR1 : (1 : G) ∈ R)
    (hS : closure S = ⊤) : closure ((R * S).image fun g =>
      ⟨g * (hR.toRightFun g : G)⁻¹, hR.mul_inv_toRightFun_mem g⟩ : Set H) = ⊤

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)) = ⊤

Tactic:
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map H.subtype ⊤ ≤ closure ((fun x => H.subtype ⟨x * (↑(hR.toRightFun x))⁻¹, ⋯⟩) '' (R * S))

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map H.subtype ⊤ ≤ closure ((fun x => H.subtype ⟨x * (↑(hR.toRightFun x))⁻¹, ⋯⟩) '' (R * S))

Tactic:
exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma nonempty_divisors : (divisors n).Nonempty ↔ n ≠ 0 :=
  ⟨fun ⟨m, hm⟩ hn ↦ by simp [hn] at hm, fun hn ↦ ⟨1, one_mem_divisors.2 hn⟩⟩

Proof state:
n : ℕ
x✝ : n.divisors.Nonempty
hn : n = 0
m : ℕ
hm : m ∈ n.divisors
⊢ False

Tactic:
simp [hn] at hm

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Polynomial.transcendental_X : Transcendental R (X (R := R))

Proof state:
R : Type u
inst✝ : CommRing R
⊢ Transcendental R X

Tactic:
simp [transcendental_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioc_sub_one_sub_one_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
    Ioc (a - 1) (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_of_one_div_eq_one_div (h : 1 / a = 1 / b) : a = b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ a = b

Tactic:
rw [← one_div_one_div a, h, one_div_one_div]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_union_isClosed_of_interior_empty (h₁ : IsClosed s)
    (h₂ : interior t = ∅) : interior (s ∪ t) = interior s :=
  have : interior (s ∪ t) ⊆ s := fun x ⟨u, ⟨(hu₁ : IsOpen u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩ =>
    by_contradiction fun hx₂ : x ∉ s =>
      have : u \ s ⊆ t := fun _ ⟨h₁, h₂⟩ => Or.resolve_left (hu₂ h₁) h₂
      have : u \ s ⊆ interior t

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this✝ : u \ s ⊆ t
this : u \ s ⊆ interior t
⊢ u \ s ⊆ ∅

Tactic:
rwa [h₂] at this

Result:
no goals

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
x✝ : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this : u \ s ⊆ t
⊢ u \ s ⊆ interior t

Tactic:
rwa [(IsOpen.sdiff hu₁ h₁).subset_interior_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem prod_le_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=
  ⟨Embedding.piCongrRight fun i =>
      Classical.choice <| by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
rwa [← mk_out (f i), ← mk_out (g i)] at this

Result:
no goals

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
have := H i

Result:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoIsInitial_hom {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).hom = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).hom = 0

Tactic:
ext

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_down : -down = up

Proof state:
⊢ -down = up

Tactic:
simp [up, down]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem map_ofNat (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : R[X]).map f = ofNat(n) :=
  show (n : R[X]).map f = n by rw [Polynomial.map_natCast]

Proof state:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ map f ↑n = ↑n

Tactic:
rw [Polynomial.map_natCast]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_eq_bot_iff (f : β → α) (S : Finset β) : S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
S : Finset β
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Tactic:
induction' S using Finset.induction with a S _ hi <;> simp [*]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
S : Finset β
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Tactic:
classical induction' S using Finset.induction with a S _ hi <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/ADEInequality.lean
theorem sumInv_pqr (p q r : ℕ+) : sumInv {p, q, r} = (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹

Proof state:
p q r : ℕ+
⊢ sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹

Tactic:
simp only [sumInv, add_zero, insert_eq_cons, add_assoc, map_cons, sum_cons,
  map_singleton, sum_singleton]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_ord_le (c : Cardinal) : c.ord.cof ≤ c

Proof state:
c : Cardinal.{u_1}
⊢ c.ord.cof ≤ c

Tactic:
simpa using cof_le_card c.ord

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_two : Irrational (√2)

Proof state:
⊢ Irrational √2

Tactic:
simpa using Nat.prime_two.irrational_sqrt

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Basic.lean
theorem comp_id (F : C ⥤ D) : F ⋙ 𝟭 D = F

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 D =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ F ⋙ 𝟭 D = F

Tactic:
cases F

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 D =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive sum_nonneg]
lemma one_le_prod_of_one_le : (∀ x ∈ s, (1 : α) ≤ x) → 1 ≤ s.prod :=
  Quotient.inductionOn s fun l hl => by simpa using List.one_le_prod_of_one_le hl

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
l : List α
hl : ∀ x ∈ ⟦l⟧, 1 ≤ x
⊢ 1 ≤ prod ⟦l⟧

Tactic:
simpa using List.one_le_prod_of_one_le hl

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
/--
The closure of a singleton `{a}` in the lower set topology is the right-closed left-infinite
interval (-∞,a].
-/
@[simp] lemma closure_singleton {a : α} : closure {a} = Ici a

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ closure {a} = Ici a

Tactic:
rw [closure_eq_upperClosure, upperClosure_singleton]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(UpperSet.Ici a) = Ici a

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(UpperSet.Ici a) = Ici a

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[simp] lemma sum_count_eq_card {s : Finset α} {m : Multiset α} (hms : ∀ a ∈ m, a ∈ s) :
    ∑ a ∈ s, m.count a = card m

Proof state:
case e_s.h
α : Type u_3
inst✝ : DecidableEq α
s : Finset α
m : Multiset α
hms : ∀ a ∈ m, a ∈ s
a : α
⊢ a ∈ Finset.filter (fun x => count x m ≠ 0) s ↔ a ∈ m.toFinset

Tactic:
simpa using hms a

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Finset α
m : Multiset α
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = m.card

Tactic:
rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]

Result:
α : Type u_3
inst✝ : DecidableEq α
s : Finset α
m : Multiset α
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ x ∈ Finset.filter (fun x => count x m ≠ 0) s, count x m = ∑ a ∈ m.toFinset, count a m

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Finset α
m : Multiset α
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ x ∈ Finset.filter (fun x => count x m ≠ 0) s, count x m = ∑ a ∈ m.toFinset, count a m

Tactic:
congr with a

Result:
case e_s.h
α : Type u_3
inst✝ : DecidableEq α
s : Finset α
m : Multiset α
hms : ∀ a ∈ m, a ∈ s
a : α
⊢ a ∈ Finset.filter (fun x => count x m ≠ 0) s ↔ a ∈ m.toFinset
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapOpcyclesIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv =
      (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv = (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals