harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
lemma IntegrableOn.finset [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ]
    {s : Finset α} {f : α → E} : IntegrableOn f s μ

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset α
f : α → E
⊢ IntegrableOn f (⋃ x ∈ ↑s, {x}) μ

Tactic:
simp [integrableOn_finset_iUnion, measure_lt_top]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset α
f : α → E
⊢ IntegrableOn f (↑s) μ

Tactic:
rw [← s.toSet.biUnion_of_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset α
f : α → E
⊢ IntegrableOn f (⋃ x ∈ ↑s, {x}) μ
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} :
    ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)

Tactic:
simp only [Inseparable, nhds_prod_eq, prod_inj]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_mono (n : ℕ) {s t : Multiset α} (h : s ≤ t) :
    powersetCard n s ≤ powersetCard n t :=
  leInductionOn h fun {l₁ l₂} h => by
    simp only [powersetCard_coe, coe_le]
    exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

Proof state:
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)

Tactic:
exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetCard n ↑l₁ ≤ powersetCard n ↑l₂

Tactic:
simp only [powersetCard_coe, coe_le]

Result:
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem pow_le_pow_left' {a b : M} (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ, pow_succ]
    exact mul_le_mul' (pow_le_pow_left' hab k) hab

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
rw [pow_succ, pow_succ]

Result:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b

Tactic:
exact mul_le_mul' (pow_le_pow_left' hab k) hab

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem map_range : f.range.map g = (g.comp f).range

Proof state:
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem toSubmodule_injective :
    Function.Injective (toSubmodule : LieSubmodule R L M → Submodule R M) := fun x y h ↦ by
  cases x; cases y; congr

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
x y : LieSubmodule R L M
h : ↑x = ↑y
⊢ x = y

Tactic:
cases x

Result:
case mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y

Proof state:
case mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y

Tactic:
cases y

Result:
case mk.mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }

Proof state:
case mk.mk
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_comm : a / b * c = c / b * a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = c / b * a

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isReflection_inv : cs.IsReflection t⁻¹

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ cs.IsReflection t⁻¹

Tactic:
rwa [ht.inv]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_self_le_self {I : FractionalIdeal S P} (hI : I ≤ 1) : I * I ≤ I

Proof state:
case h.e'_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : I ≤ 1
⊢ I = (fun x => I * x) 1

Tactic:
exact (mul_one I).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : I ≤ 1
⊢ I * I ≤ I

Tactic:
convert mul_left_mono I hI

Result:
case h.e'_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : I ≤ 1
⊢ I = (fun x => I * x) 1
-- Mathlib/Data/List/Sort.lean
theorem sorted_ofFn_iff {r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f

Proof state:
n : ℕ
α : Type u
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i j : Fin (ofFn f).length), i < j → r (f (Fin.cast ⋯ i)) (f (Fin.cast ⋯ j))) ↔
    ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)

Tactic:
exact Iff.symm (Fin.rightInverse_cast _).surjective.forall₂

Result:
no goals

Proof state:
n : ℕ
α : Type u
f : Fin n → α
r : α → α → Prop
⊢ Sorted r (ofFn f) ↔ ((fun x1 x2 => x1 < x2) ⇒ r) f f

Tactic:
simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]

Result:
n : ℕ
α : Type u
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i j : Fin (ofFn f).length), i < j → r (f (Fin.cast ⋯ i)) (f (Fin.cast ⋯ j))) ↔
    ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_finset_iff_subset_smul_finset {s : Finset α} :
    a ∈ stabilizer G s ↔ s ⊆ a • s

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ s ⊆ a • s

Tactic:
rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).le, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.algebraMap (r : R) :
    (algebraMap _ (Matrix ι ι R) r).Represents b (algebraMap _ (Module.End R M) r)

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
r : R
⊢ Represents b ((_root_.algebraMap R (Matrix ι ι R)) r) ((_root_.algebraMap R (Module.End R M)) r)

Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.Represents.one.smul r

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem card_eq_sum_ones (s : Finset α) : #s = ∑ _ ∈ s, 1

Proof state:
α : Type u_3
s : Finset α
⊢ #s = ∑ x ∈ s, 1

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Group.lean
theorem zpow_trick {G : Type*} [Group G] (a b : G) (n m : ℤ) :
    a * b ^ n * b ^ m = a * b ^ (n + m)

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)

Tactic:
rw [mul_assoc, ← zpow_add]

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem max_div_div_right' (a b c : α) : max (a / c) (b / c) = max a b / c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b c : α
⊢ a / c ⊔ b / c = (a ⊔ b) / c

Tactic:
simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_filterₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Bool} (h : Raw.WFImp m.1) : Raw.WFImp (m.filterₘ f).1 where
  buckets_hash_self := isHashSelf_filterₘ h
  size_eq

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
⊢ (m.filterₘ f).val.size = (toListModel (m.filterₘ f).val.buckets).length

Tactic:
simp [filterₘ]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem unit_le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) {m : ∀ i, E i} (h : ‖m‖ ≤ 1) :
    ‖f m‖ ≤ ‖f‖ :=
  (le_opNorm_mul_pow_card_of_le f h).trans <| by simp

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
h : ‖m‖ ≤ 1
⊢ ‖f‖ * 1 ^ Fintype.card ι ≤ ‖f‖

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.tendsto_partialSum_prod {y : E}
    (hf : HasFPowerSeriesOnBall f p x r) (hy : y ∈ EMetric.ball (0 : E) r) :
    Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y))) :=
  (hf.hasFPowerSeriesWithinOnBall (s := univ)).tendsto_partialSum_prod hy (by simp)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesOnBall f p x r
hy : y ∈ EMetric.ball 0 r
⊢ x + y ∈ insert x univ

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem lift_top (K : IntermediateField F E) :
    lift (F := K) ⊤ = K

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ lift ⊤ = K

Tactic:
rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_one_add_of_lt (h : v x < 1) : v (1 + x) = 1

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1

Tactic:
simpa only [v.map_one] using v.map_add_eq_of_lt_left h

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < 1
⊢ v (1 + x) = 1

Tactic:
rw [← v.map_one] at h

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1
-- Mathlib/GroupTheory/Complement.lean
theorem mem_leftTransversals_iff_existsUnique_quotient_mk''_eq :
    S ∈ leftTransversals (H : Set G) ↔
      ∀ q : Quotient (QuotientGroup.leftRel H), ∃! s : S, Quotient.mk'' s.1 = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ (∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q

Tactic:
exact ⟨fun h q => Quotient.inductionOn' q h, fun h g => h (Quotient.mk'' g)⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ S ∈ leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q

Tactic:
simp_rw [mem_leftTransversals_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ←
  QuotientGroup.eq]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ (∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem single_algebraMap_eq_algebraMap_mul_of {A : Type*} [CommSemiring k] [Semiring A]
    [Algebra k A] [Monoid G] (a : G) (b : k) :
    single a (algebraMap k A b) = algebraMap k (MonoidAlgebra A G) b * of A G a

Proof state:
k : Type u₁
G : Type u₂
A : Type u_3
inst✝³ : CommSemiring k
inst✝² : Semiring A
inst✝¹ : Algebra k A
inst✝ : Monoid G
a : G
b : k
⊢ single a ((algebraMap k A) b) = (algebraMap k (MonoidAlgebra A G)) b * (of A G) a

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma ι_tensorObjDesc {A : C} {k : I}
    (f : ∀ (i₁ i₂ : I) (_ : i₁ + i₂ = k), X₁ i₁ ⊗ X₂ i₂ ⟶ A) (i₁ i₂ : I) (hi : i₁ + i₂ = k) :
    ιTensorObj X₁ X₂ i₁ i₂ k hi ≫ tensorObjDesc f = f i₁ i₂ hi

Proof state:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
k : I
f : (i₁ i₂ : I) → i₁ + i₂ = k → (X₁ i₁ ⊗ X₂ i₂ ⟶ A)
i₁ i₂ : I
hi : i₁ + i₂ = k
⊢ ιTensorObj X₁ X₂ i₁ i₂ k hi ≫ tensorObjDesc f = f i₁ i₂ hi

Tactic:
apply ι_mapBifunctorMapObjDesc

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_zero_eval_zero : (ascPochhammer S 0).eval 0 = 1

Proof state:
S : Type u
inst✝ : Semiring S
⊢ eval 0 (ascPochhammer S 0) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Star.lean
@[simp]
lemma addSubmonoid_closure_range_mul_self : closure (range fun x : ℤ ↦ x * x) = nonneg _

Proof state:
⊢ closure (range fun x => x * x) = nonneg ℤ

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow even_two

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

Proof state:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
rwa [RightCancelMonoid.eq_one_of_mul_right h, one_mul] at h

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitUpper_le : I.splitUpper i x ≤ I :=
  withBotCoe_subset_iff.1 <| by simp

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitUpper i x) ⊆ ↑↑I

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem one_lt_norm_iff : 1 < ‖x‖ ↔ 1 < val.v x

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ 1 < ‖x‖ ↔ 1 < v x

Tactic:
simpa only [_root_.map_one] using (Valuation.RankOne.strictMono val.v).lt_iff_lt (a := 1)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem lintegral_snd (κ : Kernel α (β × γ)) (a : α) {g : γ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂snd κ a = ∫⁻ bc : β × γ, g bc.snd ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a

Tactic:
rw [snd_eq, lintegral_map _ measurable_snd a hg]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
@[simp] lemma toNat_bne_zero (b : Bool) : (b.toNat != 0) =  b

Proof state:
b : Bool
⊢ (b.toNat != 0) = b

Tactic:
simp [bne]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem nsmul_add_modEq (n : ℕ) : n • p + a ≡ a [PMOD p] :=
  ⟨-n, by simp [← sub_sub]⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a : α
n : ℕ
⊢ a - (n • p + a) = -↑n • p

Tactic:
simp [← sub_sub]

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem card_Ico :
    #(Finset.Ico s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ico s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1

Tactic:
rw [Finset.card_Ico_eq_card_Icc_sub_one, card_Icc]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_algebraMap (r : vR.integer) :
    ((algebraMap vR.integer vA.integer) r : A) = (algebraMap R A) (r : R)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
r : ↥vR.integer
⊢ ↑((algebraMap ↥vR.integer ↥vA.integer) r) = (algebraMap R A) ↑r

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem Convex.image_sub_lt_mul_sub_of_deriv_lt {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C}
    (lt_hf' : ∀ x ∈ interior D, deriv f x < C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D)
    (hxy : x < y) : f y - f x < C * (y - x) :=
  have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.neg, neg_lt_neg_iff]
    exact lt_hf' x hx
  by linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ -C < deriv (fun y => -f y) x

Tactic:
rw [deriv.neg, neg_lt_neg_iff]

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < C

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x
⊢ f y - f x < C * (y - x)

Tactic:
linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]

Result:
no goals

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < C

Tactic:
exact lt_hf' x hx

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.update [DecidableEq ι] {l : Filter Y} {f : Y → ∀ i, π i} {x : ∀ i, π i}
    (hf : Tendsto f l (𝓝 x)) (i : ι) {g : Y → π i} {xi : π i} (hg : Tendsto g l (𝓝 xi)) :
    Tendsto (fun a => update (f a) i (g a)) l (𝓝 <| update x i xi) :=
  tendsto_pi_nhds.2 fun j => by rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply_nhds]

Proof state:
Y : Type v
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → π i
x : (i : ι) → π i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → π i
xi : π i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 => Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply_nhds]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_mul_div_succ (a : ℕ) (hb : 0 < b) : a < b * (a / b + 1)

Proof state:
b a : ℕ
hb : 0 < b
⊢ a / b < a / b + 1

Tactic:
exact lt_succ_self _

Result:
no goals

Proof state:
b a : ℕ
hb : 0 < b
⊢ a < b * (a / b + 1)

Tactic:
rw [Nat.mul_comm, ← Nat.div_lt_iff_lt_mul hb]

Result:
b a : ℕ
hb : 0 < b
⊢ a / b < a / b + 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (k == a) = false) : getEntry a (⟨k, v⟩ :: l) h₁ =
      getEntry a l (containsKey_of_containsKey_cons (v := v) h₁ h₂)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
⊢ getEntry a (⟨k, v⟩ :: l) h₁ = getEntry a l ⋯

Tactic:
simp [getEntry, getEntry?_cons_of_false h₂]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem diag_mem_sym2_iff : Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
simp [diag_mem_sym2_mem_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_above {i : Fin (n + 1)} {m : Fin n} (h : i ≤ Fin.castSucc m) :
    (finSuccEquiv' i) m.succ = some m

Proof state:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) m.succ = some m

Tactic:
rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat)

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = decide (2 ^ (w - 1) ≤ x.toNat)

Tactic:
simp [msb_eq_getLsbD_last, getLsbD_last]

Result:
no goals