harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Nth.lean
theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
    nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
n : ℕ
⊢ nth p n = ↑((Subtype.orderIsoOfNat (setOf p)) n)

Tactic:
rw [nth, dif_neg hf]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c)

Proof state:
M : Type u_1
a : M
inst✝ : Mul M
h : IsMulCentral a
b c : M
⊢ a * (b * c) = b * (a * c)

Tactic:
simp only [h.comm, h.right_assoc]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem ext_isBase {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
    (h : ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)) : M₁ = M₂

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
⊢ M₁ = M₂

Tactic:
have h' : ∀ B, M₁.IsBase B ↔ M₂.IsBase B :=
  fun B ↦ ⟨fun hB ↦ (h hB.subset_ground).1 hB,
    fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩

Result:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
⊢ M₁ = M₂

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
⊢ M₁ = M₂

Tactic:
ext <;> simp [hE, M₁.indep_iff', M₂.indep_iff', h']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k)

Proof state:
n : Nat
k : Fin n
m : Nat
⊢ (k.addNat m).rev = castAdd m k.rev

Tactic:
rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp]
lemma le_mul_iff_one_le_right [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_left a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
a0 : 0 < a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l]
    (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0

Proof state:
k l : ℕ
inst✝¹ : NeZero k
inst✝ : NeZero l
h : k = l
x : Fin k
⊢ Fin.cast h x = 0 ↔ x = 0

Tactic:
simp [← val_eq_zero_iff]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_succ_zero (m : ℕ) : ack (m + 1) 0 = ack m 1

Proof state:
m : ℕ
⊢ ack (m + 1) 0 = ack m 1

Tactic:
rw [ack]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma mk₀_hom [HasDerivedCategory.{w'} C] (f : X ⟶ Y) :
    (mk₀ f).hom = ShiftedHom.mk₀ _ (by simp) ((singleFunctor C 0).map f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y Z T : C
inst✝ : HasDerivedCategory C
f : X ⟶ Y
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
inst✝ : HasDerivedCategory C
f : X ⟶ Y
⊢ (mk₀ f).hom = ShiftedHom.mk₀ ↑0 ⋯ ((singleFunctor C 0).map f)

Tactic:
apply SmallShiftedHom.equiv_mk₀

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma norm_wInner_le (hw : 0 ≤ w) : ‖⟪f, g⟫_[𝕜, w]‖ ≤ ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫_[ℝ, w] :=
  (norm_sum_le ..).trans_eq <| sum_congr rfl fun i _ ↦ by
    simp [Algebra.smul_def, norm_mul, abs_of_nonneg (hw i)]

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
w : ι → ℝ
f g : ι → 𝕜
hw : 0 ≤ w
i : ι
x✝ : i ∈ univ
⊢ ‖w i • inner (f i) (g i)‖ = w i • inner ((fun i => ‖f i‖) i) ((fun i => ‖g i‖) i)

Tactic:
simp [Algebra.smul_def, norm_mul, abs_of_nonneg (hw i)]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_inf {g₁ g₂ : Filter β} : f ×ˢ (g₁ ⊓ g₂) = (f ×ˢ g₁) ⊓ (f ×ˢ g₂)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂

Tactic:
rw [prod_inf_prod, inf_idem]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_comp_sub (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x => f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

Tactic:
simpa [sub_eq_add_neg] using fderivWithin_comp_add_right (-a)

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mulEquivOfLocalizations_left_inv_apply {k : N ≃* P} (x) :
    f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) x = k x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
k : N ≃* P
x : N
⊢ (f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mem_def {aig : AIG α} {a : α} : (a ∈ aig) ↔ ((.atom a) ∈ aig.decls)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
a : α
⊢ a ∈ aig ↔ Decl.atom a ∈ aig.decls

Tactic:
simp [Membership.mem, Mem]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem ssubset_toFinset {s : Finset α} : s ⊂ ht.toFinset ↔ ↑s ⊂ t

Proof state:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊂ ht.toFinset ↔ ↑s ⊂ t

Tactic:
rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.sInter {S : Set (Set X)} (h : ∀ s ∈ S, IsGδ s) (hS : S.Countable) : IsGδ (⋂₀ S)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ S, IsGδ s
hS : S.Countable
⊢ IsGδ (⋂₀ S)

Tactic:
simpa only [sInter_eq_biInter] using IsGδ.biInter hS h

Result:
no goals
-- Mathlib/Order/Monotone/Monovary.lean
lemma monovaryOn_iff_monovary : MonovaryOn f g s ↔ Monovary (fun i : s ↦ f i) fun i ↦ g i

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ Monovary (fun i => f ↑i) fun i => g ↑i

Tactic:
simp [Monovary, MonovaryOn]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem exp_mul_exp_neg_eq_one [Algebra ℚ A] : exp A * evalNegHom (exp A) = 1

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A * evalNegHom (exp A) = 1

Tactic:
convert exp_mul_exp_eq_exp_add (1 : A) (-1) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
  fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
h : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = x) → ∃ a, a ∈ l₂ ∧ f a = x

Tactic:
exact .imp fun a => .imp_left (@h _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
h : l₁ ⊆ l₂
x : β
⊢ x ∈ map f l₁ → x ∈ map f l₂

Tactic:
simp only [mem_map]

Result:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
h : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = x) → ∃ a, a ∈ l₂ ∧ f a = x
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.closedBall_div (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) :
    closedBall x δ * s = x • cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
simp [div_eq_mul_inv, hs.closedBall_mul hδ]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem exists_clusterPt_of_compactSpace [CompactSpace X] (f : Filter X) [NeBot f] :
    ∃ x, ClusterPt x f

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ f ≤ 𝓟 univ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ ∃ x, ClusterPt x f

Tactic:
simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
@[simp] lemma finsuppAntidiag_empty_of_ne_zero (hn : n ≠ 0) :
    finsuppAntidiag (∅ : Finset ι) n = ∅ :=
  eq_empty_of_forall_not_mem (by simp [@eq_comm _ 0, hn.symm])

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι →₀ μ), x ∉ ∅.finsuppAntidiag n

Tactic:
simp [@eq_comm _ 0, hn.symm]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem neg_add {X Y : C} (a b : X ⟶ Y) : -(a + b) = -a - b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -(a + b) = -a - b

Tactic:
rw [add_def, neg_sub', add_neg]

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem integral_deterministic [MeasurableSingletonClass β] (hg : Measurable g) :
    ∫ x, f x ∂deterministic g hg a = f (g a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
inst✝ : MeasurableSingletonClass β
hg : Measurable g
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
rw [deterministic_apply, integral_dirac _ (g a)]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
@[simp] lemma isInitSeg_empty : IsInitSeg (∅ : Finset (Finset α)) r

Proof state:
α : Type u_1
inst✝ : LinearOrder α
r : ℕ
⊢ IsInitSeg ∅ r

Tactic:
simp [IsInitSeg]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem integrable_stoppedValue_of_mem_finset (hτ : IsStoppingTime ℱ τ)
    (hu : ∀ n, Integrable (u n) μ) {s : Finset ι} (hbdd : ∀ ω, τ ω ∈ s) :
    Integrable (stoppedValue u τ) μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
⊢ Integrable (stoppedValue u τ) μ

Tactic:
simp_rw [← memLp_one_iff_integrable] at hu ⊢

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedValue u τ) 1 μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ s
hu : ∀ (n : ι), MemLp (u n) 1 μ
⊢ MemLp (stoppedValue u τ) 1 μ

Tactic:
exact memLp_stoppedValue_of_mem_finset hτ hu hbdd

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem cofan_inj_naturality_symm {S₁ S₂ : Split C} (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ}
    (A : Splitting.IndexSet Δ) :
    (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f A.1.unop.len ≫ (S₂.s.cofan Δ).inj A

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A

Tactic:
rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem model_infiniteTheory_iff : M ⊨ L.infiniteTheory ↔ Infinite M

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
⊢ M ⊨ L.infiniteTheory ↔ Infinite M

Tactic:
simp [infiniteTheory, infinite_iff, aleph0_le]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_subtype (s : Set β) (f : β → α) : ∏' x : s, f x = ∏' x, s.mulIndicator f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_eq_ediv : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → a.tdiv b = a / b
  | 0, _, _, _ | _, 0, _, _ => by simp
  | succ _, succ _, _, _ => rfl

Proof state:
x✝² : Int
x✝¹ : 0 ≤ x✝²
x✝ : 0 ≤ 0
⊢ x✝².tdiv 0 = x✝² / 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma IsUnit.prod_univ_iff [Fintype α] [CommMonoid β] : IsUnit (∏ a, f a) ↔ ∀ a, IsUnit (f a)

Proof state:
α : Type u_3
β : Type u_4
f : α → β
inst✝¹ : Fintype α
inst✝ : CommMonoid β
⊢ IsUnit (∏ a : α, f a) ↔ ∀ (a : α), IsUnit (f a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) : denote_le ctx (cancel m₁ m₂)

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (m₁.cancel m₂)

Tactic:
apply denote_le_cancelAux

Result:
case h
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx ([].reverse ++ m₁, [].reverse ++ m₂)

Proof state:
case h
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx ([].reverse ++ m₁, [].reverse ++ m₂)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem one_le_ceil_iff : 1 ≤ ⌈a⌉₊ ↔ 0 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem comap_apply (μ : Measure β) (s : Set α) : comap f μ s = μ (f '' s) :=
  calc
    comap f μ s = comap f μ (f ⁻¹' (f '' s))

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ) s = (Measure.comap f μ) (f ⁻¹' (f '' s))

Tactic:
rw [hf.injective.preimage_image]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.map f (Measure.comap f μ)) (f '' s) = μ (f '' s)

Tactic:
rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
  inter_eq_self_of_subset_left (image_subset_range _ _)]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iInf (f : ι → LowerSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl :=
  UpperSet.ext <| by simp only [coe_compl, coe_iInf, compl_iInter, UpperSet.coe_iInf]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → LowerSet α
⊢ ↑(⨅ i, f i).compl = ↑(⨅ i, (f i).compl)

Tactic:
simp only [coe_compl, coe_iInf, compl_iInter, UpperSet.coe_iInf]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive] lemma card_le_card_div_self : s.card ≤ (s / s).card

Proof state:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s / s)

Tactic:
cases s.eq_empty_or_nonempty <;> simp [card_le_card_div_left, *]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Int.lean
theorem ofAdd_neg_one_pow_comm (a : ℤ) (n : ℕ) :
    ((↑(ofAdd (-1 : ℤ)) : ℤₘ₀) ^ (-a)) ^ n = ofAdd (n : ℤ) ^ a

Proof state:
a : ℤ
n : ℕ
⊢ ((↑(ofAdd 1) ^ (-1)) ^ (-a)) ^ n = ↑(ofAdd ↑n) ^ a

Tactic:
simp only [zpow_neg, zpow_one, inv_zpow', inv_inv, coe_zpow]

Result:
a : ℤ
n : ℕ
⊢ (↑(ofAdd 1) ^ a) ^ n = ↑(ofAdd ↑n) ^ a

Proof state:
a : ℤ
n : ℕ
⊢ (↑(ofAdd 1) ^ a) ^ n = ↑(ofAdd ↑n) ^ a

Tactic:
rw [← zpow_natCast, zpow_comm, ← ofAdd_zpow]

Result:
no goals

Proof state:
a : ℤ
n : ℕ
⊢ (↑(ofAdd (-1)) ^ (-a)) ^ n = ↑(ofAdd ↑n) ^ a

Tactic:
rw [ofAdd_zpow (-1)]

Result:
a : ℤ
n : ℕ
⊢ ((↑(ofAdd 1) ^ (-1)) ^ (-a)) ^ n = ↑(ofAdd ↑n) ^ a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_toArray (v : Vector α n) : mk v.toArray v.2 = v

Proof state:
α : Type u_1
n : Nat
v : Vector α n
⊢ { toArray := v.toArray, size_toArray := ⋯ } = v

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
@[simp] lemma himp_eq_himp_iff : b ⇨ a = a ⇨ b ↔ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ a = a ⇨ b ↔ a = b

Tactic:
simp [le_antisymm_iff]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_map_eq {F : Type*} [EquivLike F α β] [MulEquivClass F α β]
    (f : F) {a b : α} : emultiplicity (f a) (f b) = emultiplicity a b

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a b : α
⊢ emultiplicity (f a) (f b) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← map_pow, map_dvd_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
lemma sin_half_eq_sqrt {x : ℝ} (hl : 0 ≤ x) (hr : x ≤ 2 * π) :
    sin (x / 2) = sqrt ((1 - cos x) / 2)

Proof state:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)

Tactic:
apply sin_nonneg_of_nonneg_of_le_pi <;> linarith

Result:
no goals

Proof state:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ sin (x / 2) = √((1 - cos x) / 2)

Tactic:
rw [← abs_sin_half, abs_of_nonneg]

Result:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_zero : (0 : Angle).sign = 0

Proof state:
⊢ sign 0 = 0

Tactic:
rw [sign, sin_zero, _root_.sign_zero]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_singleton_pow (f : R) (n : ℕ) (hn : 0 < n) :
    zeroLocus ({f ^ n} : Set R) = zeroLocus {f} :=
  Set.ext fun x => by simpa using x.2.pow_mem_iff_mem n hn

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f ^ n} ↔ x ∈ zeroLocus {f}

Tactic:
simpa using x.2.pow_mem_iff_mem n hn

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma inv_pow_sub_of_lt (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem card_set_walk_length_eq (u v : V) (n : ℕ) :
    Fintype.card {p : G.Walk u v | p.length = n} = #(G.finsetWalkLength n u v) :=
  Fintype.card_ofFinset (G.finsetWalkLength n u v) fun p => by
    rw [← Finset.mem_coe, coe_finsetWalkLength_eq]

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLength n u v ↔ p ∈ {p | p.length = n}

Tactic:
rw [← Finset.mem_coe, coe_finsetWalkLength_eq]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_sub_eq_sub (a b c : α) : toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c

Tactic:
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add, sub_right_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem zeroLocus_bUnion (s : Set (Set A)) :
    zeroLocus 𝒜 (⋃ s' ∈ s, s' : Set A) = ⋂ s' ∈ s, zeroLocus 𝒜 s'

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set (Set A)
⊢ zeroLocus 𝒜 (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus 𝒜 s'

Tactic:
simp only [zeroLocus_iUnion]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.clm_apply (hc : HasFDerivWithinAt c c' s x)
    (hu : HasFDerivWithinAt u u' s x) :
    HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hu : HasFDerivWithinAt u u' s x
⊢ HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x

Tactic:
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp_hasFDerivWithinAt x (hc.prod hu)

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q

Proof state:
p q : ℝ
h : p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q

Tactic:
simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma map_adj_apply {G : SimpleGraph V} {f : V ↪ W} {a b : V} :
    (G.map f).Adj (f a) (f b) ↔ G.Adj a b

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
a b : V
⊢ (SimpleGraph.map f G).Adj (f a) (f b) ↔ G.Adj a b

Tactic:
simp

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

Proof state:
a b : Int
h : b ≤ a
⊢ min a b = b

Tactic:
rw [Int.min_comm a b]

Result:
a b : Int
h : b ≤ a
⊢ min b a = b

Proof state:
a b : Int
h : b ≤ a
⊢ min b a = b

Tactic:
exact Int.min_eq_left h

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma _root_.CovBy.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∈ t, t.erase a = s

Tactic:
simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.tendsto_nhds' (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
    Filter.Tendsto u f (𝓝 y₀) ↔
    ∀ (s : Finset ι) (ε), 0 < ε → ∀ᶠ x in f, s.sup p (u x - y₀) < ε

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε

Tactic:
simp [hp.hasBasis_ball.tendsto_right_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem ι_colimitIso_hom [HasColimit G] (X : C) :
    colimit.ι (F ⋙ G) X ≫ (colimitIso F G).hom = colimit.ι G (F.obj X)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
X : C
⊢ colimit.ι (F ⋙ G) X ≫ (colimitIso F G).hom = colimit.ι G (F.obj X)

Tactic:
simp [colimitIso]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem le_of_forall_pos_le_add (h : ∀ ε : ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) : a ≤ b

Proof state:
case intro.intro
a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + ↑r < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a

Tactic:
exact ⟨r, hr0, h.trans_le le_top, hr⟩

Result:
no goals

Proof state:
a b : ℝ≥0∞
h : b < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a

Tactic:
rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩

Result:
case intro.intro
a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + ↑r < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a

Proof state:
a b : ℝ≥0∞
h : ∀ (ε : ℝ≥0), 0 < ε → b < ⊤ → a ≤ b + ↑ε
⊢ a ≤ b

Tactic:
contrapose! h

Result:
a b : ℝ≥0∞
h : b < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a