harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem denseRange_natCast : DenseRange (Nat.cast : ℕ → ℤ_[p])

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ < ε

Tactic:
apply lt_of_le_of_lt _ hn

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ ≤ ↑p ^ (-↑n)

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist x ↑(x.appr n) < ε

Tactic:
rw [dist_eq_norm]

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ < ε

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε

Tactic:
intro ε hε

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
⊢ ∃ k, dist x ↑k < ε

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Tactic:
apply appr_spec

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ ≤ ↑p ^ (-↑n)

Tactic:
rw [norm_le_pow_iff_mem_span_pow]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Nat.cast

Tactic:
intro x

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Nat.cast)

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
⊢ ∃ k, dist x ↑k < ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε

Result:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ k, dist x ↑k < ε

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Nat.cast)

Tactic:
rw [Metric.mem_closure_range_iff]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε

Proof state:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ k, dist x ↑k < ε

Tactic:
use x.appr n

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist x ↑(x.appr n) < ε
-- Mathlib/Data/Finset/Pi.lean
theorem pi_singletons {β : Type*} (s : Finset α) (f : α → β) :
    (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ s.pi fun a => {f a}) ∧ ∀ x ∈ s.pi fun a => {f a}, x = fun a x => f a

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ s.pi fun a => {f a}

case right
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ∀ x ∈ s.pi fun a => {f a}, x = fun a x => f a

Proof state:
case left
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ s.pi fun a => {f a}

Tactic:
simp

Result:
no goals

Proof state:
case right
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ s.pi fun a => {f a}
⊢ a = fun a x => f a

Tactic:
ext i hi

Result:
case right.h.h
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ s.pi fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (s.pi fun a => {f a}) = {fun a x => f a}

Tactic:
rw [eq_singleton_iff_unique_mem]

Result:
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ s.pi fun a => {f a}) ∧ ∀ x ∈ s.pi fun a => {f a}, x = fun a x => f a

Proof state:
case right.h.h
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i

Tactic:
simpa using ha i hi

Result:
no goals

Proof state:
case right
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ ∀ x ∈ s.pi fun a => {f a}, x = fun a x => f a

Tactic:
intro a ha

Result:
case right
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ s.pi fun a => {f a}
⊢ a = fun a x => f a

Proof state:
case right.h.h
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ s.pi fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i

Tactic:
rw [mem_pi] at ha

Result:
case right.h.h
α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i
-- Mathlib/Algebra/Lie/Nilpotent.lean
@[simp]
lemma LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (k : ℕ) :
    lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k =
    (lowerCentralSeries R L M k).baseChange A

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = baseChange A (lowerCentralSeries R L M k)

Tactic:
induction k with
| zero => simp
| succ k ih => simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

Result:
no goals

Proof state:
case zero
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0 = baseChange A (lowerCentralSeries R L M 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
ih : lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = baseChange A (lowerCentralSeries R L M k)
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1) = baseChange A (lowerCentralSeries R L M (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem zero_oreDiv' (s : S) : (0 : R) /ₒ s = 0

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
s : ↥S
⊢ 0 /ₒ s = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_eq_iff]

Result:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
s : ↥S
⊢ ∃ u v, u • 0 = v • 0 ∧ ↑u * ↑1 = v * ↑s

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
s : ↥S
⊢ ∃ u v, u • 0 = v • 0 ∧ ↑u * ↑1 = v * ↑s

Tactic:
exact ⟨s, 1, by simp [Submonoid.smul_def]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
s : ↥S
⊢ s • 0 = 1 • 0 ∧ ↑s * ↑1 = 1 * ↑s

Tactic:
simp [Submonoid.smul_def]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem bijection_symm_apply_id (A B : C) :
    (bijection i A B _).symm (𝟙 _) = prodComparison _ _ _

Proof state:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (fst A B))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ (reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)

Tactic:
apply hom_ext

Result:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

case h_snd
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem equalizer_sheaf_condition :
    Presieve.IsSheafFor P (S : Presieve X) ↔ Nonempty (IsLimit (Fork.ofι _ (w P S)))

Proof state:
case h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf

Tactic:
simp [firstObjEqFamily, forkMap]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique,
  ← Equiv.forall_congr_right (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]

Result:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      firstMap P S ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          secondMap P S ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, forkMap P S.arrows x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Proof state:
case h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = x f hf

Tactic:
rw [← q]

Result:
case h.h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf
-- Mathlib/Algebra/BigOperators/Pi.lean
lemma prod_indicator (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) :
    ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

Proof state:
case h
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a

Tactic:
simpa using prod_indicator_apply ..

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
⊢ ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

Tactic:
ext a

Result:
case h
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_eq_self : |a| = a ↔ 0 ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a| = a ↔ 0 ≤ a

Tactic:
rw [abs_eq_max_neg, max_eq_left_iff, neg_le_self_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_closure (M : Matroid α) [InvariantCardinalRank M] (X : Set α) :
    M.cRk (M.closure X) = M.cRk X

Proof state:
case intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]

Result:
no goals

Proof state:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X : Set α
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Result:
case intro
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ M.cRk (M.closure X) = M.cRk X
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_smul {n : ℕ} (ha : a ∈ I) :
    hI.dpow n (b • a) = b ^ n • hI.dpow n a

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (b • a) = b ^ n • hI.dpow n a

Tactic:
simp only [smul_eq_mul, hI.dpow_mul, ha]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_succ_of_none {f : Fin (n+1) → Option α} (h : f 0 = none) :
    findSome? f = findSome? fun i => f i.succ

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
h : f 0 = none
⊢ findSome? f = findSome? fun i => f i.succ

Tactic:
simp [findSome?_succ, h]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma mapToEqualizer_eq_comp (P : Cᵒᵖ ⥤ Type*) {X B : C} (π : X ⟶ B) [HasPullback π π] :
    MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition =
    equalizer.lift (P.map π.op) (equalizerCondition_w' P π) ≫
    (Types.equalizerIso _ _).hom

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
        (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv) ≫
      equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op) =
    equalizer.lift (P.map π.op) ⋯ ≫ equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv =
    equalizer.lift (P.map π.op) ⋯

Tactic:
apply equalizer.hom_ext

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
        (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv) ≫
      equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op) =
    equalizer.lift (P.map π.op) ⋯ ≫ equalizer.ι (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ =
    equalizer.lift (P.map π.op) ⋯ ≫ (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom

Tactic:
rw [← Iso.comp_inv_eq (α := Types.equalizerIso _ _)]

Result:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv =
    equalizer.lift (P.map π.op) ⋯
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|` -/
lemma binEntropy_nonpos_of_one_le (hp : 1 ≤ p) : binEntropy p ≤ 0

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy p ≤ 0

Tactic:
rw [← binEntropy_one_sub]

Result:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Tactic:
exact binEntropy_nonpos_of_nonpos (sub_nonpos.2 hp)

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_rangeRestrict : range f.rangeRestrict = ⊤

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range f.rangeRestrict = ⊤

Tactic:
simp [f.range_codRestrict _]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
lemma linearIndependent_lapMatrix_ker_basis_aux :
    LinearIndependent ℝ (lapMatrix_ker_basis_aux G)

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ LinearIndependent ℝ G.lapMatrix_ker_basis_aux

Tactic:
rw [Fintype.linearIndependent_iff]

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ ∀ (g : G.ConnectedComponent → ℝ),
    ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0 → ∀ (i : G.ConnectedComponent), g i = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
intro c

Result:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
c : G.ConnectedComponent
⊢ g c = 0

Proof state:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
c : G.ConnectedComponent
⊢ g c = 0

Tactic:
obtain ⟨i, h'⟩ : ∃ i : V, G.connectedComponentMk i = c := Quot.exists_rep c

Result:
case intro
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : (fun i => g (G.connectedComponentMk i)) = ↑0
h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)
c : G.ConnectedComponent
i : V
h' : G.connectedComponentMk i = c
⊢ g c = 0
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_eq_of_nat [Norm α] [Norm β] (n : ℕ) (h : p = n) (f : WithLp p (α × β)) :
    ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / (n : ℝ))

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : Norm α
inst✝ : Norm β
n : ℕ
h : p = ↑n
f : WithLp p (α × β)
this : 0 < p.toReal
⊢ ‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast, eq_self_iff_true,
  Finset.sum_congr, prod_norm_eq_add this]

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : Norm α
inst✝ : Norm β
n : ℕ
h : p = ↑n
f : WithLp p (α × β)
⊢ ‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)

Tactic:
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)

Result:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : Norm α
inst✝ : Norm β
n : ℕ
h : p = ↑n
f : WithLp p (α × β)
this : 0 < p.toReal
⊢ ‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_cthickening_subset (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set α) :
    cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun hx => infEdist_le_infEdist_cthickening_add.trans (add_le_add_right hx _)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
⊢ cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
intro x

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ