harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
@[simp]
lemma fromFreeYonedaCoproduct_app_mk (m : M.Elements) :
    M.fromFreeYonedaCoproduct.app _ (M.freeYonedaCoproductMk m) = m.2

Proof state:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst)) (M.freeYonedaCoproductMk m) = m.snd

Tactic:
dsimp [freeYonedaCoproductMk]

Result:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst))
      ((ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst)))) =
    m.snd

Proof state:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst))
      ((ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst)))) =
    m.snd

Tactic:
erw [M.ι_fromFreeYonedaCoproduct_apply m]

Result:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd

Proof state:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd

Tactic:
rw [m.fromFreeYoneda_app_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem mul_mul_mul_inv_mem_range_inl : σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
  mul_inv_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem uncurry_pre (f : B ⟶ A) [Exponentiable B] (X : C) :
    CartesianClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (exp.ev A).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
A B : C
inst✝² : ChosenFiniteProducts C
inst✝¹ : Exponentiable A
f : B ⟶ A
inst✝ : Exponentiable B
X : C
⊢ uncurry ((pre f).app X) = f ▷ (A ⟹ X) ≫ (exp.ev A).app X

Tactic:
rw [uncurry_eq, prod_map_pre_app_comp_ev]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
lemma CStarAlgebra.le_nnnorm_of_mem_quasispectrum {A : Type*} [NonUnitalCStarAlgebra A]
    {a : A} {x : ℝ≥0} (hx : x ∈ quasispectrum ℝ≥0 a) : x ≤ ‖a‖₊

Proof state:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ quasispectrum ℝ≥0 a
⊢ x ≤ ‖a‖₊

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx

Result:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊

Proof state:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊

Tactic:
simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y

Proof state:
w : Nat
x y : BitVec w
⊢ x = y → x.toFin = y.toFin

Tactic:
intro h

Result:
w : Nat
x y : BitVec w
h : x = y
⊢ x.toFin = y.toFin

Proof state:
w : Nat
x y : BitVec w
h : x = y
⊢ x.toFin = y.toFin

Tactic:
simp [toFin, h]

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x = y → x.toFin = y.toFin

Tactic:
case mpr =>
  intro h
  simp [toFin, h]

Result:
no goals

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ x.toFin = y.toFin → x = y

case mpr
w : Nat
x y : BitVec w
⊢ x = y → x.toFin = y.toFin

Tactic:
case mp =>
  exact @eq_of_toFin_eq w x y

Result:
case mpr
w : Nat
x y : BitVec w
⊢ x = y → x.toFin = y.toFin

Proof state:
w : Nat
x y : BitVec w
⊢ x.toFin = y.toFin → x = y

Tactic:
exact @eq_of_toFin_eq w x y

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.toFin = y.toFin ↔ x = y

Tactic:
apply Iff.intro

Result:
case mp
w : Nat
x y : BitVec w
⊢ x.toFin = y.toFin → x = y

case mpr
w : Nat
x y : BitVec w
⊢ x = y → x.toFin = y.toFin
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_neg_iff_of_neg_left (ha : a < 0) : a • b < 0 ↔ 0 < b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₂ := (0 : β))

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem findMax'_dual (t) (x : α) : findMax' x (dual t) = findMin' t x

Proof state:
α : Type u_1
t : Ordnode α
x : α
⊢ findMax' x t.dual = t.findMin' x

Tactic:
rw [← findMin'_dual, dual_dual]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Complex.isometryOfOrthonormal_apply (v : OrthonormalBasis (Fin 2) ℝ F) (z : ℂ) :
    Complex.isometryOfOrthonormal v z = z.re • v 0 + z.im • v 1

Proof state:
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ (isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1

Tactic:
simp [Complex.isometryOfOrthonormal, ← v.sum_repr_symm]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem lift_fac (H' : Set.range g.base ⊆ Set.range f.base) : lift f g H' ≫ f = g

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ lift f g H' ≫ f = g

Tactic:
erw [Category.assoc]

Result:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g

Tactic:
exact pullback.condition

Result:
no goals

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g

Tactic:
rw [IsIso.inv_comp_eq]

Result:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem rank_self : Module.rank R R = 1

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Module.rank R R = 1

Tactic:
rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]

Result:
no goals
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem exists_compact_superset [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) :
    ∃ K', IsCompact K' ∧ K ⊆ interior K'

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ⋃ x ∈ I, interior (s x) ⊆ interior (⋃ x ∈ I, s x)

Tactic:
exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ⋃ x ∈ I, interior (s x) ⊆ interior (⋃ x ∈ I, s x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : X → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'
-- Mathlib/Analysis/AbsoluteValue/Equivalence.lean
/-- Equivalence of absolute values is symmetric. -/
lemma isEquiv_symm {f g : AbsoluteValue R ℝ} (hfg : IsEquiv f g) : IsEquiv g f

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : AbsoluteValue R ℝ
hfg : f.IsEquiv g
⊢ g.IsEquiv f

Tactic:
rcases hfg with ⟨c, hcpos, h⟩

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g : AbsoluteValue R ℝ
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ g.IsEquiv f

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g : AbsoluteValue R ℝ
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ (fun x => g x ^ (1 / c)) = ⇑f

Tactic:
simp [← h, Real.rpow_rpow_inv (apply_nonneg f _) (ne_of_lt hcpos).symm]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g : AbsoluteValue R ℝ
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ g.IsEquiv f

Tactic:
refine ⟨1 / c, one_div_pos.mpr hcpos, ?_⟩

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g : AbsoluteValue R ℝ
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ (fun x => g x ^ (1 / c)) = ⇑f
-- Mathlib/Computability/TuringMachine.lean
theorem stmts_trans {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h₁ : q₁ ∈ stmts₁ q₂) :
    some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)

Tactic:
exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
  forall_eq', exists_imp, and_imp]

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P y * Q z ^ 3 = Q y * P z ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u y * Q z ^ 3 = Q y * (fun m => m • Q) u z ^ 3

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 3 * Q y * Q z ^ 3 = Q y * (↑u * Q z) ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u y * Q z ^ 3 = Q y * (fun m => m • Q) u z ^ 3

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 3 * Q y * Q z ^ 3 = Q y * (↑u * Q z) ^ 3
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem disjoint_negAt_plusPart : Pairwise (Disjoint on (fun s ↦ negAt s '' (plusPart A)))

Proof state:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
⊢ (Disjoint on fun s => ⇑(negAt s) '' plusPart A) s t

Tactic:
refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_

Result:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
⊢ False

Proof state:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
⊢ False

Tactic:
obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := Set.symmDiff_nonempty.mpr hst

Result:
case intro.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False

case intro.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Proof state:
case intro.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False

Tactic:
exact lt_irrefl _ <|
  (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_not_mem_negAt_plusPart A hx' hw.2)

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s => ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
exact lt_irrefl _ <|
  (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_not_mem_negAt_plusPart A hx hw.2)

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
⊢ Pairwise (Disjoint on fun s => ⇑(negAt s) '' plusPart A)

Tactic:
intro s t hst

Result:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
⊢ (Disjoint on fun s => ⇑(negAt s) '' plusPart A) s t
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma differentiableAt_binEntropy_iff_ne_zero_one :
    DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Proof state:
case funProp.discharger
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ (1 - 0)⁻¹ ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False

Tactic:
rw [DifferentiableAt.add_iff_left] at h

Result:
case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹) 0
⊢ False

case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p => (1 - p) * log (1 - p)⁻¹) 0

Proof state:
case refine_2
h : DifferentiableAt ℝ (fun x => (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (1 - 1)
⊢ False

Tactic:
simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h

Result:
no goals

Proof state:
case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p => (1 - p) * log (1 - p)⁻¹) 0

Tactic:
fun_prop (disch := simp)

Result:
no goals

Proof state:
case funProp.discharger
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ 1⁻¹ ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ DifferentiableAt ℝ (fun p => p * log p⁻¹) 1

Tactic:
fun_prop (disch := simp)

Result:
no goals

Proof state:
case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹) 0
⊢ False

Tactic:
simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h

Result:
no goals

Proof state:
case refine_2
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ False

Tactic:
rw [DifferentiableAt.add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] at h

Result:
case refine_2
h : DifferentiableAt ℝ (fun x => (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (1 - 1)
⊢ False

case refine_2
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ DifferentiableAt ℝ (fun p => p * log p⁻¹) 1

Proof state:
p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
  <;> rintro rfl <;> unfold binEntropy at h

Result:
case refine_1
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False

case refine_2
h : DifferentiableAt ℝ (fun p => p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ False
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem IntermediateField.isSeparable_adjoin_simple_iff_isSeparable {x : E} :
    Algebra.IsSeparable F F⟮x⟯ ↔ IsSeparable F x

Proof state:
case refine_1
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
x✝ : Algebra.IsSeparable F ↥F⟮x⟯
⊢ IsSeparable F x

Tactic:
exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x

Result:
no goals

Proof state:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Tactic:
haveI := adjoin.finiteDimensional h

Result:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
this : FiniteDimensional F ↥F⟮x⟯
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Proof state:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
this : FiniteDimensional F ↥F⟮x⟯
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Tactic:
rwa [← finSepDegree_eq_finrank_iff,
  finSepDegree_adjoin_simple_eq_finrank_iff F E x h.isAlgebraic]

Result:
no goals

Proof state:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Tactic:
have h := IsSeparable.isIntegral hsep

Result:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable F x

Tactic:
refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩

Result:
case refine_1
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
x✝ : Algebra.IsSeparable F ↥F⟮x⟯
⊢ IsSeparable F x

case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯
-- Mathlib/Data/Real/Irrational.lean
theorem of_zpow : ∀ m : ℤ, Irrational (x ^ m) → Irrational x
  | (n : ℕ) => fun h => by
    rw [zpow_natCast] at h
    exact h.of_pow _
  | -[n+1] => fun h => by
    rw [zpow_negSucc] at h
    exact h.of_inv.of_pow _

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x

Tactic:
exact h.of_pow _

Result:
no goals

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x

Tactic:
exact h.of_inv.of_pow _

Result:
no goals

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x

Tactic:
rw [zpow_negSucc] at h

Result:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x

Tactic:
rw [zpow_natCast] at h

Result:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[simp]
lemma pullback.map_id {X Y Z : C}
    {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] :
    pullback.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (pullback f g)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem natAbs_euclideanDomain_gcd (a b : ℤ) :
    Int.natAbs (EuclideanDomain.gcd a b) = Int.gcd a b

Proof state:
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(a.gcd b)

Tactic:
exact Int.dvd_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)

Result:
no goals

Proof state:
case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ EuclideanDomain.gcd a b

Tactic:
exact EuclideanDomain.dvd_gcd Int.gcd_dvd_left Int.gcd_dvd_right

Result:
no goals

Proof state:
case a
a b : ℤ
⊢ ↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)

Tactic:
rw [Int.natAbs_dvd]

Result:
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(a.gcd b)

Proof state:
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b

Tactic:
apply Nat.dvd_antisymm <;> rw [← Int.natCast_dvd_natCast]

Result:
case a
a b : ℤ
⊢ ↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)

case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs

Proof state:
case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs

Tactic:
rw [Int.dvd_natAbs]

Result:
case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ EuclideanDomain.gcd a b
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem _root_.Set.Countable.ae_not_mem (h : s.Countable) (μ : Measure α) [NoAtoms μ] :
    ∀ᵐ x ∂μ, x ∉ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NoAtoms μ
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s

Tactic:
simpa only [ae_iff, Classical.not_not] using h.measure_zero μ

Result:
no goals