harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/TietzeExtension.lean
theorem exists_extension_norm_eq_of_isClosedEmbedding (f : X →ᵇ ℝ) {e : X → Y}
    (he : IsClosedEmbedding e) : ∃ g : Y →ᵇ ℝ, ‖g‖ = ‖f‖ ∧ g ∘ e = f

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖
⊢ ∃ g_1,
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖ ∧
      ⇑g_1 ∘ e = ⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ })

Tactic:
exact ⟨g, hg, rfl⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_extension_norm_eq_of_isClosedEmbedding' f ⟨e, he.continuous⟩ he with ⟨g, hg, rfl⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖
⊢ ∃ g_1,
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖ ∧
      ⇑g_1 ∘ e = ⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ })
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 3 (by norm_num) (by norm_num)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s].get? 3 =
    some (∃ l ∈ Ico l' a, Ioc l a ⊆ s)

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s].get? 0 =
    some (s ∈ 𝓝[≤] a)

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_norm [Fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1

Proof state:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ‖fourier n‖ = 1

Tactic:
rw [ContinuousMap.norm_eq_iSup_norm]

Result:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ⨆ x, ‖(fourier n) x‖ = 1

Proof state:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1
⊢ ⨆ x, ‖(fourier n) x‖ = 1

Tactic:
simp_rw [this]

Result:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1
⊢ ⨆ x, 1 = 1

Proof state:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ⨆ x, ‖(fourier n) x‖ = 1

Tactic:
have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.norm_coe _

Result:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1
⊢ ⨆ x, ‖(fourier n) x‖ = 1

Proof state:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1
⊢ ⨆ x, 1 = 1

Tactic:
exact @ciSup_const _ _ _ Zero.instNonempty _

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a

Proof state:
α : Type u_1
l : List α
a : α
⊢ l.headD a = l.head?.getD a

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem LEComap.comp : LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
A : DiscreteQuotient X
B : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

Tactic:
tauto

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_singleton (i : ι) (f : ι → α) : ({i} : Finset ι).SupIndep f :=
  fun s hs j hji hj => by
    rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
    exact disjoint_bot_right

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) (s.sup f)

Tactic:
rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]

Result:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) ⊥

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) ⊥

Tactic:
exact disjoint_bot_right

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Ici_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
    f.measure (Ici x) = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
⊢ f.measure (Ioi x) ≤ f.measure (Ici x)

Tactic:
exact measure_mono Ioi_subset_Ici_self

Result:
no goals

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
⊢ f.measure (Ici x) = ⊤

Tactic:
rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x]

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
⊢ f.measure (Ioi x) ≤ f.measure (Ici x)
-- Mathlib/Topology/CompactOpen.lean
theorem tendsto_compactOpen_iff_forall {ι : Type*} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :
    Tendsto F l (𝓝 f) ↔
      ∀ K, IsCompact K → Tendsto (fun i => (F i).restrict K) l (𝓝 (f.restrict K))

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
⊢ Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun i => restrict K (F i)) l (𝓝 (restrict K f))

Tactic:
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem hasProd_pi_single [DecidableEq β] (b : β) (a : α) : HasProd (Pi.mulSingle b a) a

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
x✝ : β
⊢ Pi.mulSingle b a x✝ = if x✝ = b then a else 1

Tactic:
simp [Pi.mulSingle_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ HasProd (Pi.mulSingle b a) a

Tactic:
convert hasProd_ite_eq b a

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
x✝ : β
⊢ Pi.mulSingle b a x✝ = if x✝ = b then a else 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
    (a.eraseIdx! i).toList = a.toList.eraseIdx i

Proof state:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i).toList =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.eraseIdx i

Tactic:
simp_all [Array.eraseIdx!]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
hi : i < n
⊢ (a.eraseIdx! i).toList = a.toList.eraseIdx i

Tactic:
cases a

Result:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i).toList =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.eraseIdx i
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion₂_prod_const {s : ∀ i, κ i → Set α} {t : Set β} :
    (⋃ (i) (j), s i j) ×ˢ t = ⋃ (i) (j), s i j ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t

Tactic:
simp_rw [iUnion_prod_const]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
lemma ofProd_comp_toProd : (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id _ _

Proof state:
case hb.a.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₂
⊢ (ofProd Q₁ Q₂) ((toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (ι Q₂) x✝)) = 1 ᵍ⊗ₜ[R] (ι Q₂) x✝

Tactic:
simp

Result:
no goals

Proof state:
case hb.a.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₂
⊢ ((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝ =
    (((AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝

Tactic:
dsimp

Result:
case hb.a.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₂
⊢ (ofProd Q₁ Q₂) ((toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (ι Q₂) x✝)) = 1 ᵍ⊗ₜ[R] (ι Q₂) x✝

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

Tactic:
ext <;> (dsimp; simp)

Result:
no goals
-- Mathlib/RingTheory/Prime.lean
theorem mul_eq_mul_prime_pow {x y a p : R} {n : ℕ} (hp : Prime p) (hx : x * y = a * p ^ n) :
    ∃ (i j : ℕ) (b c : R), i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ b * c = b * c ∧ b * ∏ i ∈ t, p = b * p ^ #t ∧ c * ∏ i ∈ u, p = c * p ^ #u

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ #t + #u = n

Tactic:
rw [← card_union_of_disjoint htu, htus, card_range]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ ∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j

Tactic:
exact ⟨#t, #u, b, c, by rw [← card_union_of_disjoint htu, htus, card_range], by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j

Tactic:
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
  (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
    ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ ∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ x * y = a * ∏ x ∈ range n, p

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem LinearMap.toMatrix_id_eq_basis_toMatrix [Fintype ι] [DecidableEq ι] [Finite ι'] :
    LinearMap.toMatrix b b' id = b'.toMatrix b

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite ι'
⊢ (toMatrix b b') id = b'.toMatrix ⇑b

Tactic:
ext i

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite ι'
i : ι'
j✝ : ι
⊢ (toMatrix b b') id i j✝ = b'.toMatrix (⇑b) i j✝

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite ι'
i : ι'
j✝ : ι
⊢ (toMatrix b b') id i j✝ = b'.toMatrix (⇑b) i j✝

Tactic:
apply LinearMap.toMatrix_apply

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepSet_iff_Indep (s t : Set Ω) (μ : Measure Ω) :
    IndepSet s t μ ↔ Indep (generateFrom {s}) (generateFrom {t}) μ

Proof state:
Ω : Type u_1
x✝ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t μ ↔ Indep (generateFrom {s}) (generateFrom {t}) μ

Tactic:
simp only [IndepSet, Indep, Kernel.IndepSet]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem eq_one_of_x_eq_one (h₀ : d ≠ 0) {a : Solution₁ d} (ha : a.x = 1) : a = 1

Proof state:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : a.y = 0
⊢ a = 1

Tactic:
exact ext ha prop

Result:
no goals

Proof state:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
⊢ a = 1

Tactic:
have prop := a.prop_y

Result:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * a.y ^ 2 = a.x ^ 2 - 1
⊢ a = 1

Proof state:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * a.y ^ 2 = a.x ^ 2 - 1
⊢ a = 1

Tactic:
rw [ha, one_pow, sub_self, mul_eq_zero, or_iff_right h₀, sq_eq_zero_iff] at prop

Result:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : a.y = 0
⊢ a = 1
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem map_id {f : CostructuredArrow S T} : (map (𝟙 T)).obj f = f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj f = f

Tactic:
rw [eq_mk f]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj (mk f.hom) = mk f.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj (mk f.hom) = mk f.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_of_sub_nonneg {a b : Int} (h : 0 ≤ a - b) : b ≤ a

Proof state:
a b : Int
h✝ : 0 ≤ a - b
h : 0 + b ≤ a - b + b
⊢ b ≤ a

Tactic:
rwa [Int.sub_add_cancel, Int.zero_add] at h

Result:
no goals

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

Tactic:
have h := Int.add_le_add_right h b

Result:
a b : Int
h✝ : 0 ≤ a - b
h : 0 + b ≤ a - b + b
⊢ b ≤ a
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.eq_fac [HasEqualizers C] (h : f = f') :
    image.ι f = (image.eqToIso h).hom ≫ image.ι f'

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'

Tactic:
dsimp [asIso,image.eqToIso, image.eqToHom]

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f =
    factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f') ⋯) ≫ ι f'

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'

Tactic:
apply image.ext

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f =
    factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f') ⋯) ≫ ι f'

Tactic:
rw [image.lift_fac]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
lemma embDomain_comapDomain {f : α ↪ β} {g : β →₀ M} (hg : ↑g.support ⊆ Set.range f) :
    embDomain f (comapDomain f g f.injective.injOn) = g

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
by_cases hb : b ∈ Set.range f

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∈ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∉ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
⊢ embDomain f (comapDomain (⇑f) g ⋯) = g

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
a : α
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) (f a) = g (f a)

Tactic:
rw [embDomain_apply, comapDomain_apply]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∈ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
obtain ⟨a, rfl⟩ := hb

Result:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
a : α
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) (f a) = g (f a)

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range ⇑f
hg : g b = 0
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
rw [embDomain_notin_range _ _ _ hb, hg]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_mul_comm [AddCommMonoid R] [CommSemigroup R] (A : Matrix m n R) (B : Matrix n m R) :
    trace (A * B) = trace (B * A)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : CommSemigroup R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B).trace = (B * A).trace

Tactic:
rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Partition.lean
@[simp] lemma ofSym_one (s : Sym σ 1) : ofSym s = indiscrete 1

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
⊢ ofSym s = indiscrete 1

Tactic:
ext

Result:
case parts.a
σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
a✝ : ℕ
⊢ count a✝ (ofSym s).parts = count a✝ (indiscrete 1).parts

Proof state:
case parts.a
σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
a✝ : ℕ
⊢ count a✝ (ofSym s).parts = count a✝ (indiscrete 1).parts

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma δ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) :
    δ F X X' ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ δ F Y X'

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ δ F X X' ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ δ F Y X'

Tactic:
apply δ'_natural_left

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma AbsolutelyContinuous.withDensity_rnDeriv {ξ : Measure α} [μ.HaveLebesgueDecomposition ν]
    (hξμ : ξ ≪ μ) (hξν : ξ ≪ ν) :
    ξ ≪ ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Tactic:
conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ⟂ₘ μ.singularPart ν

Tactic:
exact MutuallySingular.mono_ac (mutuallySingular_singularPart μ ν).symm hξν .rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Tactic:
refine absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ⟂ₘ μ.singularPart ν
-- Mathlib/Data/Prod/Basic.lean
theorem snd_eq_iff : ∀ {p : α × β} {x : β}, p.2 = x ↔ p = (p.1, x)
  | ⟨a, b⟩, x => by simp

Proof state:
α : Type u_1
β : Type u_2
a : α
b x : β
⊢ (a, b).snd = x ↔ (a, b) = ((a, b).fst, x)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem self_mem_ordConnectedComponent : x ∈ ordConnectedComponent s x ↔ x ∈ s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ x ∈ s.ordConnectedComponent x ↔ x ∈ s

Tactic:
rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem absorbent_iff_eventually_nhdsWithin_zero :
    Absorbent 𝕜 s ↔ ∀ x : E, ∀ᶠ c : 𝕜 in 𝓝[≠] 0, c • x ∈ s :=
  forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_nhdsWithin_zero, mapsTo_singleton]

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ Absorbs 𝕜 s {x} ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, c • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_nhdsWithin_zero, mapsTo_singleton]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma norm_term_le {f g : ℕ → ℂ} (s : ℂ) {n : ℕ} (h : ‖f n‖ ≤ ‖g n‖) :
    ‖term f s n‖ ≤ ‖term g s n‖

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ ‖term f s n‖ ≤ ‖term g s n‖

Tactic:
simp only [norm_term_eq]

Result:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ (if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re) ≤ if n = 0 then 0 else ‖g n‖ / ↑n ^ s.re

Proof state:
case isTrue
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : n = 0
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s.re ≤ ‖g n‖ / ↑n ^ s.re

Tactic:
gcongr

Result:
no goals

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ (if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re) ≤ if n = 0 then 0 else ‖g n‖ / ↑n ^ s.re

Tactic:
split

Result:
case isTrue
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : n = 0
⊢ 0 ≤ 0

case isFalse
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s.re ≤ ‖g n‖ / ↑n ^ s.re