harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem essSup_measure_restrict (hs : IsFundamentalDomain G s μ) {f : α → ℝ≥0∞}
    (hf : ∀ γ : G, ∀ x : α, f (γ • x) = f x) : essSup f (μ.restrict s) = essSup f μ

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f μ ≤ essSup f (μ.restrict s)

Tactic:
rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem closure_inv (s : Set G) : closure s⁻¹ = (closure s)⁻¹

Proof state:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

Tactic:
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]

Result:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)

Proof state:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)

Tactic:
exact subset_closure

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹

Tactic:
apply le_antisymm

Result:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹

Proof state:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹

Tactic:
rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]

Result:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)

Proof state:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)

Tactic:
exact subset_closure

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.isRegular {R : Type*} [Ring R] {p : R[X]} (hp : Monic p) : IsRegular p

Proof state:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

Tactic:
intro q r h

Result:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r

Proof state:
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRegular p

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Proof state:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
intro q r h

Result:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r

Proof state:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
⊢ q = r

Tactic:
rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r

Tactic:
simp only at h

Result:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q = r

Proof state:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r

Tactic:
dsimp only at h

Result:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
⊢ q = r

Proof state:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q = r

Tactic:
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.finite {M : Matroid α} [M.Finite] (h : N ≤r M) : N.Finite

Proof state:
α : Type u_1
N M : Matroid α
inst✝ : M.Finite
h : N ≤r M
⊢ N.Finite

Tactic:
obtain ⟨R, hR, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Finite

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Finite

Tactic:
exact restrict_finite <| M.ground_finite.subset hR

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_sub_right (h : a ∣ b) : a ∣ b - c ↔ a ∣ c

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c

Tactic:
rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
lemma eq_induced : haveI := F.reflects_preregular
    regularTopology C =
      F.inducedTopology (regularTopology _)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
⊢ regularTopology C = F.inducedTopology (regularTopology D)

Tactic:
ext X S

Result:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
⊢ S ∈ (regularTopology C) X ↔ S ∈ (F.inducedTopology (regularTopology D)) X

Proof state:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
rw [← mem_sieves_iff_hasEffectiveEpi S]

Result:
no goals

Proof state:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ S ∈ (F.inducedTopology (regularTopology D)) X

Tactic:
rw [← exists_effectiveEpi_iff_mem_induced F X]

Result:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Proof state:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
⊢ S ∈ (regularTopology C) X ↔ S ∈ (F.inducedTopology (regularTopology D)) X

Tactic:
have := F.reflects_preregular

Result:
case h.h.h
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ S ∈ (F.inducedTopology (regularTopology D)) X
-- Mathlib/Condensed/Discrete/Colimit.lean
lemma isoLocallyConstantOfIsColimit_inv (X : LightProfinite.{u}ᵒᵖ ⥤ Type u)
    [PreservesFiniteProducts X] (hX : ∀ S : LightProfinite.{u}, (IsColimit <|
      X.mapCocone (coconeRightOpOfCone S.asLimitCone))) :
    (isoLocallyConstantOfIsColimit X hX).inv =
      (CompHausLike.LocallyConstant.counitApp.{u, u} X)

Proof state:
case w.h.w
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (fun f => ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g

Tactic:
simp only [← Category.assoc]

Result:
case w.h.w
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ ((fun f => ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv) ≫ X.map g =
    (counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem image_eq_inter_preimage_of_subset_support {s : Set M} (hs : s ⊆ support f) :
    extChartAt I c '' s =
      closedBall (extChartAt I c c) f.rOut ∩ range I ∩ (extChartAt I c).symm ⁻¹' s

Proof state:
case intro.h₂
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c) '' s

Tactic:
refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_

Result:
case intro.h₂
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ (extChartAt I c).target ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c) '' s

Proof state:
case intro.h₁.refine_1.intro.intro
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
x : M
⊢ ↑(extChartAt I c) x ∈ range ↑I

Tactic:
exact mem_range_self _

Result:
no goals

Proof state:
case intro.h₂
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ (extChartAt I c).target ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c) '' s

Tactic:
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem eq_preimage (f : r ↪r s) : r = f ⁻¹'o s

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ r = ⇑f ⁻¹'o s

Tactic:
ext a b

Result:
case h.h.a
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (⇑f ⁻¹'o s) a b

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (⇑f ⁻¹'o s) a b

Tactic:
exact f.map_rel_iff.symm

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mk_zero : mk 0 = 0

Proof state:
⊢ mk 0 = { cauchy := 0 }

Tactic:
rfl

Result:
no goals

Proof state:
⊢ mk 0 = 0

Tactic:
rw [← ofCauchy_zero]

Result:
⊢ mk 0 = { cauchy := 0 }
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_lt_one_iff {e : ℝ≥0} {m : ℤₘ₀} (he : 1 < e) :
    toNNReal (ne_zero_of_lt he) m < 1 ↔ m < 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m < 1 ↔ m < 1

Tactic:
simp_rw [this]

Result:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m < (toNNReal ⋯) 1 ↔ m < 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
⊢ (toNNReal ⋯) m < 1 ↔ m < 1

Tactic:
have : 1 = (toNNReal (ne_zero_of_lt he)) 1 := rfl

Result:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m < 1 ↔ m < 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m < (toNNReal ⋯) 1 ↔ m < 1

Tactic:
exact StrictMono.lt_iff_lt (toNNReal_strictMono he)

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem Flat.pointed {S : ConvexCone 𝕜 E} (hS : S.Flat) : S.Pointed

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ S.Pointed

Tactic:
rw [Pointed, ← add_neg_cancel x]

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ x + -x ∈ S

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ x + -x ∈ S

Tactic:
exact add_mem S hx hxneg

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
hS : S.Flat
⊢ S.Pointed

Tactic:
obtain ⟨x, hx, _, hxneg⟩ := hS

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
x : E
hx : x ∈ S
left✝ : x ≠ 0
hxneg : -x ∈ S
⊢ S.Pointed
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem div_sat' {c : Constraint} {x y} (h : Coeffs.gcd x ≠ 0) (w : c.sat (Coeffs.dot x y)) :
    (c.div (Coeffs.gcd x)).sat' (Coeffs.sdiv x (Coeffs.gcd x)) y

Proof state:
c : Constraint
x y : Coeffs
h : x.gcd ≠ 0
w : c.sat (x.dot y) = true
⊢ (c.div x.gcd).sat' (x.sdiv ↑x.gcd) y = true

Tactic:
dsimp [sat']

Result:
c : Constraint
x y : Coeffs
h : x.gcd ≠ 0
w : c.sat (x.dot y) = true
⊢ (c.div x.gcd).sat ((x.sdiv ↑x.gcd).dot y) = true

Proof state:
c : Constraint
x y : Coeffs
h : x.gcd ≠ 0
w : c.sat (x.dot y) = true
⊢ (c.div x.gcd).sat (x.dot y / ↑x.gcd) = true

Tactic:
exact div_sat c _ (Coeffs.gcd x) h (Coeffs.gcd_dvd_dot_left x y) w

Result:
no goals

Proof state:
c : Constraint
x y : Coeffs
h : x.gcd ≠ 0
w : c.sat (x.dot y) = true
⊢ (c.div x.gcd).sat ((x.sdiv ↑x.gcd).dot y) = true

Tactic:
rw [Coeffs.dot_sdiv_left _ _ (Int.dvd_refl _)]

Result:
c : Constraint
x y : Coeffs
h : x.gcd ≠ 0
w : c.sat (x.dot y) = true
⊢ (c.div x.gcd).sat (x.dot y / ↑x.gcd) = true
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem coe_inf (I J : WithBot (Box ι)) : (↑(I ⊓ J) : Set (ι → ℝ)) = (I : Set _) ∩ J

Proof state:
case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(mk' (a✝¹.lower ⊔ a✝.lower) (a✝¹.upper ⊓ a✝.upper)) = ↑↑a✝¹ ∩ ↑↑a✝

Tactic:
simp only [coe_eq_pi, ← pi_inter_distrib, Ioc_inter_Ioc, Pi.sup_apply, Pi.inf_apply, coe_mk',
  coe_coe]

Result:
no goals

Proof state:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ∅ = ↑↑a✝ ∩ ↑⊥

Tactic:
simp

Result:
no goals

Proof state:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ↑(⊥ ⊓ J) = ↑⊥ ∩ ↑J

Tactic:
change ∅ = _

Result:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ∅ = ↑⊥ ∩ ↑J

Proof state:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑(I ⊓ J) = ↑I ∩ ↑J

Tactic:
induction I

Result:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ↑(⊥ ⊓ J) = ↑⊥ ∩ ↑J

case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ J) = ↑↑a✝ ∩ ↑J

Proof state:
case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ J) = ↑↑a✝ ∩ ↑J

Tactic:
induction J

Result:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ ⊥) = ↑↑a✝ ∩ ↑⊥

case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(↑a✝¹ ⊓ ↑a✝) = ↑↑a✝¹ ∩ ↑↑a✝

Proof state:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ ⊥) = ↑↑a✝ ∩ ↑⊥

Tactic:
change ∅ = _

Result:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ∅ = ↑↑a✝ ∩ ↑⊥

Proof state:
case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(↑a✝¹ ⊓ ↑a✝) = ↑↑a✝¹ ∩ ↑↑a✝

Tactic:
change ((mk' _ _ : WithBot (Box ι)) : Set (ι → ℝ)) = _

Result:
case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(mk' (a✝¹.lower ⊔ a✝.lower) (a✝¹.upper ⊓ a✝.upper)) = ↑↑a✝¹ ∩ ↑↑a✝

Proof state:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ∅ = ↑⊥ ∩ ↑J

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem sum_lineCount_eq_sum_pointCount [Fintype P] [Fintype L] :
    ∑ p : P, lineCount L p = ∑ l : L, pointCount P l

Proof state:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ ∑ p : P, lineCount L p = ∑ l : L, pointCount P l

Tactic:
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]

Result:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card ((i : P) × { l // i ∈ l }) = Fintype.card ((i : L) × { p // p ∈ i })

Proof state:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card ((i : P) × { l // i ∈ l }) = Fintype.card ((i : L) × { p // p ∈ i })

Tactic:
apply Fintype.card_congr

Result:
case f
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ (i : P) × { l // i ∈ l } ≃ (i : L) × { p // p ∈ i }
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem exists_mul_add_sub_mem_of_mem_jacobson {I : Ideal R} (r : R) (h : r ∈ jacobson I) :
    ∃ s, s * (r + 1) - 1 ∈ I

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
⊢ ∃ s, s * (r + 1) - 1 ∈ I

Tactic:
obtain ⟨s, hs⟩ := mem_jacobson_iff.1 h 1

Result:
case intro
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ ∃ s, s * (r + 1) - 1 ∈ I

Proof state:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * r + s - 1 ∈ I

Tactic:
simpa using hs

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ ∃ s, s * (r + 1) - 1 ∈ I

Tactic:
use s

Result:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I

Proof state:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I

Tactic:
rw [mul_add, mul_one]

Result:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * r + s - 1 ∈ I
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendsto_prod_principal_iff {c : β} :
    Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun _ => c) p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p (𝓟 s)

Tactic:
exact tendsto_prod_filter_iff

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun x => c) p s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p (𝓟 s)
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Equiv.Perm.viaFintypeEmbedding_apply_image (a : α) :
    e.viaFintypeEmbedding f (f a) = f (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.extendDomain f.toEquivRange) (f a) = f (e a)

Tactic:
convert Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.viaFintypeEmbedding f) (f a) = f (e a)

Tactic:
rw [Equiv.Perm.viaFintypeEmbedding]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.extendDomain f.toEquivRange) (f a) = f (e a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem zero_addChar_byteIdx (c : Char) : ((0 : Pos) + c).byteIdx = c.utf8Size

Proof state:
c : Char
⊢ (0 + c).byteIdx = c.utf8Size

Tactic:
simp only [addChar_byteIdx, byteIdx_zero, Nat.zero_add]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem compact_open_separated_mul_left {K U : Set G} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), V * K ⊆ U

Proof state:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ ∃ V ∈ 𝓝 1, V * K ⊆ U

Tactic:
refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩

Result:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, V * K ⊆ U

Tactic:
rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
    (image_subset op hKU) with
  ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩

Result:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ ∃ V ∈ 𝓝 1, V * K ⊆ U

Proof state:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U

Tactic:
rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
  preimage_image_eq _ op_injective] at hV'

Result:
no goals