harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Minimal.lean
theorem minimal_apply_mem_inter_range_iff :
    Minimal (· ∈ t ∩ range f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Proof state:
case refine_2
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
⊢ ∀ ⦃y : β⦄, (fun x => x ∈ t ∩ range ⇑f) y → y ≤ f x → f x ≤ y

Tactic:
rintro _ ⟨hyt, ⟨y, rfl⟩⟩

Result:
case refine_2.intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ f y ≤ f x → f x ≤ f y

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
⊢ f x ∈ range ⇑f

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ y ≤ x → x ≤ y

Tactic:
exact h.le_of_le hyt

Result:
no goals

Proof state:
case refine_1
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x => f x ∈ t) y
⊢ y ≤ x → x ≤ y

Tactic:
rw [← f.le_iff_le, ← f.le_iff_le]

Result:
case refine_1
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x => f x ∈ t) y
⊢ f y ≤ f x → f x ≤ f y

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal (fun x => x ∈ t ∩ range ⇑f) (f x) ↔ Minimal (fun x => f x ∈ t) x

Tactic:
refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, by simp⟩, ?_⟩⟩

Result:
case refine_1
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x => f x ∈ t) y
⊢ y ≤ x → x ≤ y

case refine_2
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
⊢ ∀ ⦃y : β⦄, (fun x => x ∈ t ∩ range ⇑f) y → y ≤ f x → f x ≤ y

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x => f x ∈ t) y
⊢ f y ∈ range ⇑f

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ f y ≤ f x → f x ≤ f y

Tactic:
simp_rw [f.le_iff_le]

Result:
case refine_2.intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => f x ∈ t) x
y : α
hyt : f y ∈ t
⊢ y ≤ x → x ≤ y

Proof state:
case refine_1
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x => x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x => f x ∈ t) y
⊢ f y ≤ f x → f x ≤ f y

Tactic:
exact h.le_of_le ⟨hy, by simp⟩

Result:
no goals
-- Mathlib/Topology/Order/LawsonTopology.lean
lemma singleton_isClosed (a : α) : IsClosed ({a} : Set α)

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithLawson.ofLawson ⁻¹' (↑(upperClosure {a}) ∩ ↑(lowerClosure {a})))

Tactic:
apply IsClosed.inter
  (lawsonClosed_of_lowerClosed _ (IsLower.isClosed_upperClosure (finite_singleton a)))

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed ↑(lowerClosure {a})

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithLawson.ofLawson ⁻¹' Iic a)

Tactic:
apply lawsonClosed_of_scottClosed

Result:
case h
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithScott.ofScott ⁻¹' Iic a)

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed {a}

Tactic:
rw [← (Set.OrdConnected.upperClosure_inter_lowerClosure ordConnected_singleton),
  ← WithLawson.isClosed_preimage_ofLawson]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithLawson.ofLawson ⁻¹' (↑(upperClosure {a}) ∩ ↑(lowerClosure {a})))

Proof state:
case h
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithScott.ofScott ⁻¹' Iic a)

Tactic:
exact IsScott.isClosed_Iic

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed ↑(lowerClosure {a})

Tactic:
rw [lowerClosure_singleton, LowerSet.coe_Iic, ← WithLawson.isClosed_preimage_ofLawson]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed (⇑WithLawson.ofLawson ⁻¹' Iic a)
-- Mathlib/Data/Multiset/Bind.lean
theorem mem_join {a S} : a ∈ @join α S ↔ ∃ s ∈ S, a ∈ s :=
  Multiset.induction_on S (by simp) <| by
    simp +contextual [or_and_right, exists_or]

Proof state:
α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ a ∈ join 0 ↔ ∃ s ∈ 0, a ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ ∀ (a_1 : Multiset α) (s : Multiset (Multiset α)),
    (a ∈ s.join ↔ ∃ s_1 ∈ s, a ∈ s_1) → (a ∈ (a_1 ::ₘ s).join ↔ ∃ s_1 ∈ a_1 ::ₘ s, a ∈ s_1)

Tactic:
simp +contextual [or_and_right, exists_or]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem antitoneOn (hf : LocallyBoundedVariationOn f s) {b : α} (bs : b ∈ s) :
    AntitoneOn (fun a => variationOnFromTo f s a b) s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b

Tactic:
exact le_add_of_nonneg_left (variationOnFromTo.nonneg_of_le f s ac)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ (fun a => variationOnFromTo f s a b) c ≤ (fun a => variationOnFromTo f s a b) a

Tactic:
dsimp only

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a b

Tactic:
rw [← variationOnFromTo.add hf as cs bs]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
⊢ AntitoneOn (fun a => variationOnFromTo f s a b) s

Tactic:
rintro a as c cs ac

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ (fun a => variationOnFromTo f s a b) c ≤ (fun a => variationOnFromTo f s a b) a
-- Mathlib/Computability/Primrec.lean
theorem sub : Nat.Primrec (unpaired (· - ·)) :=
  (prec .id ((pred.comp right).comp right)).of_eq fun p => by
    simp; induction p.unpair.2 <;> simp [*, Nat.sub_add_eq]

Proof state:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH => IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2

Tactic:
induction p.unpair.2 <;> simp [*, Nat.sub_add_eq]

Result:
no goals

Proof state:
p : ℕ
⊢ unpaired (fun z n => Nat.rec (id z) (fun y IH => (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.pred) n) p =
    unpaired (fun x1 x2 => x1 - x2) p

Tactic:
simp

Result:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH => IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
    filter p l = l'.push a ↔
      ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a ∧ (∀ x, x ∈ l₂ → ¬p x)

Proof state:
case mk
α : Type u_1
p : α → Bool
l' : Array α
a : α
l : List α
⊢ filter p { toList := l } = l'.push a ↔
    ∃ l₁ l₂, { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ filter p { toList := l } = { toList := l' }.push a ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_singleton {α : Type*} [PseudoMetricSpace α] (x : α) {δ : ℝ} (hδ : 0 ≤ δ) :
    cthickening δ ({x} : Set α) = closedBall x δ

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ cthickening δ {x} = closedBall x δ

Tactic:
ext y

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
y : α
⊢ y ∈ cthickening δ {x} ↔ y ∈ closedBall x δ

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
y : α
⊢ y ∈ cthickening δ {x} ↔ y ∈ closedBall x δ

Tactic:
simp [cthickening, edist_dist, ENNReal.ofReal_le_ofReal_iff hδ]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma erase_le_erase (ha : a ∈ s) (hb : b ∈ s) :
    toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a

Proof state:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a : α
inst✝ : DecidableEq α
ha hb : a ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase a } ↔ a ≤ a

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
  singleton_le_singleton]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a

Tactic:
classical
rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha,
  singleton_le_singleton]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a

Tactic:
obtain rfl | hab := eq_or_ne a b

Result:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a : α
inst✝ : DecidableEq α
ha hb : a ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase a } ↔ a ≤ a

case inr
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyGE_of_iso (n : ℤ) [K.IsStrictlyGE n] : L.IsStrictlyGE n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ L.IsStrictlyGE n

Tactic:
apply isStrictlySupported_of_iso e

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma dropLast_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) :
    (p.concat h).dropLast = p.copy rfl (by simp)

Proof state:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
simp [*]

Result:
no goals

Proof state:
case cons.hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil

Tactic:
simp [concat, nil_iff_length_eq]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
simp_rw [concat_cons]

Result:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ (cons h✝ (p✝.concat h)).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u✝ v✝ w t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ v = (p.concat h).penultimate

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ (cons h✝ (p✝.concat h)).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
rw [dropLast_cons_of_not_nil]

Result:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

case cons.hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil

Proof state:
case nil
V : Type u
G : SimpleGraph V
t u v u✝ : V
h : G.Adj u✝ t
⊢ (nil.concat h).dropLast = nil.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).dropLast = p.copy ⋯ ⋯

Tactic:
induction p

Result:
case nil
V : Type u
G : SimpleGraph V
t u v u✝ : V
h : G.Adj u✝ t
⊢ (nil.concat h).dropLast = nil.copy ⋯ ⋯

case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯
-- Mathlib/Topology/Separation/Basic.lean
theorem isClosedEmbedding_update {ι : Type*} {β : ι → Type*}
    [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)]
    (x : (i : ι) → β i) (i : ι) [(i : ι) → T1Space (β i)] :
    IsClosedEmbedding (update x i)

Proof state:
case hs
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ ∀ a ∈ univ, IsClosed (update (fun j => {x j}) i s a)

Tactic:
simp [forall_update_iff, hs, isClosed_singleton]

Result:
no goals

Proof state:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ IsClosed (update x i '' s)

Tactic:
rw [update_image]

Result:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ IsClosed (univ.pi (update (fun j => {x j}) i s))

Proof state:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ IsClosed (univ.pi (update (fun j => {x j}) i s))

Tactic:
apply isClosed_set_pi

Result:
case hs
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ ∀ a ∈ univ, IsClosed (update (fun j => {x j}) i s a)

Proof state:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
⊢ IsClosedEmbedding (update x i)

Tactic:
refine .of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
  (update_injective x i) fun s hs ↦ ?_

Result:
ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed s
⊢ IsClosed (update x i '' s)
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_norm_mk_eq (S : AddSubgroup M) (m : M) :
    ‖mk' S m‖ = sInf ((‖m + ·‖) '' S)

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖

Tactic:
simp only [dist_eq_norm', sub_neg_eq_add, add_comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖(mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)

Tactic:
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg_eq_neg,
  neg_coe_set (H := S), infDist_eq_iInf]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem choice_mem_aux (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) :
    (Classical.epsilon fun z : ZFSet.{u} => z ∈ y) ∈ y :=
  (@Classical.epsilon_spec _ fun z : ZFSet.{u} => z ∈ y) <|
    by_contradiction fun n => h <| by rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]

Proof state:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ ∅ ∈ x

Tactic:
rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
    x.2 < k + length l

Proof state:
α : Type u_1
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < k + l.length

Tactic:
rcases mem_iff_get.1 h with ⟨i, rfl⟩

Result:
case intro
α : Type u_1
l : List α
k : Nat
i : Fin (l.zipIdx k).length
h : (l.zipIdx k).get i ∈ l.zipIdx k
⊢ ((l.zipIdx k).get i).snd < k + l.length

Proof state:
case intro
α : Type u_1
l : List α
k : Nat
i : Fin (l.zipIdx k).length
h : (l.zipIdx k).get i ∈ l.zipIdx k
⊢ ((l.zipIdx k).get i).snd < k + l.length

Tactic:
simpa using i.isLt

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem inner_eq_mul_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
⊢ angle x y = 0

Tactic:
have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = 0

Tactic:
rw [angle, h, div_self h₁, Real.arccos_one]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y = ‖x‖ * ‖y‖ ↔ angle x y = 0

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

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = ‖x‖ * ‖y‖
⊢ angle x y = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldlM_push [Monad m] [LawfulMonad m] (l : Vector α n) (a : α) (f : β → α → m β) (b) :
    (l.push a).foldlM f b = l.foldlM f b >>= fun b => f b a

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
a : α
f : β → α → m β
b : β
⊢ foldlM f b (l.push a) = do
    let b ← foldlM f b l
    f b a

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
f : β → α → m β
b : β
l : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ }.push a) = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    f b a

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
f : β → α → m β
b : β
l : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ }.push a) = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    f b a

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_compact : IsCompact (convexBodySum K B)

Proof state:
case h.e'_3.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x✝ : mixedSpace K
⊢ x✝ ∈ convexBodySum K B ↔ x✝ ∈ convexBodySumFun ⁻¹' Set.Icc 0 B

Tactic:
simp [convexBodySumFun_nonneg]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsCompact (convexBodySum K B)

Tactic:
classical
rw [Metric.isCompact_iff_isClosed_bounded]
refine ⟨?_, convexBodySum_isBounded K B⟩
convert IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
ext
simp [convexBodySumFun_nonneg]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsCompact (convexBodySum K B)

Tactic:
rw [Metric.isCompact_iff_isClosed_bounded]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsClosed (convexBodySum K B) ∧ Bornology.IsBounded (convexBodySum K B)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsClosed (convexBodySum K B)

Tactic:
convert IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))

Result:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ convexBodySum K B = convexBodySumFun ⁻¹' Set.Icc 0 B

Proof state:
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ convexBodySum K B = convexBodySumFun ⁻¹' Set.Icc 0 B

Tactic:
ext

Result:
case h.e'_3.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x✝ : mixedSpace K
⊢ x✝ ∈ convexBodySum K B ↔ x✝ ∈ convexBodySumFun ⁻¹' Set.Icc 0 B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsClosed (convexBodySum K B) ∧ Bornology.IsBounded (convexBodySum K B)

Tactic:
refine ⟨?_, convexBodySum_isBounded K B⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsClosed (convexBodySum K B)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_antiperiodic : Function.Antiperiodic cos (π : Angle)

Proof state:
θ : Angle
⊢ (θ + ↑π).cos = -θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).cos = -(↑x✝).cos

Proof state:
⊢ Function.Antiperiodic cos ↑π

Tactic:
intro θ

Result:
θ : Angle
⊢ (θ + ↑π).cos = -θ.cos

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).cos = -(↑x✝).cos

Tactic:
exact Real.cos_antiperiodic _

Result:
no goals