harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem seq_norm_le (n : ℕ) :
    Int.natAbs (Algebra.norm ℤ (seq K w₁ hB n : 𝓞 K)) ≤ B

Proof state:
case succ
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ |(Algebra.norm ℚ) ↑↑(seq K w₁ hB (n + 1))| ≤ ↑B

Tactic:
exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : B < 1
⊢ ↑(convexBodyLTFactor K) * ↑B ≤ minkowskiBound K 1

Tactic:
simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ 1 ≤ B

Tactic:
contrapose! hB

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : B < 1
⊢ ↑(convexBodyLTFactor K) * ↑B ≤ minkowskiBound K 1

Proof state:
case succ
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB (n + 1))).natAbs ≤ B

Tactic:
rw [← Nat.cast_le (α := ℚ), Int.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]

Result:
case succ
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ |(Algebra.norm ℚ) ↑↑(seq K w₁ hB (n + 1))| ≤ ↑B

Proof state:
case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : 1 ≤ B
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB 0)).natAbs ≤ B

Tactic:
simp only [ne_eq, seq, map_one, Int.natAbs_one, this]

Result:
no goals

Proof state:
case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB 0)).natAbs ≤ B

Tactic:
have : 1 ≤ B := by
  contrapose! hB
  simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]

Result:
case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : 1 ≤ B
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB 0)).natAbs ≤ B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B

Tactic:
cases n with
| zero =>
    have : 1 ≤ B := by
      contrapose! hB
      simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]
    simp only [ne_eq, seq, map_one, Int.natAbs_one, this]
| succ n =>
    rw [← Nat.cast_le (α := ℚ), Int.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]
    exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.image_of_continuousOn_injOn [OpensMeasurableSpace β]
    [tγ : TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ]
    (hs : MeasurableSet s)
    (f_cont : ContinuousOn f s) (f_inj : InjOn f s) : MeasurableSet (f '' s)

Proof state:
case intro.intro.intro.intro
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁴ : T2Space β
s : Set γ
f : γ → β
inst✝³ : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed s
right✝ : IsOpen s
⊢ MeasurableSet (f '' s)

Tactic:
exact
  @IsClosed.measurableSet_image_of_continuousOn_injOn γ t' t'_polish β _ _ _ _ s s_closed f
    (f_cont.mono_dom t't) f_inj

Result:
no goals

Proof state:
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁴ : T2Space β
s : Set γ
f : γ → β
inst✝³ : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
  hs.isClopenable

Result:
case intro.intro.intro.intro
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁴ : T2Space β
s : Set γ
f : γ → β
inst✝³ : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed s
right✝ : IsOpen s
⊢ MeasurableSet (f '' s)
-- Mathlib/Topology/Order/Compact.lean
theorem cocompact_le_atBot [OrderTop α] [CompactIccSpace α] :
    cocompact α ≤ atBot

Proof state:
case refine_2.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩

Result:
case refine_2.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝¹ : Set α
hs : x✝¹ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝¹
x✝ : α
hx : x✝ ∈ (Icc t ⊤)ᶜ
⊢ x✝ ∈ x✝¹

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot

Tactic:
refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro

Result:
case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Proof state:
case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs

Result:
case refine_2.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Proof state:
case refine_2.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝¹ : Set α
hs : x✝¹ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝¹
x✝ : α
hx : x✝ ∈ (Icc t ⊤)ᶜ
⊢ x✝ ∈ x✝¹

Tactic:
exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_le h)) (fun h ↦ (h le_top).elim)

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem toSeq_ofSeq (s : Seq α) : toSeq (ofSeq s) = s

Proof state:
case a.h.a
α : Type u
s : Seq α
n : ℕ
⊢ ↑s n ∈ (↑s).get? n

Tactic:
rw [get?_ofSeq]

Result:
case a.h.a
α : Type u
s : Seq α
n : ℕ
⊢ ↑s n ∈ Computation.pure (s.get? n)

Proof state:
α : Type u
s : Seq α
⊢ (↑s).toSeq = s

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
s : Seq α
⊢ ↑(↑s).toSeq = ↑s

Proof state:
case a
α : Type u
s : Seq α
⊢ ↑(↑s).toSeq = ↑s

Tactic:
funext n

Result:
case a.h
α : Type u
s : Seq α
n : ℕ
⊢ ↑(↑s).toSeq n = ↑s n

Proof state:
case a.h
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).get = ↑s n

Tactic:
apply get_eq_of_mem

Result:
case a.h.a
α : Type u
s : Seq α
n : ℕ
⊢ ↑s n ∈ (↑s).get? n

Proof state:
case a.h
α : Type u
s : Seq α
n : ℕ
⊢ ↑(↑s).toSeq n = ↑s n

Tactic:
dsimp [toSeq]

Result:
case a.h
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).get = ↑s n

Proof state:
case a.h.a
α : Type u
s : Seq α
n : ℕ
⊢ ↑s n ∈ Computation.pure (s.get? n)

Tactic:
apply ret_mem

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
@[simp]
lemma powersetCard_eq_empty : powersetCard n s = ∅ ↔ s.card < n

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ → #s < n

Tactic:
contrapose!

Result:
α : Type u_1
n : ℕ
s : Finset α
⊢ n ≤ #s → powersetCard n s ≠ ∅

Proof state:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ #(powersetCard n s) = 0

Tactic:
rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ n ≤ #s → powersetCard n s ≠ ∅

Tactic:
exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Finset α
h : n ≤ #s
⊢ ∀ (a : Finset α), a ⊆ s ∧ #a = n → a ∈ powersetCard n s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ ↔ #s < n

Tactic:
refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩

Result:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ → #s < n
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_le_ker_coord (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n}
    (h : k ≤ l.castSucc) : b.flag k ≤ LinearMap.ker (b.coord l)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
⊢ b.flag k ≤ LinearMap.ker (b.coord l)

Tactic:
nontriviality R

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
a✝ : Nontrivial R
⊢ b.flag k ≤ LinearMap.ker (b.coord l)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
a✝ : Nontrivial R
⊢ b.flag k ≤ LinearMap.ker (b.coord l)

Tactic:
exact b.flag_le_ker_coord_iff.2 h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Extra.lean
theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i

Proof state:
case mk
s : String
pos : Pos
h : pos.byteIdx < s.endPos.byteIdx
⊢ s.utf8ByteSize - (s.next pos).byteIdx < s.utf8ByteSize - pos.byteIdx

Tactic:
exact Nat.sub_lt_sub_left h (String.lt_next s pos)

Result:
no goals

Proof state:
case mk
s : String
pos : Pos
h : { s := s, i := pos }.hasNext = true
⊢ sizeOf { s := s, i := pos }.next < sizeOf { s := s, i := pos }

Tactic:
simp [Iterator.next, Iterator.sizeOf_eq]

Result:
case mk
s : String
pos : Pos
h : { s := s, i := pos }.hasNext = true
⊢ s.utf8ByteSize - (s.next pos).byteIdx < s.utf8ByteSize - pos.byteIdx

Proof state:
i : Iterator
h : i.hasNext = true
⊢ sizeOf i.next < sizeOf i

Tactic:
cases i

Result:
case mk
s✝ : String
i✝ : Pos
h : { s := s✝, i := i✝ }.hasNext = true
⊢ sizeOf { s := s✝, i := i✝ }.next < sizeOf { s := s✝, i := i✝ }

Proof state:
case mk
s : String
pos : Pos
h : { s := s, i := pos }.hasNext = true
⊢ s.utf8ByteSize - (s.next pos).byteIdx < s.utf8ByteSize - pos.byteIdx

Tactic:
simp [Iterator.hasNext] at h

Result:
case mk
s : String
pos : Pos
h : pos.byteIdx < s.endPos.byteIdx
⊢ s.utf8ByteSize - (s.next pos).byteIdx < s.utf8ByteSize - pos.byteIdx

Proof state:
case mk
s✝ : String
i✝ : Pos
h : { s := s✝, i := i✝ }.hasNext = true
⊢ sizeOf { s := s✝, i := i✝ }.next < sizeOf { s := s✝, i := i✝ }

Tactic:
rename_i s pos

Result:
case mk
s : String
pos : Pos
h : { s := s, i := pos }.hasNext = true
⊢ sizeOf { s := s, i := pos }.next < sizeOf { s := s, i := pos }
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem infinite_iff {α : Type u} : Infinite α ↔ ℵ₀ ≤ #α

Proof state:
α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Map.lean
theorem comap_atTop (e : α ≃o β) : comap e atTop = atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ comap (⇑e) atTop = atTop

Tactic:
simp [atTop, ← e.surjective.iInf_comp]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Red.Step.lift {f : α → β} (H : Red.Step L₁ L₂) : Lift.aux f L₁ = Lift.aux f L₂

Proof state:
case not
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

Tactic:
cases b <;> simp [Lift.aux]

Result:
no goals

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂

Tactic:
obtain @⟨_, _, _, b⟩ := H

Result:
case not
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_univ :
    TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p

Tactic:
simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then none else l.getLast?

Proof state:
α : Type u_1
l : List α
⊢ l.tail.getLast? = if l.length = 1 then none else l.getLast?

Tactic:
match l with
| [] => simp
| [a] => simp
| _ :: _ :: l =>
  simp only [tail_cons, length_cons, getLast?_cons_cons]
  rw [if_neg]
  rintro ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
⊢ (head✝¹ :: head✝ :: l).tail.getLast? =
    if (head✝¹ :: head✝ :: l).length = 1 then none else (head✝¹ :: head✝ :: l).getLast?

Tactic:
simp only [tail_cons, length_cons, getLast?_cons_cons]

Result:
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
⊢ (head✝ :: l).getLast? = if l.length + 1 + 1 = 1 then none else (head✝ :: l).getLast?

Proof state:
α : Type u_1
l : List α
a : α
⊢ [a].tail.getLast? = if [a].length = 1 then none else [a].getLast?

Tactic:
simp

Result:
no goals

Proof state:
case hnc
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
⊢ ¬l.length + 1 + 1 = 1

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
⊢ (head✝ :: l).getLast? = if l.length + 1 + 1 = 1 then none else (head✝ :: l).getLast?

Tactic:
rw [if_neg]

Result:
case hnc
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
⊢ ¬l.length + 1 + 1 = 1

Proof state:
α : Type u_1
l : List α
⊢ [].tail.getLast? = if [].length = 1 then none else [].getLast?

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_insert_of_eq [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k = .eq) :
    (t.insert k v).find? k' = some v

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ (t.insert k v).find? k' = some v

Tactic:
rw [find?, findEntry?_insert_of_eq _ h]

Result:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v
-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_coeff_zero (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
    (v : Fin 0 → E) (v' : Fin 0 → F) : (q.comp p) 0 v = q 0 v'

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ (q.comp p 0) v = (q 0) v'

Tactic:
dsimp [FormalMultilinearSeries.comp]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ (∑ c : Composition 0, q.compAlongComposition p c) v = (q 0) v'

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ {c} = Finset.univ

Tactic:
apply Finset.eq_of_subset_of_card_le <;> simp [Finset.card_univ, composition_card 0]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
@[simp]
lemma toFinite_apply_eq_zero_iff [SFinite μ] {s : Set α} : μ.toFinite s = 0 ↔ μ s = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ.toFinite s = 0 ↔ μ s = 0

Tactic:
simp only [← compl_mem_ae_iff, ae_toFinite]

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
lemma cons_support : (s.cons y).support ⊆ insert 0 (s.support.map (Fin.succEmb n))

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
this : i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ ∀ (a : Fin n), i = a.succ → ¬s a = 0 ∧ a.succ = i

Tactic:
rintro i rfl

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬s i = 0 ∧ i.succ = i.succ

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i

Tactic:
apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ ∀ (a : Fin n), i = a.succ → ¬s a = 0 ∧ a.succ = i

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ (cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
intro i hi

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬s i = 0 ∧ i.succ = i.succ

Tactic:
simpa [Finsupp.mem_support_iff] using hi

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma add_zero_inv_app (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X) ≫
      eqToHom (by dsimp; rw [add_zero])

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (n + 0)).obj X

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (𝟭 C).obj ((h.F n).obj X) = (h.F (n + 0)).obj X

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (n + 0)).obj X

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
  Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
    a[i]?.getD d = if p : i < a.size then a[i]'p else d

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
⊢ a[i]?.getD d = if p : i < a.size then a[i] else d

Tactic:
if h : i < a.size then
  simp [h, getElem?_def]
else
  have p : i ≥ a.size := Nat.le_of_not_gt h
  simp [getElem?_eq_none p, h]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
h : i < a.size
⊢ a[i]?.getD d = if p : i < a.size then a[i] else d

Tactic:
simp [h, getElem?_def]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
h : ¬i < a.size
⊢ a[i]?.getD d = if p : i < a.size then a[i] else d

Tactic:
have p : i ≥ a.size := Nat.le_of_not_gt h

Result:
α : Type u_1
a : Array α
i : Nat
d : α
h : ¬i < a.size
p : i ≥ a.size
⊢ a[i]?.getD d = if p : i < a.size then a[i] else d

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
h : ¬i < a.size
p : i ≥ a.size
⊢ a[i]?.getD d = if p : i < a.size then a[i] else d

Tactic:
simp [getElem?_eq_none p, h]

Result:
no goals
-- Mathlib/Data/Fintype/Powerset.lean
@[simp] lemma univ_filter_card_eq (k : ℕ) :
   ({s | #s = k} : Finset (Finset α)) = univ.powersetCard k

Proof state:
case h
α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => #s = k) univ ↔ a✝ ∈ powersetCard k univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ filter (fun s => #s = k) univ = powersetCard k univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => #s = k) univ ↔ a✝ ∈ powersetCard k univ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
    get? m a = get? m b

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a b : α
hab : (a == b) = true
⊢ get? m a = get? m b

Tactic:
simp_to_raw using Raw₀.Const.get?_congr

Result:
no goals