harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Compact.lean
theorem isCompact_Ico_iff {a b : α} : IsCompact (Set.Ico a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ico_iff.mp h.isClosed, by simp_all⟩

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ico a b)

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem lift_symm_apply (F : FreeAlgebra R X →ₐ[R] A) : (lift R).symm F = F ∘ ι R

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ (lift R).symm F = ⇑F ∘ ι R

Tactic:
rw [lift]

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm F = ⇑F ∘ ι R

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm F = ⇑F ∘ ι R

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Injective.lean
theorem injective_object_of_injective_module [inj : Injective R M] :
    CategoryTheory.Injective (ModuleCat.of R M) where
  factors g f m :=
    have ⟨l, h⟩ := inj.out f.hom ((ModuleCat.mono_iff_injective f).mp m) g.hom
    ⟨ModuleCat.ofHom l, by ext x; simpa using h x⟩

Proof state:
case hf.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x

Tactic:
simpa using h x

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
ext x

Result:
case hf.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x
-- Mathlib/Probability/Independence/Basic.lean
theorem iIndepSets_singleton_iff {s : ι → Set Ω} :
    iIndepSets (fun i ↦ {s i}) μ ↔ ∀ t, μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)

Proof state:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
⊢ iIndepSets (fun i => {s i}) μ ↔ ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)

Tactic:
simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
  Kernel.const_apply]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma prod_top (L : Sublattice α) : L.prod (⊤ : Sublattice β) = L.comap LatticeHom.fst :=
  ext fun a ↦ by simp [mem_prod, LatticeHom.coe_fst]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
a : α × β
⊢ a ∈ L.prod ⊤ ↔ a ∈ comap LatticeHom.fst L

Tactic:
simp [mem_prod, LatticeHom.coe_fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forM_map [Monad m] [LawfulMonad m] (l : List α) (g : α → β) (f : β → m PUnit) :
    forM (l.map g) f = forM l (fun a => f (g a))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
g : α → β
f : β → m PUnit
⊢ forM (map g l) f = forM l fun a => f (g a)

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_single (a : α) (n : ℕ) : toMultiset (single a n) = n • {a}

Proof state:
α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0

Tactic:
apply zero_nsmul

Result:
no goals

Proof state:
α : Type u_1
a : α
n : ℕ
⊢ toMultiset (single a n) = n • {a}

Tactic:
rw [toMultiset_apply, sum_single_index]

Result:
α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂]
    [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
    coprod.map f g ≫ coprod.map h k = coprod.map (f ≫ h) (g ≫ k)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryCoproduct A₁ B₁
inst✝¹ : HasBinaryCoproduct A₂ B₂
inst✝ : HasBinaryCoproduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ map f g ≫ map h k = map (f ≫ h) (g ≫ k)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
@[simp] lemma preimage_inr (s : Finset (α ⊕ β)) :
    s.preimage Sum.inr Sum.inr_injective.injOn = s.toRight

Proof state:
α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inr ⋯ = s.toRight

Tactic:
ext x

Result:
case h
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight

Proof state:
case h
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma isCondKernelCDF_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    IsCondKernelCDF (fun p : Unit × α ↦ condCDF ρ p.2) (Kernel.const Unit ρ)
      (Kernel.const Unit ρ.fst)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p => stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
exact isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_preCDF ρ)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p => condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p => stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_eq_hammingNorm [∀ i, AddGroup (β i)] (x y : ∀ i, β i) :
    hammingDist x y = hammingNorm (x - y)

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (x - y)

Tactic:
simp_rw [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
@[simp]
lemma mem_ofSign {s : ℤˣ} {σ : Perm α} : σ ∈ ofSign s ↔ σ.sign = s

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ℤˣ
σ : Perm α
⊢ σ ∈ ofSign s ↔ sign σ = s

Tactic:
rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.even_odd₅ (a b c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 5)
    (hc : a / 2 = c) (hr : jacobiSymNat c b = r) : jacobiSymNat a b = -r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Result:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Proof state:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
norm_num

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
simp [hb]

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.ofNat_ediv, Nat.cast_ofNat]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_zero : (0 : A)⁻ = 0

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
⊢ 0⁻ = 0

Tactic:
simp [negPart_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
private lemma tendsto_log_one_sub_sub_log_nhdsGT_atAtop :
    Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[>] 0) atTop

Proof state:
case hf
h₁ : 0 < 1 / 2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

Tactic:
filter_upwards [Ioc_mem_nhdsGT h₁] with p hx

Result:
case h
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ log (1 / 2) ≤ log (1 - p)

Proof state:
⊢ Tendsto (fun p => log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
apply Filter.tendsto_atTop_add_left_of_le' (𝓝[>] 0) (log (1/2) : ℝ)

Result:
case hf

⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

case hg

⊢ Tendsto (fun x => -log x) (𝓝[>] 0) atTop

Proof state:
case h
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ log (1 / 2) ≤ log (1 - p)

Tactic:
gcongr

Result:
case h.hxy
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ 1 / 2 ≤ 1 - p

Proof state:
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h.hxy
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ 1 / 2 ≤ 1 - p

Tactic:
linarith [hx.2]

Result:
no goals

Proof state:
case hg

⊢ Tendsto (fun x => -log x) (𝓝[>] 0) atTop

Tactic:
apply tendsto_neg_atTop_iff.mpr tendsto_log_nhdsWithin_zero_right

Result:
no goals

Proof state:
case hf

⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

Tactic:
have h₁ : (0 : ℝ) < 1 / 2 := by norm_num

Result:
case hf
h₁ : 0 < 1 / 2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem natCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
    (d : ℕ) (hd : d ≠ 0) :
    PosDef (d : Matrix n n R) :=
  ⟨isHermitian_natCast _, fun x hx => by
    simp only [natCast_mulVec, dotProduct_smul]
    rw [Nat.cast_smul_eq_nsmul]
    exact nsmul_pos (dotProduct_star_self_pos_iff.mpr hx) hd⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ ↑d *ᵥ x

Tactic:
simp only [natCast_mulVec, dotProduct_smul]

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
x : n → R
hx : x ≠ 0
⊢ 0 < ↑d • (star x ⬝ᵥ x)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
x : n → R
hx : x ≠ 0
⊢ 0 < ↑d • (star x ⬝ᵥ x)

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
x : n → R
hx : x ≠ 0
⊢ 0 < d • (star x ⬝ᵥ x)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
x : n → R
hx : x ≠ 0
⊢ 0 < d • (star x ⬝ᵥ x)

Tactic:
exact nsmul_pos (dotProduct_star_self_pos_iff.mpr hx) hd

Result:
no goals
-- Mathlib/Data/Int/Basic.lean
lemma pow_right_injective (h : 1 < a.natAbs) : ((a ^ ·) : ℕ → ℤ).Injective

Proof state:
case h.e'_3.h
a : ℤ
h : 1 < a.natAbs
x✝ : ℕ
⊢ (natAbs ∘ fun x => a ^ x) x✝ = a.natAbs ^ x✝

Tactic:
rw [Function.comp_apply, natAbs_pow]

Result:
no goals

Proof state:
a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective (natAbs ∘ fun x => a ^ x)

Tactic:
convert Nat.pow_right_injective h using 2

Result:
case h.e'_3.h
a : ℤ
h : 1 < a.natAbs
x✝ : ℕ
⊢ (natAbs ∘ fun x => a ^ x) x✝ = a.natAbs ^ x✝
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem ker_eq_bot_iff_range_eq_top [FiniteDimensional K V] {f : V →ₗ[K] V} :
    LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ ker f = ⊥ ↔ range f = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem two_mul (n : α) : 2 * n = n + n :=
  (congrArg₂ _ one_add_one_eq_two.symm rfl).trans <| (right_distrib 1 1 n).trans (by rw [one_mul])

Proof state:
α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Definability.lean
theorem mvPolynomial_zeroLocus_definable {ι K : Type*} [Field K]
    [CompatibleRing K] (S : Finset (MvPolynomial ι K)) :
    Set.Definable (⋃ p ∈ S, p.coeff '' p.support : Set K) Language.ring
      (zeroLocus (Ideal.span (S : Set (MvPolynomial ι K))))

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, {x | ∀ p ∈ ↑S, (eval x) p = 0} = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
refine ⟨BoundedFormula.iInf
    (fun i : S => Term.equal
      ((termOfFreeCommRing (p' i)).relabel
        (Sum.map (fun p => ⟨p.1.1.coeff p.2.1, by
          simp only [Set.mem_iUnion]
          exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩⟩) id)) 0), ?_⟩

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ {x | ∀ p ∈ ↑S, (eval x) p = 0} =
    {v |
      Formula.Realize
        (BoundedFormula.iInf fun i =>
          (Term.relabel (Sum.map (fun p => ⟨coeff ↑p.snd ↑p.fst, ⋯⟩) id) (termOfFreeCommRing (p' i))).equal 0)
        (Sum.elim Subtype.val v)}
-- Mathlib/CategoryTheory/Equivalence.lean
theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
    (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)

Tactic:
dsimp [funInvIdAssoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (𝟙 (F.obj X) ≫ F.map (e.unitIso.hom.app X)) ≫ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) = F.map (e.unit.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (𝟙 (F.obj X) ≫ F.map (e.unitIso.hom.app X)) ≫ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) = F.map (e.unit.app X)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem le_symmDiff_iff_right : b ≤ a ∆ b ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ a ∆ b ↔ Disjoint a b

Tactic:
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_hom_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).hom ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).hom ≫
      snd (snd g g ≫ g) f =
    fst (fst f g) (fst f g) ≫ fst f g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ snd (snd g g ≫ g) f = fst (fst f g) (fst f g) ≫ fst f g

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).hom ≫
      snd (snd g g ≫ g) f =
    fst (fst f g) (fst f g) ≫ fst f g
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_pred : ∀ {n}, 0 < n → ((n - 1 : ℕ) : R) = n - 1
  | 0, h => by cases h
  | n + 1, _ => by rw [cast_succ, add_sub_cancel_right]; rfl

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1

Tactic:
rw [cast_succ, add_sub_cancel_right]

Result:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1

Tactic:
cases h

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracket_smul_right
    (hW : MDifferentiableAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) x) :
    mlieBracket I V (c • W) x = c • mlieBracket I V W x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
⊢ mlieBracket I V (c • W) x = c • mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hW ⊢

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
⊢ mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
⊢ mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_smul_right hW (uniqueMDiffWithinAt_univ _)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem hasEigenvector_of_isMinOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
    (hextr : IsMinOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
    HasEigenvector (T : E →ₗ[𝕜] E) (↑(⨅ x : { x : E // x ≠ 0 }, T.rayleighQuotient x)) x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T) (↑(⨅ x, T.rayleighQuotient ↑x)) x₀

Tactic:
convert hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inl hextr.localize)

Result:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ⨅ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀

Proof state:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.rayleighQuotient x₀ ≤ T.rayleighQuotient x

Tactic:
simp only [ContinuousLinearMap.rayleighQuotient]

Result:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x / ‖x‖ ^ 2

Proof state:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x / ‖x₀‖ ^ 2

Tactic:
gcongr

Result:
case h.e'_7.h.e'_3.hab
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x₀ ≤ T.reApplyInnerSelf x
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_pair_le_of_mem_of_mem {p₁ p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) : line[k, p₁, p₂] ≤ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ p₂ ∈ ↑s

Tactic:
exact ⟨hp₁, hp₂⟩

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
inst✝ : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ affineSpan k {p₁, p₂} ≤ s

Tactic:
rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ p₂ ∈ ↑s