harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem tendsto_self_mul_Gamma_nhds_zero : Tendsto (fun z : ℂ => z * Gamma z) (𝓝[≠] 0) (𝓝 1)

Proof state:
⊢ 𝓝 1 = 𝓝 (Gamma (0 + 1))

Tactic:
simp only [zero_add, Complex.Gamma_one]

Result:
no goals

Proof state:
⊢ Tendsto (fun z => z * Gamma z) (𝓝[≠] 0) (𝓝 1)

Tactic:
rw [show 𝓝 (1 : ℂ) = 𝓝 (Gamma (0 + 1)) by simp only [zero_add, Complex.Gamma_one]]

Result:
⊢ Tendsto (fun z => z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (0 + 1)))

Proof state:
case convert_1
m : ℕ
⊢ -↑m ≤ 0

Tactic:
exact neg_nonpos.mpr (Nat.cast_nonneg _)

Result:
no goals

Proof state:
case convert_1
m : ℕ
⊢ ¬1 = -↑m

Tactic:
refine (lt_of_le_of_lt ?_ zero_lt_one).ne'

Result:
case convert_1
m : ℕ
⊢ -↑m ≤ 0

Proof state:
⊢ Tendsto (fun z => z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (0 + 1)))

Tactic:
convert (Tendsto.mono_left _ nhdsWithin_le_nhds).congr'
  (eventuallyEq_of_mem self_mem_nhdsWithin Complex.Gamma_add_one) using 1

Result:
case convert_1

⊢ Tendsto (fun x => Gamma (x + 1)) (𝓝 0) (𝓝 (Gamma (0 + 1)))

Proof state:
case convert_1

⊢ ContinuousAt Gamma (0 + 1)

Tactic:
refine (Complex.differentiableAt_Gamma _ fun m => ?_).continuousAt

Result:
case convert_1
m : ℕ
⊢ 0 + 1 ≠ -↑m

Proof state:
case convert_1
m : ℕ
⊢ 0 + 1 ≠ -↑m

Tactic:
rw [zero_add, ← ofReal_natCast, ← ofReal_neg, ← ofReal_one, Ne, ofReal_inj]

Result:
case convert_1
m : ℕ
⊢ ¬1 = -↑m

Proof state:
case convert_1

⊢ Tendsto (fun x => Gamma (x + 1)) (𝓝 0) (𝓝 (Gamma (0 + 1)))

Tactic:
refine ContinuousAt.comp (g := Gamma) ?_ (continuous_id.add continuous_const).continuousAt

Result:
case convert_1

⊢ ContinuousAt Gamma (0 + 1)
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_update_of_mem {i : δ} (hi : i ∈ s)
    (f : (∀ i, π i) → ℝ≥0∞) (x : ∀ i, π i) (y : π i) :
    (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∂μ) x

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
j : δ
hj : j ∉ s
⊢ update x i y j = x j

Tactic:
have : j ≠ i := by rintro rfl; exact hj hi

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
j : δ
hj : j ∉ s
this : j ≠ i
⊢ update x i y j = x j

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
j : δ
hj : j ∉ s
hi : j ∈ s
y : π j
⊢ False

Tactic:
exact hj hi

Result:
no goals

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
j : δ
hj : j ∉ s
this : j ≠ i
⊢ update x i y j = x j

Tactic:
apply update_of_ne this

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
j : δ
hj : j ∉ s
⊢ j ≠ i

Tactic:
rintro rfl

Result:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
j : δ
hj : j ∉ s
hi : j ∈ s
y : π j
⊢ False

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
⊢ (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∂μ) x

Tactic:
apply lmarginal_congr

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
⊢ ∀ i_1 ∉ s, update x i y i_1 = x i_1

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
⊢ ∀ i_1 ∉ s, update x i y i_1 = x i_1

Tactic:
intro j hj

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
hi : i ∈ s
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
y : π i
j : δ
hj : j ∉ s
⊢ update x i y j = x j
-- Mathlib/Data/Nat/Digits.lean
theorem digits_append_zeroes_append_digits {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) :
    digits b n ++ List.replicate k 0 ++ digits b m =
    digits b (n + b ^ ((digits b n).length + k) * m)

Proof state:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m

Tactic:
ring

Result:
no goals

Proof state:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
rw [List.append_assoc, ← digits_base_pow_mul hb hm]

Result:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)

Proof state:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]

Result:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
/-- Two group homomorphisms `G →* G'` are equal if and only if they agree on a generator of `G`. -/
@[to_additive
   "Two homomorphisms `G →+ G'` of additive groups are equal if and only if they agree
   on a generator of `G`."]
lemma MonoidHom.eq_iff_eq_on_generator (f₁ f₂ : G →* G') : f₁ = f₂ ↔ f₁ g = f₂ g

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
⊢ f₁ x = f₂ x

Tactic:
obtain ⟨n, hn⟩ := mem_zpowers_iff.mp <| hg x

Result:
case intro
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ x = f₂ x

Proof state:
case intro
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ x = f₂ x

Tactic:
rw [← hn, map_zpow, map_zpow, H]

Result:
no goals

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
⊢ (∀ (x : G), f₁ x = f₂ x) ↔ f₁ g = f₂ g

Tactic:
refine ⟨fun H ↦ H g, fun H x ↦ ?_⟩

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
⊢ f₁ x = f₂ x

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
⊢ f₁ = f₂ ↔ f₁ g = f₂ g

Tactic:
rw [DFunLike.ext_iff]

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
⊢ (∀ (x : G), f₁ x = f₂ x) ↔ f₁ g = f₂ g
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_cancel (a b : G) : a * (b / a) = b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b

Tactic:
rw [← mul_div_assoc, mul_div_cancel_left]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.of_dvd {f g : R[X]} (hf : f.Separable) (hfg : g ∣ f) : g.Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
⊢ g.Separable

Tactic:
rcases hfg with ⟨f', rfl⟩

Result:
case intro
R : Type u
inst✝ : CommSemiring R
g f' : R[X]
hf : (g * f').Separable
⊢ g.Separable

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
g f' : R[X]
hf : (g * f').Separable
⊢ g.Separable

Tactic:
exact Separable.of_mul_left hf

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.dest_map {α β : TypeVec n} (g : α ⟹ β) (x : P.M α) :
    M.dest P (g <$$> x) = (appendFun g fun x => g <$$> x) <$$> M.dest P x

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
x : P.M α
⊢ dest P (g <$$> x) = (g ::: fun x => g <$$> x) <$$> dest P x

Tactic:
obtain ⟨a, f⟩ := x

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P (g <$$> ⟨a, f⟩) = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
conv =>
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ =
    ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
      splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
        ((fun x => g <$$> x) ∘ fun x => ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P (g <$$> ⟨a, f⟩) = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
rw [map_eq]

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ = (g ::: fun x => g <$$> x) <$$> dest P ⟨a, f⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ dest P ⟨a, g ⊚ f⟩ =
    ⟨(PFunctor.M.dest ⟨a, f⟩.fst).fst,
      splitFun (g ⊚ pathDestLeft P ⋯ ⟨a, f⟩.snd)
        ((fun x => g <$$> x) ∘ fun x => ⟨(PFunctor.M.dest ⟨a, f⟩.fst).snd x, pathDestRight P ⋯ ⟨a, f⟩.snd x⟩)⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_eq_natCast_iff (a b c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [MOD c]

Proof state:
a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]

Tactic:
simpa [Int.natCast_modEq_iff] using ZMod.intCast_eq_intCast_iff a b c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_append {l₁ l₂ : Array α} :
    (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p)

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
toList✝ : List α
⊢ find? p ({ toList := toList✝ } ++ l₂) = (find? p { toList := toList✝ }).or (find? p l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
p : α → Bool
toList✝¹ toList✝ : List α
⊢ find? p ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    (find? p { toList := toList✝¹ }).or (find? p { toList := toList✝ })

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
⊢ find? p (l₁ ++ l₂) = (find? p l₁).or (find? p l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
toList✝ : List α
⊢ find? p ({ toList := toList✝ } ++ l₂) = (find? p { toList := toList✝ }).or (find? p l₂)

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
toList✝¹ toList✝ : List α
⊢ find? p ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    (find? p { toList := toList✝¹ }).or (find? p { toList := toList✝ })

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem sin_angle_sub_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Tactic:
rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma isIso_fst_of_isIso (h : IsPullback fst snd f g) [IsIso g] : IsIso fst

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso g
⊢ IsIso fst

Tactic:
have := h.hasPullback

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso g
this : HasPullback f g
⊢ IsIso fst

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso g
this : HasPullback f g
⊢ IsIso fst

Tactic:
rw [← h.isoPullback_hom_fst]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_smooth_zero_one_nhds_of_isClosed [T2Space M] [NormalSpace M] [SigmaCompactSpace M]
    {s t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
    ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, (∀ᶠ x in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ x in 𝓝ˢ t, f x = 1) ∧
      ∀ x, f x ∈ Icc 0 1

Proof state:
case intro.intro.intro
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
u : Set M
u_op : IsOpen u
hsu : s ⊆ u
hut : closure u ⊆ tᶜ
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
  (subset_compl_comm.mp hut)

Result:
case intro.intro.intro.intro.intro.intro
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
u : Set M
u_op : IsOpen u
hsu : s ⊆ u
hut : closure u ⊆ tᶜ
v : Set M
v_op : IsOpen v
htv : t ⊆ v
hvu : closure v ⊆ (closure u)ᶜ
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
-- Mathlib/Data/Nat/Basic.lean
protected lemma div_mul_div_le (a b c d : ℕ) :
    (a / b) * (c / d) ≤ (a * c) / (b * d)

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b * (c / d * d) ≤ a * c

Tactic:
apply Nat.mul_le_mul <;> apply div_mul_le_self

Result:
no goals

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) ≤ a * c / (b * d)

Tactic:
rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]

Result:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a * c

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a / b * b * (c / d * d)

Tactic:
apply Nat.le_of_eq

Result:
case p
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) = a / b * b * (c / d * d)

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)

Tactic:
simp [hd]

Result:
no goals

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a * c

Tactic:
transitivity ((a / b) * b) * ((c / d) * d)

Result:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a / b * b * (c / d * d)

a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b * (c / d * d) ≤ a * c

Proof state:
case p
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) = a / b * b * (c / d * d)

Tactic:
simp only [Nat.mul_assoc, Nat.mul_left_comm]

Result:
no goals

Proof state:
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)

Tactic:
simp [hb]

Result:
no goals

Proof state:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)

Tactic:
have hbd : b * d ≠ 0 := Nat.mul_ne_zero hb hd

Result:
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
-- Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
theorem contDiffOn_piLp :
    ContDiffOn 𝕜 n f t ↔ ∀ i, ContDiffOn 𝕜 n (fun x => f x i) t

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem sSup_within_of_ordConnected {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty)
    (h_bdd : BddAbove t) : sSup ((↑) '' t : Set α) ∈ s

Proof state:
case intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
refine hs.out c.2 B.2 ⟨?_, ?_⟩

Result:
case intro.intro.refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

case intro.intro.refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B

Proof state:
case intro.intro.refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

Tactic:
exact (Subtype.mono_coe s).le_csSup_image hct ⟨B, hB⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht

Result:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s

Proof state:
case intro.intro.refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B

Tactic:
exact (Subtype.mono_coe s).csSup_image_le ⟨c, hct⟩ hB

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd

Result:
case intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G}
    (hf : Integrable f μ) {g : G → F} (hg : g 0 = 0) :
    (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' {x}) (g x)

Proof state:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∑ c ∈ filter (fun b => g b = g (f a)) f.range, (T (⇑f ⁻¹' {c})) (g (f a)) =
    ∑ j ∈ filter (fun b => g b = g (f a)) f.range, (T (⇑f ⁻¹' {j})) (g j)

Tactic:
refine Finset.sum_congr rfl fun x hx => ?_

Result:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ⊤
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑(filter (fun b => g b = g (f a)) f.range))) (g (f a)) =
    (T (⋃ y ∈ filter (fun b => g b = g (f a)) f.range, ⇑f ⁻¹' {y})) (g (f a))
x : G
hx : x ∈ filter (fun b => g b = g (f a)) f.range
⊢ (T (⇑f ⁻¹' {x})) (g (f a)) = (T (⇑f ⁻¹' {x})) (g x)