harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioo_add_one_right_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ioo a (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Basic.lean
@[reassoc (attr := simp)]
lemma π₁Toπ₂_comp_π₂Toπ₃ : (π₁Toπ₂ : (_ : _ ⥤ C) ⟶ _) ≫ π₂Toπ₃ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
⊢ π₁Toπ₂ ≫ π₂Toπ₃ = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem empty_mem_powerset (s : Finset α) : ∅ ∈ powerset s

Proof state:
α : Type u_1
s : Finset α
⊢ ∅ ∈ s.powerset

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem eq_whisker {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : f ≫ h = g ≫ h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_zero : (0 : R[X]).smeval x = 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 0 x = 0

Tactic:
simp only [smeval_eq_sum, smul_pow, sum_zero_index]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a

Proof state:
a : ℤ
⊢ (↑a.natAbs).natAbs = a.natAbs

Tactic:
rfl

Result:
no goals

Proof state:
a : ℤ
⊢ |a|.natAbs = a.natAbs

Tactic:
rw [abs_eq_natAbs]

Result:
a : ℤ
⊢ (↑a.natAbs).natAbs = a.natAbs
-- Mathlib/Data/Num/Lemmas.lean
theorem to_nat_eq_succ_pred (n : PosNum) : (n : ℕ) = n.pred' + 1

Proof state:
n : PosNum
⊢ ↑n = ↑n.pred' + 1

Tactic:
rw [← Num.succ'_to_nat, n.succ'_pred']

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffAt.continuousAt (h : ContDiffAt 𝕜 n f x) : ContinuousAt f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffAt 𝕜 n f x
⊢ ContinuousAt f x

Tactic:
simpa [continuousWithinAt_univ] using h.continuousWithinAt

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_cons_nil_eq_subgraphOfAdj (h : G.Adj u v) :
    (cons h nil).toSubgraph = G.subgraphOfAdj h

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).toSubgraph = G.subgraphOfAdj h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[mono, gcongr, bound]
lemma div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a / c ≤ b / c

Tactic:
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * (1 / c) ≤ b * (1 / c)

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * (1 / c) ≤ b * (1 / c)

Tactic:
exact mul_le_mul_of_nonneg_right hab (one_div_nonneg.2 hc)

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Defs.lean
@[aesop safe apply (rule_sets := [SetLike])]
lemma nnqsmul_mem (s : S) (q : ℚ≥0) (hx : x ∈ s) : q • x ∈ s

Proof state:
K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ≥0
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
simpa only [NNRat.smul_def] using mul_mem (nnratCast_mem _ _) hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldl_subtype {p : α → Prop} {l : Vector { x // p x } n}
    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
    l.foldl f x = l.unattach.foldl g x

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : Array { x // p x }
⊢ foldl f x { toArray := l, size_toArray := ⋯ } = foldl g x { toArray := l, size_toArray := ⋯ }.unattach

Tactic:
simp [Array.foldl_subtype hf]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
p : α → Prop
l : Vector { x // p x } n
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : Array { x // p x }
⊢ foldl f x { toArray := l, size_toArray := ⋯ } = foldl g x { toArray := l, size_toArray := ⋯ }.unattach
-- Mathlib/Data/List/Cycle.lean
theorem next_reverse_eq_prev' (s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) :
    s.reverse.next hs x hx = s.prev (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.next hs x hx = s.prev ⋯ x ⋯

Tactic:
simp [← prev_reverse_eq_next]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem subset_insert_iff_of_not_mem (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
rw [subset_insert_iff, erase_eq_of_not_mem h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.isEmpty = l.isEmpty

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (insertMany empty l).val.val.isEmpty = l.isEmpty

Tactic:
simp [isEmpty_insertMany_list _ Raw.WF.empty₀]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_empty (w : ι → k) (p : ι → P) : (∅ : Finset ι).weightedVSub p w = (0 : V)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
⊢ (∅.weightedVSub p) w = 0

Tactic:
simp [weightedVSub_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_sub_right_distrib (a b c : α) : (a - b) * c = a * c - b * c

Proof state:
α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem abs_eq_normalize (z : ℤ) : |z| = normalize z

Proof state:
z : ℤ
⊢ |z| = normalize z

Tactic:
cases le_total 0 z <;>
simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_mul_ι (a : M) (b : CliffordAlgebra Q) :
    b * ι Q a⌊d = d a • b - b⌊d * ι Q a

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractRight (b * (ι Q) a)) d = d a • b - (contractRight b) d * (ι Q) a

Tactic:
rw [contractRight_eq, reverse.map_mul, reverse_ι, contractLeft_ι_mul, map_sub, map_smul,
  reverse_reverse, reverse.map_mul, reverse_ι, contractRight_eq]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem ball_add_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) :
    ball a ε + closedBall b δ = ball (a + b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_add]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma continuousAt_iff' (hf : IsInducing f) {x : X} (h : range f ∈ 𝓝 (f x)) :
    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
theorem map_intCast' [AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β]
    [AddMonoidHomClass F α β] (f : F) (h₁ : f 1 = 1) : ∀ n : ℤ, f n = n :=
  eq_intCast' ((f : α →+ β).comp <| Int.castAddHom _) (by simpa)

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : AddGroupWithOne α
inst✝² : AddGroupWithOne β
inst✝¹ : FunLike F α β
inst✝ : AddMonoidHomClass F α β
f : F
h₁ : f 1 = 1
⊢ ((↑f).comp (castAddHom α)) 1 = 1

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_eq_one_iff_eq_inv {a : α} : a * u = 1 ↔ a = ↑u⁻¹

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a = ↑u⁻¹

Tactic:
rw [← mul_inv_eq_one, inv_inv]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_ne_zero_iff {θ : Angle} : (2 : ℕ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← two_nsmul_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_one : GammaIntegral 1 = 1

Proof state:
⊢ GammaIntegral 1 = 1

Tactic:
simpa only [← ofReal_one, GammaIntegral_ofReal, ofReal_inj, sub_self, rpow_zero,
  mul_one] using integral_exp_neg_Ioi_zero

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicator_zero {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α}
    (x_out : x ∉ thickening δ E) : thickenedIndicator δ_pos E x = 0

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ (thickenedIndicator δ_pos E) x = 0

Tactic:
rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, zero_toNNReal]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atTop_mul_const_of_neg' (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atBot

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot

Tactic:
simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem HasColimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
    (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) :
    colimit.ι F j ≫ (HasColimit.isoOfEquivalence e w).hom =
      F.map (e.unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ colimit.ι F j ≫ (isoOfEquivalence e w).hom =
    F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))

Tactic:
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem diff_iInter (s : Set β) (t : ι → Set β) : (s \ ⋂ i, t i) = ⋃ i, s \ t i

Proof state:
β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ s \ ⋂ i, t i = ⋃ i, s \ t i

Tactic:
rw [diff_eq, compl_iInter, inter_iUnion]

Result:
β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ ⋃ i, s ∩ (t i)ᶜ = ⋃ i, s \ t i

Proof state:
β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ ⋃ i, s ∩ (t i)ᶜ = ⋃ i, s \ t i

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Tower.lean
theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : R[X]) :
    aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ (aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0

Tactic:
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
  iff_false_intro (one_ne_zero' B), or_false]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableAt_iff_target {x : M} :
    MDifferentiableAt I I' f x ↔
      ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (extChartAt I' (f x) ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
⊢ MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (↑(extChartAt I' (f x)) ∘ f) x

Tactic:
rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
  mdifferentiableWithinAt_iff_target, continuousWithinAt_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem mem_sup_left {S T : Subsemigroup M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left

Result:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem card_sym2 (s : Finset α) : s.sym2.card = Nat.choose (s.card + 1) 2

Proof state:
α : Type u_1
s : Finset α
⊢ #s.sym2 = (#s + 1).choose 2

Tactic:
rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
lemma IsFiniteKernel.integrable (μ : Measure α) [IsFiniteMeasure μ]
    (κ : Kernel α β) [IsFiniteKernel κ] {s : Set β} (hs : MeasurableSet s) :
    Integrable (fun x ↦ (κ x s).toReal) μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ‖((κ x) s).toReal‖ ≤ (IsFiniteKernel.bound κ).toReal

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ((κ x) s).toReal ≤ (IsFiniteKernel.bound κ).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x => ((κ x) s).toReal) μ

Tactic:
refine Integrable.mono' (integrable_const (IsFiniteKernel.bound κ).toReal)
  ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
  (ae_of_all μ fun x ↦ ?_)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ‖((κ x) s).toReal‖ ≤ (IsFiniteKernel.bound κ).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ((κ x) s).toReal ≤ (IsFiniteKernel.bound κ).toReal

Tactic:
exact ENNReal.toReal_mono (IsFiniteKernel.bound_ne_top _) (Kernel.measure_le_bound _ _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
    (f : { x // P x } → β) :
    (o.attachWith P H).map f =
      o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩)

Proof state:
α : Type u_1
β : Type u_2
o : Option α
P : α → Prop
H : ∀ (a : α), a ∈ o → P a
f : { x // P x } → β
⊢ Option.map f (o.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) o ⋯

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem surjective_toEventualRanges (h : F.IsMittagLeffler) ⦃i j⦄ (f : i ⟶ j) :
    (F.toEventualRanges.map f).Surjective := fun ⟨x, hx⟩ => by
  obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx
  exact ⟨⟨y, hy⟩, rfl⟩

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x✝ : F.toEventualRanges.obj j
x : F.obj j
hx : x ∈ F.eventualRange j
⊢ ∃ a, F.toEventualRanges.map f a = ⟨x, hx⟩

Tactic:
obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx

Result:
case intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x✝ : F.toEventualRanges.obj j
y : F.obj i
hy : y ∈ F.eventualRange i
hx : F.map f y ∈ F.eventualRange j
⊢ ∃ a, F.toEventualRanges.map f a = ⟨F.map f y, hx⟩

Proof state:
case intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x✝ : F.toEventualRanges.obj j
y : F.obj i
hy : y ∈ F.eventualRange i
hx : F.map f y ∈ F.eventualRange j
⊢ ∃ a, F.toEventualRanges.map f a = ⟨F.map f y, hx⟩

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_arrow_comp : factorThruImageSubobject f ≫ (imageSubobject f).arrow = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow = f

Tactic:
simp [factorThruImageSubobject, imageSubobject_arrow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β k} {f : β k → β k} :
    (m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
fallback : β k
f : β k → β k
⊢ (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback

Tactic:
simp_to_model [modify] using List.getValueCastD_modifyKey_self

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem zero_opow_le (a : Ordinal) : (0 : Ordinal) ^ a ≤ 1

Proof state:
a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
rw [zero_opow']

Result:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1

Proof state:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1

Tactic:
exact sub_le_self 1 a

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem pi_trans (ei : ∀ i, PartialEquiv (αi i) (βi i)) (ei' : ∀ i, PartialEquiv (βi i) (γi i)) :
    (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = .pi fun i ↦ (ei i).trans (ei' i)

Proof state:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
⊢ (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i => (ei i).trans (ei' i)

Tactic:
ext <;> simp [forall_and]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem HasProd.mul_isCompl {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd f (a * b)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : IsCompl s t
ha : HasProd (f ∘ Subtype.val) a
hb : HasProd (f ∘ Subtype.val) b
⊢ HasProd f (a * b)

Tactic:
simpa [← hs.compl_eq] using
  (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb)

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_sum_le (f : ι → S[X]) :
    natDegree (∑ i ∈ s, f i) ≤ s.fold max 0 (natDegree ∘ f)

Proof state:
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
⊢ (∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (natDegree ∘ f) s

Tactic:
simpa using natDegree_multiset_sum_le (s.val.map f)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma le_traceDual_comm {I J : Submodule B L} :
    I ≤ Jᵛ ↔ J ≤ Iᵛ

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ J ≤ Iᵛ

Tactic:
rw [le_traceDual, mul_comm, ← le_traceDual]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
/-- See `MemLp.prod` for the unapplied version. -/
protected lemma MemLp.prod' (hf : ∀ i ∈ s, MemLp (f i) (p i) μ) :
    MemLp (fun ω ↦ ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Proof state:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp (fun ω => ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
simpa [Finset.prod_fn] using MemLp.prod hf

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.of_pow {n : ℕ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℕ
x✝ : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m) x = y
⊢ (f ^ (↑n * m)) x = y

Tactic:
simp [zpow_mul, h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem toFinset_sum_count_nsmul_eq (s : Multiset α) :
    ∑ a ∈ s.toFinset, s.count a • {a} = s

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
⊢ ∑ a ∈ s.toFinset, count a s • {a} = s

Tactic:
rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem intCast_re (n : ℤ) : re (n : K) = n

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑n = ↑n

Tactic:
rw [← ofReal_intCast, ofReal_re]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_setWidth' (x : BitVec w) (h : w ≤ v) : (x.setWidth' h).msb = (decide (0 < v) && x.getLsbD (v - 1))

Proof state:
w v : Nat
x : BitVec w
h : w ≤ v
⊢ (setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Tactic:
rw [setWidth'_eq, msb_setWidth]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isClosedMap_iff_closure_image :
    IsClosedMap f ↔ ∀ s, closure (f '' s) ⊆ f '' closure s :=
  ⟨IsClosedMap.closure_image_subset, fun hs c hc =>
    isClosed_of_closure_subset <|
      calc
        closure (f '' c) ⊆ f '' closure c := hs c
        _ = f '' c

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s
c : Set X
hc : IsClosed c
⊢ f '' closure c = f '' c

Tactic:
rw [hc.closure_eq]

Result:
no goals