harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma _root_.isOpen.dynEntourage [TopologicalSpace X] {T : X → X} (T_cont : Continuous T)
    {U : Set (X × X)} (U_open : IsOpen U) (n : ℕ) :
    IsOpen (dynEntourage T U n)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous T
U : Set (X × X)
U_open : IsOpen U
n : ℕ
k : ↑(Ico 0 n)
⊢ IsOpen ((map T T)^[↑k] ⁻¹' U)

Tactic:
exact U_open.preimage ((T_cont.prodMap T_cont).iterate k)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous T
U : Set (X × X)
U_open : IsOpen U
n : ℕ
⊢ IsOpen (⋂ k, (map T T)^[↑k] ⁻¹' U)

Tactic:
refine isOpen_iInter_of_finite fun k ↦ ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous T
U : Set (X × X)
U_open : IsOpen U
n : ℕ
k : ↑(Ico 0 n)
⊢ IsOpen ((map T T)^[↑k] ⁻¹' U)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous T
U : Set (X × X)
U_open : IsOpen U
n : ℕ
⊢ IsOpen (Dynamics.dynEntourage T U n)

Tactic:
rw [dynEntourage_eq_inter_Ico T U n]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous T
U : Set (X × X)
U_open : IsOpen U
n : ℕ
⊢ IsOpen (⋂ k, (map T T)^[↑k] ⁻¹' U)
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_clm_apply {f : E → F →L[𝕜] G} {g : E → F} {s : Set E} {x : E}
    {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hn : n ≤ N) :
    ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) s x‖ ≤
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f✝ : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffOn 𝕜 N f✝ s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G).flip
f : F →L[𝕜] G
⊢ ‖f‖ ≤ ‖f‖

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_four : normEDS b c d 4 = d * b

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 4 = d * b

Tactic:
erw [normEDS_ofNat, preNormEDS'_four, if_pos <| by decide]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ Even 4

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma εIso_inv_freeMk (x : PUnit) : (εIso R).inv (freeMk x) = 1

Proof state:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.single x 1) PUnit.unit = 1

Tactic:
rw [Finsupp.single_eq_same]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.lapply PUnit.unit) (Finsupp.single x 1) = 1

Tactic:
erw [Finsupp.lapply_apply]

Result:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.single x 1) PUnit.unit = 1

Proof state:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (εIso R).inv) (freeMk x) = 1

Tactic:
dsimp [εIso, freeMk]

Result:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.lapply PUnit.unit) (Finsupp.single x 1) = 1
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.isIso_inl_iff_id_eq_fst_comp_inl (X Y : C) [HasBinaryBiproduct X Y] :
    IsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ 𝟙 (X ⊞ Y) = biprod.fst ≫ biprod.inl

Proof state:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : 𝟙 (X ⊞ Y) = fst ≫ inl
⊢ IsIso inl

Tactic:
exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

Result:
no goals

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl ↔ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
constructor

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl

case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
intro h

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
rw [this, IsIso.inv_hom_id]

Result:
no goals

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Proof state:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl

Tactic:
intro h

Result:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : 𝟙 (X ⊞ Y) = fst ≫ inl
⊢ IsIso inl
-- Mathlib/Data/List/Rotate.lean
theorem getElem_rotate (l : List α) (n : ℕ) (k : Nat) (h : k < (l.rotate n).length) :
    (l.rotate n)[k] =
      l[(k + n) % l.length]'(mod_lt _ (length_rotate l n ▸ k.zero_le.trans_lt h))

Proof state:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k] = l[(k + n) % l.length]

Tactic:
rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]

Result:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Proof state:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Tactic:
exact h.trans_eq (length_rotate _ _)

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem mem_sSup {Us : Set (Opens α)} {x : α} : x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Tactic:
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_incidenceSet_eq_degree [DecidableEq V] :
    Fintype.card (G.incidenceSet v) = G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(G.incidenceSet v) = G.degree v

Tactic:
rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v)]

Result:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(G.neighborSet v) = G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(G.neighborSet v) = G.degree v

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem single_zero (a : G) : (single a 0 : SkewMonoidAlgebra k G) = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
⊢ single a 0 = 0

Tactic:
rw [ofFinsupp_eq_zero, single, Finsupp.single_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem zero_mem_measurableLE : (0 : α → ℝ≥0∞) ∈ measurableLE μ ν :=
  ⟨measurable_zero, fun A _ ↦ by simp⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
A : Set α
x✝ : MeasurableSet A
⊢ ∫⁻ (x : α) in A, 0 x ∂μ ≤ ν A

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem forall_rightMoves_fuzzy_iff_equiv_zero : (∀ j, G.moveRight j ‖ 0) ↔ G ≈ 0

Proof state:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (j : G.RightMoves), G.moveRight j ‖ 0
⊢ G ≈ 0

Tactic:
rw [equiv_zero_iff_ge G, zero_le_lf]

Result:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (j : G.RightMoves), G.moveRight j ‖ 0
⊢ ∀ (j : G.RightMoves), 0 ⧏ G.moveRight j

Proof state:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.RightMoves
⊢ G.moveRight i ‖ 0

Tactic:
rw [fuzzy_zero_iff_gf]

Result:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.RightMoves
⊢ 0 ⧏ G.moveRight i

Proof state:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.RightMoves
⊢ 0 ⧏ G.moveRight i

Tactic:
exact hp.2.lf_moveRight i

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ (∀ (j : G.RightMoves), G.moveRight j ‖ 0) ↔ G ≈ 0

Tactic:
refine ⟨fun hb => ?_, fun hp i => ?_⟩

Result:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (j : G.RightMoves), G.moveRight j ‖ 0
⊢ G ≈ 0

case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.RightMoves
⊢ G.moveRight i ‖ 0

Proof state:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (j : G.RightMoves), G.moveRight j ‖ 0
⊢ ∀ (j : G.RightMoves), 0 ⧏ G.moveRight j

Tactic:
exact fun i => (hb i).2

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_inj [∀ i, NeBot (f₁ i)] : pi f₁ = pi f₂ ↔ f₁ = f₂

Proof state:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
⊢ f₁ = f₂

Tactic:
have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le

Result:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂

Proof state:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂

Tactic:
refine ⟨fun h => ?_, congr_arg pi⟩

Result:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
⊢ f₁ = f₂

Proof state:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂

Tactic:
haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)

Result:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), (f₂ i).NeBot
⊢ f₁ = f₂

Proof state:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), (f₂ i).NeBot
⊢ f₁ = f₂

Tactic:
exact hle.antisymm (pi_le_pi.1 h.ge)

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

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 ≫ fst (snd g g ≫ g) f ≫ fst g g = fst (fst f g) (fst f g) ≫ snd 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 ≫
      fst (snd g g ≫ g) f ≫ fst g g =
    fst (fst f g) (fst f g) ≫ snd f g

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 ≫
      fst (snd g g ≫ g) f ≫ fst g g =
    fst (fst f g) (fst f g) ≫ snd f g

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_map {l : List α} :
    (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b)

Proof state:
case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)

Tactic:
simp only [map, pairwise_cons, forall_mem_map, *]

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
l : List α
⊢ Pairwise R (map f l) ↔ Pairwise (fun a b => R (f a) (f b)) l

Tactic:
induction l

Result:
case nil
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []

case cons
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R (map f tail✝) ↔ Pairwise (fun a b => R (f a) (f b)) tail✝
⊢ Pairwise R (map f (head✝ :: tail✝)) ↔ Pairwise (fun a b => R (f a) (f b)) (head✝ :: tail✝)

Proof state:
case nil
α : Type u_1
α✝ : Type u_2
f : α → α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type*}
    (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) :
    ∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Proof state:
case insert
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i

Tactic:
have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi

Result:
case insert
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)
hU' : ∀ i ∈ t, IsOpen (U i)
⊢ ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen (U x) ∧ ∀ x ∈ t, IsOpen (U x)
hU' : ∀ i ∈ t, IsOpen (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ Membership.mem t.val, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ IsCompact (update K x K₁ i)

Tactic:
simp only [update_of_ne hi, h1K]

Result:
no goals
-- Mathlib/Analysis/Convex/Independent.lean
theorem ConvexIndependent.comp_embedding {ι' : Type*} (f : ι' ↪ ι) {p : ι → E}
    (hc : ConvexIndependent 𝕜 p) : ConvexIndependent 𝕜 (p ∘ f)

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ x ∈ s

Tactic:
rw [← f.injective.mem_set_image]

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ f x ∈ ⇑f '' s

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 (p ∘ ⇑f)

Tactic:
intro s x hx

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ p (f x) ∈ (convexHull 𝕜) (p '' (⇑f '' s))

Tactic:
rwa [Set.image_image]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ f x ∈ ⇑f '' s

Tactic:
exact hc _ _ (by rwa [Set.image_image])

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem comm_trans_lTensorOne :
    (TensorProduct.comm R _ _).trans M.lTensorOne = M.rTensorOne

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] (algebraMap R ↥⊥) x) =
    ↑M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) x)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne

Tactic:
refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun m r ↦ ?_

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Tactic:
rw [← h]

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] (algebraMap R ↥⊥) x) =
    ↑M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) x)

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)

Tactic:
replace h : algebraMap R _ x = r := Subtype.val_injective h

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
r : ↥⊥
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.cyclicPermutations {l l' : List α} (h : l ~r l') :
    l.cyclicPermutations ~r l'.cyclicPermutations

Proof state:
case intro
α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations ~r (l.rotate k).cyclicPermutations

Tactic:
exact ⟨k, by simp⟩

Result:
no goals

Proof state:
α : Type u
l l' : List α
h : l ~r l'
⊢ l.cyclicPermutations ~r l'.cyclicPermutations

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case intro
α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations ~r (l.rotate k).cyclicPermutations

Proof state:
α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations.rotate k = (l.rotate k).cyclicPermutations

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem X_eq_normalize : (X : Polynomial R) = normalize X

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
⊢ X = normalize X

Tactic:
simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ_self {n} {i : Fin (n + 2)} :
    X.δ (Fin.castSucc i) ≫ X.δ i = X.δ i.succ ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ_self]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op
-- Mathlib/Data/Set/Prod.lean
theorem diagonal_eq_univ_iff : diagonal α = univ ↔ Subsingleton α

Proof state:
α : Type u_1
⊢ diagonal α = univ ↔ Subsingleton α

Tactic:
simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Balanced.alter {t : RBNode α}
    (h : t.Balanced c n) : ∃ c n, (t.alter cut f).Balanced c n

Proof state:
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
⊢ ∃ c n, (path.insertNew y✝).Balanced c n

Tactic:
have ⟨_, _, .nil, h⟩ := h.zoom .root eq

Result:
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
h : Path.Balanced c n path black 0
⊢ ∃ c n, (path.insertNew y✝).Balanced c n

Proof state:
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
h : Path.Balanced c n path black 0
⊢ ∃ c n, (path.insertNew y✝).Balanced c n

Tactic:
exact ⟨_, h.insertNew⟩

Result:
no goals