harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_distrib {f g : β → α} (u₁ u₂ : α) (s : Multiset β) :
    (s.map fun x => f x * g x).fold op (u₁ * u₂) = (s.map f).fold op u₁ * (s.map g).fold op u₂ :=
  Multiset.induction_on s (by simp) (fun a b h => by
    rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc])

Proof state:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))

Tactic:
rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
  fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
  ha.assoc, hc.comm (g a), ha.assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_eq_nnrpow {a : A} : sqrt a = a ^ (1 / 2 : ℝ≥0)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ sqrt a = a ^ (1 / 2)

Tactic:
simp only [sqrt, nnrpow, NNReal.coe_inv, NNReal.coe_ofNat, NNReal.rpow_eq_pow]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ cfcₙ (⇑NNReal.sqrt) a = a ^ (1 / 2)

Proof state:
case e_f
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ ⇑NNReal.sqrt = fun x => x.nnrpow (1 / 2)

Tactic:
ext

Result:
case e_f.h.a
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x✝ : ℝ≥0
⊢ ↑(NNReal.sqrt x✝) = ↑(x✝.nnrpow (1 / 2))

Proof state:
case e_f.h.a
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x✝ : ℝ≥0
⊢ ↑(NNReal.sqrt x✝) = ↑(x✝.nnrpow (1 / 2))

Tactic:
exact_mod_cast NNReal.sqrt_eq_rpow _

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ cfcₙ (⇑NNReal.sqrt) a = a ^ (1 / 2)

Tactic:
congr

Result:
case e_f
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ ⇑NNReal.sqrt = fun x => x.nnrpow (1 / 2)
-- Mathlib/GroupTheory/HNNExtension.lean
theorem lift_of (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) (g : G) :
    lift f x hx (of g) = f g

Proof state:
G : Type u_1
inst✝¹ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝ : Group H
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
g : G
⊢ (lift f x hx) (of g) = f g

Tactic:
simp [lift, of]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem disjoint_withBotCoe {I J : WithBot (Box ι)} :
    Disjoint (I : Set (ι → ℝ)) J ↔ Disjoint I J

Proof state:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
I J : WithBot (Box ι)
⊢ Disjoint ↑I ↑J ↔ Disjoint I J

Tactic:
simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]

Result:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
-- Mathlib/SetTheory/Game/Impartial.lean
theorem equiv_iff_add_equiv_zero' (H : PGame) : G ≈ H ↔ G + H ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
H : PGame
⊢ G ≈ H ↔ G + H ≈ 0

Tactic:
rw [equiv_iff_game_eq, ← add_left_cancel_iff, mk'_add_self, ← quot_add, equiv_iff_game_eq,
  Eq.comm, quot_zero]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_point_open (ht₁ : Convex ℝ t) (ht₂ : IsOpen t) (disj : x ∉ t) :
    ∃ f : E →L[ℝ] ℝ, ∀ b ∈ t, f x < f b :=
  let ⟨f, hf⟩ := geometric_hahn_banach_open_point ht₁ ht₂ disj
  ⟨-f, by simpa⟩

Proof state:
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
x : E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : x ∉ t
f : E →L[ℝ] ℝ
hf : ∀ a ∈ t, f a < f x
⊢ ∀ b ∈ t, (-f) x < (-f) b

Tactic:
simpa

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
    (hV : V₁ =ᶠ[𝓝[insert x s] x] V) (hW : W₁ =ᶠ[𝓝[insert x s] x] W) :
    mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[insert x s] x] V
hW : W₁ =ᶠ[𝓝[insert x s] x] W
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s)
  (hV.mlieBracketWithin_vectorField' hW (subset_insert x s))

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_iff_nodup_primeFactorsList {n : ℕ} (h0 : n ≠ 0) :
    Squarefree n ↔ n.primeFactorsList.Nodup

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ Squarefree n ↔ n.primeFactorsList.Nodup

Tactic:
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]

Result:
n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_nonpos_of_nonneg {a : Int} (h : 0 ≤ a) : -a ≤ 0

Proof state:
a : Int
h : 0 ≤ a
this : -a ≤ -0
⊢ -a ≤ 0

Tactic:
rwa [Int.neg_zero] at this

Result:
no goals

Proof state:
a : Int
h : 0 ≤ a
⊢ -a ≤ 0

Tactic:
have : -a ≤ -0 := Int.neg_le_neg h

Result:
a : Int
h : 0 ≤ a
this : -a ≤ -0
⊢ -a ≤ 0
-- Mathlib/Algebra/GeomSum.lean
lemma nat_pow_one_sub_dvd_pow_mul_sub_one (x m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1

Proof state:
x m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1 ^ n

Tactic:
apply nat_sub_dvd_pow_sub_pow (x ^ m) 1

Result:
no goals

Proof state:
x m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1 ^ n

Tactic:
rw [Nat.pow_mul x m n]

Result:
x m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1 ^ n

Proof state:
x m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
nth_rw 2 [← Nat.one_pow n]

Result:
x m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1 ^ n
-- Mathlib/Topology/Inseparable.lean
theorem preimage_image_mk_open (hs : IsOpen s) : mk ⁻¹' (mk '' s) = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) ⊆ s

Tactic:
rintro x ⟨y, hys, hxy⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s

Tactic:
exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) ⊆ s
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem Pullback.continuous_proj (f : B' → B) : Continuous (π F (f *ᵖ E))

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous TotalSpace.proj

Tactic:
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Result:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced TotalSpace.proj inst✝¹

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced TotalSpace.proj inst✝¹

Tactic:
exact inf_le_left

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem card_eq_one_iff : card α = 1 ↔ ∃ x : α, ∀ y, y = x

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x

Tactic:
exact
  ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
   fun ⟨x, hx⟩ =>
    ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
        Subsingleton.elim _ _⟩⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
rw [← card_unit, card_eq]

Result:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp) nsmul_singleton]
lemma singleton_pow (a : α) : ∀ n, ({a} : Set α) ^ n = {a ^ n}
  | 0 => by simp [singleton_one]
  | n + 1 => by simp [pow_succ, singleton_pow _ n]

Proof state:
α : Type u_2
inst✝ : Monoid α
a : α
⊢ {a} ^ 0 = {a ^ 0}

Tactic:
simp [singleton_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isOpen_iff (U : Set (PrimeSpectrum R)) : IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s

Tactic:
simp only [@eq_comm _ Uᶜ]

Result:
R : Type u
inst✝ : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
-- Mathlib/Order/Filter/Partial.lean
theorem tendsto_iff_ptendsto_univ (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
    Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂

Proof state:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂

Tactic:
simp [principal_univ]

Result:
no goals

Proof state:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂

Tactic:
rw [← tendsto_iff_ptendsto]

Result:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem iUnion_mem_generateMeasurableRec {s : Set (Set α)} {i : Ordinal} {f : ℕ → Set α}
    (hf : ∀ n, ∃ j < i, f n ∈ generateMeasurableRec s j) :
    ⋃ n, f n ∈ generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ ⋃ n, f n ∈
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ ⋃ n, f n ∈
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)

Tactic:
exact mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion₂.2 ⟨j, hj, hf⟩⟩, rfl⟩

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem one_left : (1 : Submodule R S).LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Submodule.LinearDisjoint 1 N

Tactic:
rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Function.Injective ⇑(N.subtype ∘ₗ ↑N.lTensorOne)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Function.Injective ⇑(N.subtype ∘ₗ ↑N.lTensorOne)

Tactic:
exact N.injective_subtype.comp N.lTensorOne.injective

Result:
no goals
-- Mathlib/Data/List/Infix.lean
lemma dropSlice_sublist (n m : ℕ) (l : List α) : l.dropSlice n m <+ l :=
  calc
    l.dropSlice n m = take n l ++ drop m (drop n l)

Proof state:
α : Type u_1
n m : ℕ
l : List α
⊢ dropSlice n m l = take n l ++ drop m (drop n l)

Tactic:
rw [dropSlice_eq, drop_drop, Nat.add_comm]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem integrable_toReal_condExpKernel {s : Set Ω} (hs : MeasurableSet s) :
    Integrable (fun ω => (condExpKernel μ m ω s).toReal) μ

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => (((condExpKernel μ m) ω) s).toReal) μ

Tactic:
rw [condExpKernel_eq]

Result:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ((((condDistrib id id μ).comap id ⋯) ω) s).toReal) μ

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Integrable (fun ω => (((condExpKernel μ m) ω) s).toReal) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => (((condExpKernel μ m) ω) s).toReal) μ

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ((((condDistrib id id μ).comap id ⋯) ω) s).toReal) μ

Tactic:
exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma map_mk' (h : M →ₗ[R] N) (x) (s : S) :
    map S f g h (IsLocalizedModule.mk' f x s) = (IsLocalizedModule.mk' g (h x) s)

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ ↑⋯.unit⁻¹ ((g ∘ₗ h) x) = mk' g (h x) s

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ ((map S f g) h) (mk' f x s) = mk' g (h x) s

Tactic:
simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe,
  Function.comp_apply]

Result:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯) ((iso S f).symm (mk' f x s)) = mk' g (h x) s

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯) ((iso S f).symm (mk' f x s)) = mk' g (h x) s

Tactic:
rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]

Result:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ ↑⋯.unit⁻¹ ((g ∘ₗ h) x) = mk' g (h x) s
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem iterate {f : α → α} (hf : LocallyLipschitz f) : ∀ n, LocallyLipschitz f^[n]
  | 0 => by simpa only [pow_zero] using LocallyLipschitz.id
  | n + 1 => by rw [iterate_add, iterate_one]; exact (hf.iterate n).comp hf

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)

Tactic:
exact (hf.iterate n).comp hf

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
⊢ LocallyLipschitz f^[0]

Tactic:
simpa only [pow_zero] using LocallyLipschitz.id

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz f^[n + 1]

Tactic:
rw [iterate_add, iterate_one]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem div_tendsto_leadingCoeff_div_of_degree_eq (hdeg : P.degree = Q.degree) :
    Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 <| P.leadingCoeff / Q.leadingCoeff)

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ ↑P.natDegree = ↑Q.natDegree

Tactic:
simp [hdeg, natDegree]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
simp [tendsto_const_nhds]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem foldr_induction' (f : α → β → β) [LeftCommutative f] (x : β) (q : α → Prop)
    (p : β → Prop) (s : Multiset α) (hpqf : ∀ a b, q a → p b → p (f a b)) (px : p x)
    (q_s : ∀ a ∈ s, q a) : p (foldr f x s)

Proof state:
case empty
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ a ∈ 0, q a
⊢ p (foldr f x 0)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ a ∈ s, q a
⊢ p (foldr f x s)

Tactic:
induction s using Multiset.induction with
| empty => simpa
| cons a s ihs =>
  simp only [forall_mem_cons, foldr_cons] at q_s ⊢
  exact hpqf _ _ q_s.1 (ihs q_s.2)

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ a ∈ s, q a) → p (foldr f x s)
q_s : ∀ a_1 ∈ a ::ₘ s, q a_1
⊢ p (foldr f x (a ::ₘ s))

Tactic:
simp only [forall_mem_cons, foldr_cons] at q_s ⊢

Result:
case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ a ∈ s, q a) → p (foldr f x s)
q_s : q a ∧ ∀ x ∈ s, q x
⊢ p (f a (foldr f x s))

Proof state:
case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ a ∈ s, q a) → p (foldr f x s)
q_s : q a ∧ ∀ x ∈ s, q x
⊢ p (f a (foldr f x s))

Tactic:
exact hpqf _ _ q_s.1 (ihs q_s.2)

Result:
no goals