harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMConfig.lean
theorem Cont.then_eval {k k' : Cont} {v} : (k.then k').eval v = k.eval v >>= k'.eval

Proof state:
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((fix a✝¹ a✝).then k').eval v = (fix a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, *]

Result:
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a✝.eval v.tail >>= k'.eval else a✝¹.fix.eval v.tail >>= (a✝.then k').eval) =
    (if v.headI = 0 then a✝.eval v.tail else a✝¹.fix.eval v.tail >>= a✝.eval) >>= k'.eval

Proof state:
case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((comp a✝¹ a✝).then k').eval v = (comp a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]

Result:
no goals

Proof state:
case fix
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ (if v.headI = 0 then a✝.eval v.tail >>= k'.eval else a✝¹.fix.eval v.tail >>= (a✝.then k').eval) =
    (if v.headI = 0 then a✝.eval v.tail else a✝¹.fix.eval v.tail >>= a✝.eval) >>= k'.eval

Tactic:
split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

Result:
no goals

Proof state:
case cons₂
k' : Cont
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((cons₂ a✝¹ a✝).then k').eval v = (cons₂ a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, *]

Result:
no goals

Proof state:
case halt
k' : Cont
v : List ℕ
⊢ (halt.then k').eval v = halt.eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, pure_bind]

Result:
no goals

Proof state:
k k' : Cont
v : List ℕ
⊢ (k.then k').eval v = k.eval v >>= k'.eval

Tactic:
induction k generalizing v with
| halt => simp only [Cont.eval, Cont.then, pure_bind]
| cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
| cons₂ => simp only [Cont.eval, Cont.then, *]
| comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
| fix _ _ k_ih =>
  simp only [Cont.eval, Cont.then, *]
  split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

Result:
no goals

Proof state:
case cons₁
k' : Cont
a✝² : Code
a✝¹ : List ℕ
a✝ : Cont
a_ih✝ : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((cons₁ a✝² a✝¹ a✝).then k').eval v = (cons₁ a✝² a✝¹ a✝).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_set (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :
    (v.set i x hi)[j] = if i = j then x else v[j]

Proof state:
case mk
α : Type u_1
n i : Nat
x : α
hi : i < n
j : Nat
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i x hi)[j] =
    if i = j then x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]

Tactic:
split <;> simp_all [Array.getElem_set]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
hi : i < n
j : Nat
hj : j < n
⊢ (v.set i x hi)[j] = if i = j then x else v[j]

Tactic:
cases v

Result:
case mk
α : Type u_1
n i : Nat
x : α
hi : i < n
j : Nat
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i x hi)[j] =
    if i = j then x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma neg_comp
    {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
    (-α).comp β h = -α.comp β h

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y Z : C
inst✝ : Preadditive C
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (-α).comp β h = -α.comp β h

Tactic:
rw [comp, comp, Preadditive.neg_comp]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_apply {i i' b} :
    (single i b : Π₀ i, β i) i' = if h : i = i' then Eq.recOn h b else 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (single i b) i' = if h : i = i' then Eq.recOn h b else 0

Tactic:
rw [single_eq_pi_single, Pi.single, Function.update]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0

Tactic:
simp [@eq_comm _ i i']

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isLittleO_deriv_one_sub_smoothingFn :
    deriv (fun x => 1 - ε x) =o[atTop] fun (x : ℝ) => x⁻¹ := calc
  deriv (fun x => 1 - ε x) =ᶠ[atTop] fun z => -(deriv ε z)

Proof state:
⊢ (fun z => -deriv ε z) =o[atTop] fun x => x⁻¹

Tactic:
rw [isLittleO_neg_left]

Result:
⊢ deriv ε =o[atTop] fun x => x⁻¹

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 - ε x) x = -deriv ε x

Tactic:
rw [deriv_sub] <;> aesop

Result:
no goals

Proof state:
⊢ deriv ε =o[atTop] fun x => x⁻¹

Tactic:
exact isLittleO_deriv_smoothingFn

Result:
no goals

Proof state:
⊢ (deriv fun x => 1 - ε x) =ᶠ[atTop] fun z => -deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 - ε x) x = -deriv ε x
-- Mathlib/Data/Finset/Card.lean
theorem card_le_one_iff_subset_singleton [Nonempty α] : #s ≤ 1 ↔ ∃ x : α, s ⊆ {x}

Proof state:
case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1

Tactic:
rintro ⟨x, hx⟩

Result:
case refine_2.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ 1

Proof state:
case refine_1.inr.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}

Tactic:
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}

Tactic:
rw [card_le_one.1 H y hy x hx, mem_singleton]

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ 1

Tactic:
rw [← card_singleton x]

Result:
case refine_2.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}

Proof state:
case refine_1.inl
α : Type u_1
inst✝ : Nonempty α
H : #∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

Tactic:
exact ⟨Classical.arbitrary α, empty_subset _⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
⊢ ∃ x, s ⊆ {x}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case refine_1.inl
α : Type u_1
inst✝ : Nonempty α
H : #∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

case refine_1.inr.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}

Proof state:
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ #s ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
refine ⟨fun H => ?_, ?_⟩

Result:
case refine_1
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
⊢ ∃ x, s ⊆ {x}

case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1

Proof state:
case refine_2.intro
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}

Tactic:
exact card_le_card hx

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem card_mul_index : Nat.card H * H.index = Nat.card G

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H * H.index = Nat.card G

Tactic:
rw [← relindex_bot_left, ← index_bot]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relindex H * H.index = ⊥.index

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relindex H * H.index = ⊥.index

Tactic:
exact relindex_mul_index bot_le

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_of_not_mem (s) (h : a ∉ t) : insert a s \ t = insert a (s \ t)

Proof state:
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
⊢ insert a s \ t = insert a (s \ t)

Tactic:
ext x

Result:
case h
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

Proof state:
case pos
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
h' : x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

Tactic:
simp [h, h', ne_of_mem_of_not_mem h' h]

Result:
no goals

Proof state:
case h
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

Tactic:
by_cases h' : x ∈ t

Result:
case pos
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
h' : x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

case neg
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
h' : x ∉ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

Proof state:
case neg
α : Type u
t : Set α
a : α
s : Set α
h : a ∉ t
x : α
h' : x ∉ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

Tactic:
simp [h, h']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_deleteVerts (s s' : Set V) :
    (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

Tactic:
ext <;> simp +contextual [not_or, and_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k fallback : α}
    (h' : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.getKeyD k fallback = m.getKeyD k fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k fallback : α
h' : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp_to_model [insertMany] using List.getKeyD_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_dedup (s : Multiset α) : (dedup s).lcm = s.lcm :=
  Multiset.induction_on s (by simp) fun a s IH ↦ by
    by_cases h : a ∈ s <;> simp [IH, h]
    unfold lcm
    rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
    apply lcm_eq_of_associated_left (associated_normalize _)

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ s.lcm = GCDMonoid.lcm a s.lcm

Tactic:
unfold lcm

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
by_cases h : a ∈ s <;> simp [IH, h]

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ s.lcm = GCDMonoid.lcm a s.lcm

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) = GCDMonoid.lcm (normalize a) (fold GCDMonoid.lcm 1 (s.erase a))

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) = GCDMonoid.lcm (normalize a) (fold GCDMonoid.lcm 1 (s.erase a))

Tactic:
apply lcm_eq_of_associated_left (associated_normalize _)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).lcm = lcm 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is unique. -/
lemma ExpChar.eq {p q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q

Proof state:
case zero.zero
R : Type u_1
inst✝² : AddMonoidWithOne R
inst✝¹ inst✝ : CharZero R
⊢ 1 = 1

case zero.prime
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : CharZero R
hq' : Nat.Prime q
hchar✝ : CharP R q
⊢ 1 = q

Tactic:
exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q

Tactic:
rcases hq with hq | hq'

Result:
case prime.zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp' : Nat.Prime p
hchar✝ : CharP R p
inst✝ : CharZero R
⊢ p = 1

case prime.prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp' : Nat.Prime p
hchar✝¹ : CharP R p
hq' : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q

Proof state:
case prime.zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp' : Nat.Prime p
hchar✝ : CharP R p
inst✝ : CharZero R
⊢ p = 1

case prime.prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp' : Nat.Prime p
hchar✝¹ : CharP R p
hq' : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q

Tactic:
exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
  CharP.eq R ‹_› ‹_›]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst✝ : CharZero R
⊢ 1 = q

Tactic:
rcases hq with hq | hq'

Result:
case zero.zero
R : Type u_1
inst✝² : AddMonoidWithOne R
inst✝¹ inst✝ : CharZero R
⊢ 1 = 1

case zero.prime
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : CharZero R
hq' : Nat.Prime q
hchar✝ : CharP R q
⊢ 1 = q

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
⊢ p = q

Tactic:
rcases hp with ⟨hp⟩ | ⟨hp'⟩

Result:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst✝ : CharZero R
⊢ 1 = q

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q
-- Mathlib/GroupTheory/Order/Min.lean
@[to_additive]
lemma le_minOrder_iff_forall_subgroup {n : ℕ∞} :
    n ≤ minOrder α ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (s : Set α).Finite → n ≤ Nat.card s

Proof state:
α : Type u_1
inst✝ : Group α
n : ℕ∞
⊢ (∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)) ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

Tactic:
refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup α
hs : s ≠ ⊥
hs' : (↑s).Finite
⊢ n ≤ ↑(Nat.card ↥s)

case refine_2
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : α
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf a)

Proof state:
α : Type u_1
inst✝ : Group α
n : ℕ∞
⊢ n ≤ minOrder α ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

Tactic:
rw [le_minOrder]

Result:
α : Type u_1
inst✝ : Group α
n : ℕ∞
⊢ (∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)) ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

Proof state:
case refine_1
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup α
hs : s ≠ ⊥
hs' : (↑s).Finite
⊢ n ≤ ↑(Nat.card ↥s)

Tactic:
obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs

Result:
case refine_1.intro.intro
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup α
hs : s ≠ ⊥
hs' : (↑s).Finite
a : α
has : a ∈ s
ha : a ≠ 1
⊢ n ≤ ↑(Nat.card ↥s)

Proof state:
case refine_2
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : α
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf a)

Tactic:
simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
inst✝ : Group α
n : ℕ∞
h : ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup α
hs : s ≠ ⊥
hs' : (↑s).Finite
a : α
has : a ∈ s
ha : a ≠ 1
⊢ n ≤ ↑(Nat.card ↥s)

Tactic:
exact
  (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
    (WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
/-- Induction principle for finset families. To prove a statement for every finset family,
it suffices to prove it for
* the empty finset family.
* the finset family which only contains the empty finset.
* `ℬ ∪ {s ∪ {a} | s ∈ 𝒞}` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the
  ground type and `𝒜` and `ℬ` are families of finsets not containing `a`.
  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you
  `𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, so that `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.

This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.

See also `Finset.family_induction_on.` -/
@[elab_as_elim]
lemma memberFamily_induction_on {p : Finset (Finset α) → Prop}
    (𝒜 : Finset (Finset α)) (empty : p ∅) (singleton_empty : p {∅})
    (subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
      p (𝒜.nonMemberSubfamily a) → p (𝒜.memberSubfamily a) → p 𝒜) : p 𝒜

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s = ∅
⊢ p 𝒜

Tactic:
rw [← subset_singleton_iff', subset_singleton_iff] at hu

Result:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ p 𝒜

Proof state:
case insert.refine_1
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u

Tactic:
simp only [mem_nonMemberSubfamily, and_imp]

Result:
case insert.refine_1
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ 𝒜, a ∉ s → s ⊆ u
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[ext]
lemma hom_ext {C D : HomologicalComplex V c} (f g : C ⟶ D)
    (h : ∀ i, f.f i = g.f i) : f = g

Proof state:
case f.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
x✝ : ι
⊢ f.f x✝ = g.f x✝

Tactic:
apply h

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f = g

Tactic:
apply Hom.ext

Result:
case f
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f.f = g.f

Proof state:
case f
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f.f = g.f

Tactic:
funext

Result:
case f.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
x✝ : ι
⊢ f.f x✝ = g.f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_succ_ne_empty (n : Nat) (a : α) : mkArray (n+1) a ≠ #[]

Proof state:
α : Type u_1
n : Nat
a : α
⊢ mkArray (n + 1) a ≠ #[]

Tactic:
simp [mkArray_succ]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem tendsto_leftLim (x : α) : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x = ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x ≠ ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x ≠ ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
rw [leftLim_eq_sSup hf h']

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x ≠ ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x ≠ ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
exact hf.tendsto_nhdsLT x

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[<] x = ⊥
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
simp [h']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma IsHamiltonianCycle.support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a ≠ b) :
    p.support.count b = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.support = 1

Tactic:
rw [← cons_support_tail p hp.1.not_nil, List.count_cons_of_ne h.symm, hp.isHamiltonian_tail]

Result:
no goals