harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem derivWithin_comp (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x))
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s') :
    derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
exact (hh₂.hasDerivWithinAt.comp x hh.hasDerivWithinAt hs).derivWithin hxs

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem _root_.Set.InjOn.injective_iff (s : Set β) (h : InjOn g s) (hs : range f ⊆ s) :
    Injective (g ∘ f) ↔ Injective f :=
  ⟨(·.of_comp), fun h _ ↦ by aesop⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
h✝ : InjOn g s
hs : range f ⊆ s
h : Injective f
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (g ∘ f) x✝ = (g ∘ f) a₂ → x✝ = a₂

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem restr_toPartialEquiv' (s : Set X) (hs : IsOpen s) :
    (e.restr s).toPartialEquiv = e.toPartialEquiv.restr s

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
⊢ (e.restr s).toPartialEquiv = e.restr s

Tactic:
rw [e.restr_toPartialEquiv, hs.interior_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a b : α}
    (hab : a == b) : get! m a = get! m b

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a b : α
hab : (a == b) = true
⊢ get! m a = get! m b

Tactic:
simp_to_raw using Raw₀.Const.get!_congr

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem groupoid_of_pregroupoid_le (PG₁ PG₂ : Pregroupoid H)
    (h : ∀ f s, PG₁.property f s → PG₂.property f s) : PG₁.groupoid ≤ PG₂.groupoid

Proof state:
H : Type u
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : PartialHomeomorph H H
he : PG₁.property (↑e) e.source ∧ PG₁.property (↑e.symm) e.target
⊢ PG₂.property (↑e) e.source ∧ PG₂.property (↑e.symm) e.target

Tactic:
exact ⟨h _ _ he.1, h _ _ he.2⟩

Result:
no goals

Proof state:
H : Type u
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
⊢ PG₁.groupoid ≤ PG₂.groupoid

Tactic:
refine StructureGroupoid.le_iff.2 fun e he ↦ ?_

Result:
H : Type u
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : PartialHomeomorph H H
he : e ∈ PG₁.groupoid
⊢ e ∈ PG₂.groupoid

Proof state:
H : Type u
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : PartialHomeomorph H H
he : e ∈ PG₁.groupoid
⊢ e ∈ PG₂.groupoid

Tactic:
rw [mem_groupoid_of_pregroupoid] at he ⊢

Result:
H : Type u
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : PartialHomeomorph H H
he : PG₁.property (↑e) e.source ∧ PG₁.property (↑e.symm) e.target
⊢ PG₂.property (↑e) e.source ∧ PG₂.property (↑e.symm) e.target
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem arsinh_nonneg_iff : 0 ≤ arsinh x ↔ 0 ≤ x

Proof state:
x : ℝ
⊢ 0 ≤ arsinh x ↔ 0 ≤ x

Tactic:
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/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✝¹ : 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/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1

Proof state:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a

Tactic:
constructor <;> assumption

Result:
no goals

Proof state:
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ a / b = (a - b) / b + 1

Tactic:
rw [div_eq a, if_pos]

Result:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_blimsup {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ n, p n → MeasurableSet (s n)) :
    MeasurableSet <| blimsup s atTop p

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋂ i, ⋃ j, ⋃ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)

Tactic:
simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋂ i, ⋃ j, ⋃ (_ : p j ∧ i ≤ j), s j)
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
lemma isAffineOpen_basicOpen : IsAffineOpen (basicOpen 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsAffineOpen (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))

Tactic:
exact isAffineOpen_opensRange (awayι _ _ _ _)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsAffineOpen (basicOpen 𝒜 f)

Tactic:
rw [← opensRange_awayι 𝒜 f f_deg hm]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsAffineOpen (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem subset_hom (C : G.ComponentCompl L) (h : K ⊆ L) : (C : Set V) ⊆ (C.hom h : Set V)

Proof state:
case intro
V : Type u
G : SimpleGraph V
K L : Set V
h : K ⊆ L
c : V
cL : c ∉ L
⊢ c ∈ ↑(hom h (G.componentComplMk cL))

Tactic:
exact ⟨fun h' => cL (h h'), rfl⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ↑C ⊆ ↑(hom h C)

Tactic:
rintro c ⟨cL, rfl⟩

Result:
case intro
V : Type u
G : SimpleGraph V
K L : Set V
h : K ⊆ L
c : V
cL : c ∉ L
⊢ c ∈ ↑(hom h (G.componentComplMk cL))
-- Mathlib/Topology/Algebra/Module/WeakBilin.lean
theorem tendsto_iff_forall_eval_tendsto {l : Filter α} {f : α → WeakBilin B} {x : WeakBilin B}
    (hB : Function.Injective B) :
    Tendsto f l (𝓝 x) ↔ ∀ y, Tendsto (fun i => B (f i) y) l (𝓝 (B x y))

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ⇑B
⊢ Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i => (B (f i)) y) l (𝓝 ((B x) y))

Tactic:
rw [← tendsto_pi_nhds, (isEmbedding hB).tendsto_nhds_iff]

Result:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ⇑B
⊢ Tendsto ((fun x y => (B x) y) ∘ f) l (𝓝 fun y => (B x) y) ↔ Tendsto (fun i => ⇑(B (f i))) l (𝓝 ⇑(B x))

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ⇑B
⊢ Tendsto ((fun x y => (B x) y) ∘ f) l (𝓝 fun y => (B x) y) ↔ Tendsto (fun i => ⇑(B (f i))) l (𝓝 ⇑(B x))

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/IsLUB.lean
theorem isLUB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) :
    IsLUB s a

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure s
⊢ IsLUB s a

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
exact isLUB_of_mem_nhds hsa (mem_principal_self s)

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem a_zero : a 0 = (1 : QuaternionGroup n)

Proof state:
n : ℕ
⊢ a 0 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem Prime.coprime_iff_not_dvd {p n : ℕ} (pp : Prime p) : Coprime p n ↔ ¬p ∣ n :=
  ⟨fun co d => pp.not_dvd_one <| co.dvd_of_dvd_mul_left (by simp [d]), fun nd =>
    coprime_of_dvd fun _ m2 mp => ((prime_dvd_prime_iff_eq m2 pp).1 mp).symm ▸ nd⟩

Proof state:
p n : ℕ
pp : Prime p
co : p.Coprime n
d : p ∣ n
⊢ p ∣ n * 1

Tactic:
simp [d]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
@[simp] lemma pow_eq_zero_iff' [Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
n : ℕ
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ}
    (v₁ : ι₁ → F) (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ}
    (v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
    ⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
      (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
  real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
  ← div_add_div_same, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
  Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
  mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
  Finset.sum_div, mul_div_assoc, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsLowerSet.cthickening' (hs : IsLowerSet s) (ε : ℝ) :
    IsLowerSet (cthickening ε s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (cthickening ε s)

Tactic:
rw [cthickening_eq_iInter_thickening'']

Result:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (⋂ ε_1, ⋂ (_ : 0 ⊔ ε < ε_1), thickening ε_1 s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (⋂ ε_1, ⋂ (_ : 0 ⊔ ε < ε_1), thickening ε_1 s)

Tactic:
exact isLowerSet_iInter₂ fun δ _ => hs.thickening' _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ico_iff_integrableOn_Ioo :
    IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ :=
  integrableOn_Ico_iff_integrableOn_Ioo' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ μ {a} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma π_comp_colimitOpIsoOpLimit_inv (F : J ⥤ C) [HasLimit F] (j : J) :
    (limit.π F j).op ≫ (colimitOpIsoOpLimit F).inv = colimit.ι F.op (op j)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ (limit.π F j).op ≫ (colimitOpIsoOpLimit F).inv = colimit.ι F.op (op j)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_relabel : relabel r1 (relabel r2 f) = relabel (r1 ∘ r2) f

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
f : CNF α✝
⊢ relabel r1 (relabel r2 f) = relabel (r1 ∘ r2) f

Tactic:
simp only [relabel, List.map_map, Clause.relabel_relabel']

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem insert'.valid [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)]
    (x : α) {t} (h : Valid t) : Valid (insert' x t)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (insert' x t).Valid

Tactic:
rw [insert'_eq_insertWith]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ => id) h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_lt_one_iff_real_of_norm_one {x y : F} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    ⟪x, y⟫_ℝ < 1 ↔ x ≠ y

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_ℝ < 1 ↔ x ≠ y

Tactic:
convert inner_lt_norm_mul_iff_real (F := F) <;> simp [hx, hy]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Nat.pred_mul_geom_sum_le (a b n : ℕ) :
    ((b - 1) * ∑ i ∈ range n.succ, a / b ^ i) ≤ a * b - a / b ^ n :=
  calc
    ((b - 1) * ∑ i ∈ range n.succ, a / b ^ i) =
    (∑ i ∈ range n, a / b ^ (i + 1) * b) + a * b - ((∑ i ∈ range n, a / b ^ i) + a / b ^ n)

Proof state:
a b n : ℕ
⊢ ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n) ≤
    ∑ i ∈ range n, a / b ^ i + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
gcongr with i hi

Result:
case h.bc.h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i

Proof state:
case h.bc.h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i

Tactic:
exact Nat.div_mul_le_self _ _

Result:
no goals

Proof state:
a b n : ℕ
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
  Nat.div_one]

Result:
no goals

Proof state:
case h.bc.h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i

Tactic:
rw [pow_succ, ← Nat.div_div_eq_div_mul]

Result:
case h.bc.h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem kernel.ι_unop :
    (kernel.ι g.unop).op = eqToHom (Opposite.op_unop _) ≫ cokernel.π g ≫ (kernelUnopOp g).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι g.unop).op = eqToHom ⋯ ≫ cokernel.π g ≫ (kernelUnopOp g).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mdifferentiableAt_iff_differentiableAt :
    MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x

Tactic:
exact ⟨fun H => H.2, fun H => ⟨H.continuousAt, H⟩⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [mdifferentiableAt_iff, differentiableWithinAt_univ, mfld_simps]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} : k' ∈ m.modify k f ↔ k' ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
⊢ k' ∈ m.modify k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_modify]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem eq_affineCombination_subset_iff_eq_affineCombination_subtype {p0 : P} {s : Set ι}
    {p : ι → P} :
    (∃ fs : Finset ι, ↑fs ⊆ s ∧ ∃ w : ι → k, ∑ i ∈ fs, w i = 1 ∧
        p0 = fs.affineCombination k p w) ↔
      ∃ (fs : Finset s) (w : s → k), ∑ i ∈ fs, w i = 1 ∧
        p0 = fs.affineCombination k (fun i : s => p i) w

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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs,
      ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w) ↔
    ∃ fs w,
      ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint (fun i => p ↑i) (Classical.choice ⋯)) w

Tactic:
exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

Result:
no goals

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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i => p ↑i) w

Tactic:
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]

Result:
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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs,
      ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w) ↔
    ∃ fs w,
      ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint (fun i => p ↑i) (Classical.choice ⋯)) w
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_eraseMax (t : Ordnode α) : dual (eraseMax t) = eraseMin (dual t)

Proof state:
α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.eraseMin

Tactic:
rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]

Result:
no goals