harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_sub (hf : Integrable f μ) (hg : Integrable g μ) (m : MeasurableSpace α) :
    μ[f - g|m] =ᵐ[μ] μ[f|m] - μ[g|m]

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f - g|m] =ᶠ[ae μ] μ[f|m] - μ[g|m]

Tactic:
simp_rw [sub_eq_add_neg]

Result:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f + -g|m] =ᶠ[ae μ] μ[f|m] + -μ[g|m]

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f + -g|m] =ᶠ[ae μ] μ[f|m] + -μ[g|m]

Tactic:
exact (condExp_add hf hg.neg _).trans (EventuallyEq.rfl.add (condExp_neg ..))

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem distortion_biUnionPrepartition (π : TaggedPrepartition I) (πi : ∀ J, Prepartition J) :
    (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
exact sup_biUnion _ _

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
lemma wbtw_iff_of_le {x y z : R} (hxz : x ≤ z) : Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Proof state:
case inl
R : Type u_1
inst✝ : LinearOrderedField R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x

Tactic:
rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
have hxz' : 0 < z - x := sub_pos.mpr hxz

Result:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Proof state:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
hy : y = r * (z - x) + x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
  mul_le_iff_le_one_left hxz', hxz.ne]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x = z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
subst hxz

Result:
case inl
R : Type u_1
inst✝ : LinearOrderedField R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x

Proof state:
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ y = r * (z - x) + x

Tactic:
simp [r, hxz'.ne']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz : x ≤ z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
cases hxz.eq_or_lt with
| inl hxz =>
  subst hxz
  rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
| inr hxz =>
  have hxz' : 0 < z - x := sub_pos.mpr hxz
  let r := (y - x) / (z - x)
  have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
  simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
    mul_le_iff_le_one_left hxz', hxz.ne]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
let r := (y - x) / (z - x)

Result:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Proof state:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']

Result:
case inr
R : Type u_1
inst✝ : LinearOrderedField R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
hy : y = r * (z - x) + x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_comm (x y : Nat) : x &&& y = y &&& x

Proof state:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x &&& y).testBit i = (y &&& x).testBit i

Tactic:
simp [Bool.and_comm]

Result:
no goals

Proof state:
x y : Nat
⊢ x &&& y = y &&& x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x &&& y).testBit i = (y &&& x).testBit i
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_right_cancel {x y} {c : S} (h : f.toMap (c * x) = f.toMap (c * y)) :
    f.toMap x = f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
⊢ f.toMap x = f.toMap y

Tactic:
let ⟨u, hu⟩ := f.map_units c

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
u : Nˣ
hu : ↑u = f.toMap ↑c
⊢ f.toMap x = f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
u : Nˣ
h : ↑u * f.toMap x = ↑u * f.toMap y
hu : ↑u = f.toMap ↑c
⊢ f.toMap x = f.toMap y

Tactic:
exact (Units.mul_right_inj u).1 h

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap (↑c * x) = f.toMap (↑c * y)
⊢ f.toMap x = f.toMap y

Tactic:
rw [f.toMap.map_mul, f.toMap.map_mul] at h

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
⊢ f.toMap x = f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
u : Nˣ
hu : ↑u = f.toMap ↑c
⊢ f.toMap x = f.toMap y

Tactic:
rw [← hu] at h

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
u : Nˣ
h : ↑u * f.toMap x = ↑u * f.toMap y
hu : ↑u = f.toMap ↑c
⊢ f.toMap x = f.toMap y
-- Mathlib/Algebra/Module/Torsion.lean
@[simp]
lemma infinite_range_add_smul_iff
    [AddCommGroup M] [Ring R] [Module R M] [Infinite R] [NoZeroSMulDivisors R M] (x y : M) :
    (Set.range <| fun r : R ↦ x + r • y).Infinite ↔ y ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ (Set.range fun r => x + r • y).Infinite ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
h : y ≠ 0
r s : R
hrs : x + r • y = x + s • y
⊢ r = s

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s

Tactic:
exact smul_left_injective _ h hrs

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
h : (Set.range fun r => x + r • y).Infinite
hy : y = 0
⊢ False

Tactic:
simp [hy] at h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
h : y ≠ 0
r s : R
hrs : x + r • y = x + s • y
⊢ r = s

Tactic:
rw [add_right_inj] at hrs

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Infinite R
inst✝ : NoZeroSMulDivisors R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_spec' (n : ℕ) :
    (∑ k ∈ antidiagonal n, ((k.1 + k.2).choose k.2 : ℚ) / (k.2 + 1) * bernoulli' k.1) = 1

Proof state:
n x : ℕ
hx : x ∈ range n.succ
⊢ ↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) / (↑(x, n - x).2 + 1) * bernoulli' (x, n - x).1 =
    ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x

Tactic:
simp only [add_tsub_cancel_of_le, mem_range_succ_iff.mp hx, cast_sub]

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1

Tactic:
refine ((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans ?_).trans (bernoulli'_spec n)

Result:
n : ℕ
⊢ ∑ k ∈ range n.succ,
      ↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) / (↑(k, n - k).2 + 1) * bernoulli' (k, n - k).1 =
    ∑ k ∈ range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k

Proof state:
n : ℕ
⊢ ∑ k ∈ range n.succ,
      ↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) / (↑(k, n - k).2 + 1) * bernoulli' (k, n - k).1 =
    ∑ k ∈ range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k

Tactic:
refine sum_congr rfl fun x hx => ?_

Result:
n x : ℕ
hx : x ∈ range n.succ
⊢ ↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) / (↑(x, n - x).2 + 1) * bernoulli' (x, n - x).1 =
    ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.finrank_add_finrank_orthogonal' [FiniteDimensional 𝕜 E] {K : Submodule 𝕜 E}
    {n : ℕ} (h_dim : finrank 𝕜 K + n = finrank 𝕜 E) : finrank 𝕜 Kᗮ = n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 ↥K + n = finrank 𝕜 E
⊢ finrank 𝕜 ↥Kᗮ = n

Tactic:
rw [← add_right_inj (finrank 𝕜 K)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 ↥K + n = finrank 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 ↥K + n = finrank 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + n

Tactic:
simp [Submodule.finrank_add_finrank_orthogonal, h_dim]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_conj (x : ℂ) (h : x.arg ≠ π) : log (conj x) = conj (log x)

Proof state:
x : ℂ
h : x.arg ≠ π
⊢ log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)

Tactic:
rw [log_conj_eq_ite, if_neg h]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem empty_infinite_Theory_isComplete : Language.empty.infiniteTheory.IsComplete :=
  (empty_theory_categorical.{0} ℵ₀ _).isComplete ℵ₀ _ le_rfl (by simp)
    ⟨by
      haveI : Language.empty.Structure ℕ := emptyStructure
      exact ((model_infiniteTheory_iff Language.empty).2 (inferInstanceAs (Infinite ℕ))).bundled⟩
    fun M => (model_infiniteTheory_iff Language.empty).1 M.is_model

Proof state:
⊢ lift.{0, 0} Language.empty.card ≤ lift.{0, 0} ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
this : Language.empty.Structure ℕ
⊢ Language.empty.infiniteTheory.ModelType

Tactic:
exact ((model_infiniteTheory_iff Language.empty).2 (inferInstanceAs (Infinite ℕ))).bundled

Result:
no goals

Proof state:
⊢ Language.empty.infiniteTheory.ModelType

Tactic:
haveI : Language.empty.Structure ℕ := emptyStructure

Result:
this : Language.empty.Structure ℕ
⊢ Language.empty.infiniteTheory.ModelType
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma stableUnderComposition :
    StableUnderComposition FormallyUnramified

Proof state:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x✝¹ : f.FormallyUnramified
x✝ : g.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.FormallyUnramified R S
algebraizeInst✝ : Algebra.FormallyUnramified S T
⊢ (g.comp f).FormallyUnramified

Tactic:
exact .comp R S T

Result:
no goals

Proof state:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x✝¹ : f.FormallyUnramified
x✝ : g.FormallyUnramified
⊢ (g.comp f).FormallyUnramified

Tactic:
algebraize [f, g, g.comp f]

Result:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x✝¹ : f.FormallyUnramified
x✝ : g.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.FormallyUnramified R S
algebraizeInst✝ : Algebra.FormallyUnramified S T
⊢ (g.comp f).FormallyUnramified

Proof state:
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] => FormallyUnramified

Tactic:
intros R S T _ _ _ f g _ _

Result:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x✝¹ : f.FormallyUnramified
x✝ : g.FormallyUnramified
⊢ (g.comp f).FormallyUnramified
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
/-- The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases
is the conjugate transpose of the matrix associated to the linear map. -/
lemma LinearMap.toMatrix_adjoint (f : E →ₗ[𝕜] F) :
    toMatrix v₂.toBasis v₁.toBasis (adjoint f) = (toMatrix v₁.toBasis v₂.toBasis f)ᴴ :=
  toLin v₂.toBasis v₁.toBasis |>.injective <| by simp [toLin_conjTranspose]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
f : E →ₗ[𝕜] F
⊢ (toLin v₂.toBasis v₁.toBasis) ((toMatrix v₂.toBasis v₁.toBasis) (adjoint f)) =
    (toLin v₂.toBasis v₁.toBasis) ((toMatrix v₁.toBasis v₂.toBasis) f)ᴴ

Tactic:
simp [toLin_conjTranspose]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
protected lemma _root_.IsClosed.everywherePosSubset (hs : IsClosed s) :
    IsClosed (μ.everywherePosSubset s)

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed (μ.everywherePosSubset s)

Tactic:
rw [hu]

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed (s \ u)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed s
⊢ IsClosed (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed (μ.everywherePosSubset s)

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed (s \ u)

Tactic:
exact hs.sdiff u_open

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem card_quotient_normalizer_modEq_card_quotient [Finite G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    {H : Subgroup G} (hH : Nat.card H = p ^ n) :
    Nat.card (normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) ≡
      Nat.card (G ⧸ H) [MOD p]

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≡ Nat.card (G ⧸ H) [MOD p]

Tactic:
exact ((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card (↥H.normalizer ⧸ comap H.normalizer.subtype H) ≡ Nat.card (G ⧸ H) [MOD p]

Tactic:
rw [← Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)]

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≡ Nat.card (G ⧸ H) [MOD p]
-- Mathlib/Algebra/Algebra/Operations.lean
theorem le_pow_toAddSubmonoid {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Proof state:
case inl
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ 1 ≤ toAddSubmonoid 1

Tactic:
exact le_one_toAddSubmonoid

Result:
no goals

Proof state:
case inl
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid

Tactic:
rw [Submodule.pow_zero, pow_zero]

Result:
case inl
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ 1 ≤ toAddSubmonoid 1

Proof state:
case inr
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
exact (pow_toAddSubmonoid M hn).ge

Result:
no goals

Proof state:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
obtain rfl | hn := Decidable.eq_or_ne n 0

Result:
case inl
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid

case inr
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
-- Mathlib/Topology/Path.lean
theorem continuous_uncurry_extend_of_continuous_family {ι : Type*} [TopologicalSpace ι]
    {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) :
    Continuous ↿fun t => (γ t).extend

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ Continuous ↿fun t => (γ t).extend

Tactic:
apply h.comp (continuous_id.prodMap continuous_projIcc)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous ↿γ
⊢ 0 ≤ 1
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapComp_eq {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    map (f ≫ g) = (map f) ⋙ (map g)

Proof state:
case h_map.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Over X
k : U ⟶ V
⊢ ((map (f ≫ g)).map k).left = (eqToHom ⋯ ≫ (map f ⋙ map g).map k ≫ eqToHom ⋯).left

Tactic:
simp

Result:
no goals

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map f ⋙ map g).map f_1 ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro U V k

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Over X
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map f ⋙ map g).map k ≫ eqToHom ⋯

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Over X), (map (f ≫ g)).obj X_1 = (map f ⋙ map g).obj X_1

Tactic:
simp [Over.map, Comma.mapRight]

Result:
no goals

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Over X
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map f ⋙ map g).map k ≫ eqToHom ⋯

Tactic:
ext

Result:
case h_map.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Over X
k : U ⟶ V
⊢ ((map (f ≫ g)).map k).left = (eqToHom ⋯ ≫ (map f ⋙ map g).map k ≫ eqToHom ⋯).left

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map f ⋙ map g

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Over X), (map (f ≫ g)).obj X_1 = (map f ⋙ map g).obj X_1

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map f ⋙ map g).map f_1 ≫ eqToHom ⋯)
    _auto✝