harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_eq_sInf [CompleteLattice α] [SuccOrder α] (a : α) :
    succ a = sInf (Set.Ioi a)

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_sInf fun b => succ_le_of_lt).antisymm

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Result:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ succ ⊤

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a

Proof state:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ succ ⊤

Tactic:
rw [succ_top]

Result:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ ⊤

Proof state:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a

Tactic:
exact sInf_le (lt_succ_iff_ne_top.2 ha)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
private lemma prop_red_S (hS : ∀ B, C B → C (S • B)) (B) : C (S • B) ↔ C B

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C B

Tactic:
rw [← (S_smul_four B)]

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C (S • S • S • S • B)

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) → C B

Tactic:
intro ih

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C B

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C (S • S • S • S • B)

Tactic:
solve_by_elim

Result:
no goals

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) ↔ C B

Tactic:
refine ⟨?_, hS _⟩

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) → C B
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem atEnd : ∀ {it}, ValidFor l r it → (it.atEnd ↔ r = [])
  | it, h => by
    simp only [Iterator.atEnd, h.pos, h.toString, endPos_eq, utf8Len_reverseAux, ge_iff_le,
      decide_eq_true_eq]
    exact Nat.add_le_add_iff_left.trans <| Nat.le_zero.trans utf8Len_eq_zero

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l + utf8Len r ≤ utf8Len l ↔ r = []

Tactic:
exact Nat.add_le_add_iff_left.trans <| Nat.le_zero.trans utf8Len_eq_zero

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.atEnd = true ↔ r = []

Tactic:
simp only [Iterator.atEnd, h.pos, h.toString, endPos_eq, utf8Len_reverseAux, ge_iff_le,
  decide_eq_true_eq]

Result:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l + utf8Len r ≤ utf8Len l ↔ r = []
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_convergent {s : ℝ} (h : 0 < s) :
    IntegrableOn (fun x : ℝ => exp (-x) * x ^ (s - 1)) (Ioi 0)

Proof state:
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume ∧
    IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
constructor

Result:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume

case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Proof state:
case right
s : ℝ
h : 0 < s
⊢ ContinuousOn (fun x => rexp (-x) * x ^ (s - 1)) (Ici 1)

Tactic:
refine continuousOn_id.neg.rexp.mul (continuousOn_id.rpow_const ?_)

Result:
case right
s : ℝ
h : 0 < s
⊢ ∀ x ∈ Ici 1, id x ≠ 0 ∨ 0 ≤ s - 1

Proof state:
s : ℝ
h : 0 < s
⊢ -1 < s - 1

Tactic:
linarith

Result:
no goals

Proof state:
case right
s : ℝ
h : 0 < s
⊢ ∀ x ∈ Ici 1, id x ≠ 0 ∨ 0 ≤ s - 1

Tactic:
intro x hx

Result:
case right
s : ℝ
h : 0 < s
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0 ∨ 0 ≤ s - 1

Proof state:
case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
refine integrable_of_isBigO_exp_neg one_half_pos ?_ (Gamma_integrand_isLittleO _).isBigO

Result:
case right
s : ℝ
h : 0 < s
⊢ ContinuousOn (fun x => rexp (-x) * x ^ (s - 1)) (Ici 1)

Proof state:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume

Tactic:
rw [← integrableOn_Icc_iff_integrableOn_Ioc]

Result:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume

Proof state:
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
rw [← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrableOn_union]

Result:
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume ∧
    IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Proof state:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume

Tactic:
refine IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp ?_ isCompact_Icc

Result:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => x ^ (s - 1)) (Icc 0 1) volume

Proof state:
case left
s : ℝ
h : 0 < s
⊢ IntervalIntegrable (fun x => x ^ (s - 1)) volume 0 1

Tactic:
exact intervalIntegrable_rpow' (by linarith)

Result:
no goals

Proof state:
case right
s : ℝ
h : 0 < s
x : ℝ
hx : x ∈ Ici 1
⊢ id x ≠ 0 ∨ 0 ≤ s - 1

Tactic:
exact Or.inl ((zero_lt_one : (0 : ℝ) < 1).trans_le hx).ne'

Result:
no goals

Proof state:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x => x ^ (s - 1)) (Icc 0 1) volume

Tactic:
refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Result:
case left
s : ℝ
h : 0 < s
⊢ IntervalIntegrable (fun x => x ^ (s - 1)) volume 0 1
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_eq_right_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) :
    gcd a b = b ↔ b ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ gcd a b = b ↔ b ∣ a

Tactic:
simpa only [gcd_comm a b] using gcd_eq_left_iff b a h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
    {v : β k} :
    getEntry? a (replaceEntry k v l) = if containsKey k l ∧ k == a then some ⟨k, v⟩ else
      getEntry? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
cases h : k == a

Result:
case true.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
h : (k == a) = false
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ false = true then some ⟨k, v⟩ else getEntry? a l

case true.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
h : (k == a) = true
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ true = true then some ⟨k, v⟩ else getEntry? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
⊢ getEntry? a (replaceEntry k v l) = if containsKey k l = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
cases hl : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = false
⊢ getEntry? a (replaceEntry k v l) = if false = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = false
⊢ getEntry? a (replaceEntry k v l) = if false = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [getEntry?_replaceEntry_of_containsKey_eq_false hl]

Result:
no goals

Proof state:
case true.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
h : (k == a) = true
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ true = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [getEntry?_replaceEntry_of_true hl h]

Result:
no goals

Proof state:
case true.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
h : (k == a) = false
⊢ getEntry? a (replaceEntry k v l) = if true = true ∧ false = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [getEntry?_replaceEntry_of_false h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_attach {l : Array α} : l.attach.unattach = l

Proof state:
α : Type u_1
l : Array α
⊢ l.attach.unattach = l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.unattach = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.unattach = { toList := toList✝ }

Tactic:
simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
lemma LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ}
    (hs : abscissaOfAbsConv f < s.re) : LSeriesSummable f s

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
y : ℝ
hy : LSeriesSummable f ↑y
hys : y < s.re
⊢ LSeriesSummable f s

Tactic:
exact hy.of_re_le_re <| ofReal_re y ▸ hys.le

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
⊢ LSeriesSummable f s

Tactic:
obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
  simpa [abscissaOfAbsConv, sInf_lt_iff] using hs

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
y : ℝ
hy : LSeriesSummable f ↑y
hys : y < s.re
⊢ LSeriesSummable f s

Proof state:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
⊢ ∃ a, LSeriesSummable f ↑a ∧ a < s.re

Tactic:
simpa [abscissaOfAbsConv, sInf_lt_iff] using hs

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hamming_zero_eq_dist {x y : ∀ i, β i} : 0 = hammingDist x y ↔ x = y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 = hammingDist x y ↔ x = y

Tactic:
rw [eq_comm, hammingDist_eq_zero]

Result:
no goals
-- Mathlib/Order/Disjointed.lean
theorem preimage_find_eq_disjointed (s : ℕ → Set α) (H : ∀ x, ∃ n, x ∈ s n)
    [∀ x n, Decidable (x ∈ s n)] (n : ℕ) : (fun x => Nat.find (H x)) ⁻¹' {n} = disjointed s n

Proof state:
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
⊢ (fun x => Nat.find ⋯) ⁻¹' {n} = disjointed s n

Tactic:
ext x

Result:
case h
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ x ∈ (fun x => Nat.find ⋯) ⁻¹' {n} ↔ x ∈ disjointed s n

Proof state:
case h
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ x ∈ (fun x => Nat.find ⋯) ⁻¹' {n} ↔ x ∈ disjointed s n

Tactic:
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2 ≤ exp x :=
  calc
    1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / i !

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = 1 / (↑0 + 1) + x / (↑0 + 1) + x ^ 2 / (↑0 + 1 + 1)

Tactic:
ring_nf

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / ↑i !

Tactic:
simp only [sum_range_succ, range_one, sum_singleton, _root_.pow_zero, factorial, cast_one,
  ne_eq, one_ne_zero, not_false_eq_true, div_self, pow_one, mul_one, div_one, Nat.mul_one,
  cast_succ, add_right_inj]

Result:
x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = 1 / (↑0 + 1) + x / (↑0 + 1) + x ^ 2 / (↑0 + 1 + 1)
-- Mathlib/SetTheory/Lists.lean
theorem ofList_subset {l₁ l₂ : List (Lists α)} (h : l₁ ⊆ l₂) :
    Lists'.ofList l₁ ⊆ Lists'.ofList l₂

Proof state:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList

Tactic:
simp only [List.cons_subset] at h

Result:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList

Proof state:
case nil
α : Type u_1
l₂ : List (Lists α)
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂

Tactic:
exact Subset.nil

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂

Tactic:
induction l₁ with
| nil => exact Subset.nil
| cons _ _ l₁_ih =>
  refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
  simp only [List.cons_subset] at h; simp [h]

Result:
no goals

Proof state:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ ofList (head✝ :: tail✝) ⊆ ofList l₂

Tactic:
refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))

Result:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem isEquivalent_of_tendsto_one (hz : ∀ᶠ x in l, v x = 0 → u x = 0)
    (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
huv : Tendsto (u / v) l (𝓝 1)
⊢ u ~[l] v

Tactic:
rw [isEquivalent_iff_exists_eq_mul]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
huv : Tendsto (u / v) l (𝓝 1)
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
huv : Tendsto (u / v) l (𝓝 1)
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
exact ⟨u / v, huv, hz.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_iff_of_monotone
    (h₁ : ∀ a, Monotone (op a)) (h₂ : ∀ a, Monotone (Function.swap op a)) :
    Principal op o ↔ ∀ a < o, op a a < o

Proof state:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ Principal op o ↔ ∀ a < o, op a a < o

Tactic:
use fun h a ha => h ha ha

Result:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ (∀ a < o, op a a < o) → Principal op o

Proof state:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o

Tactic:
obtain hab | hba := le_or_lt a b

Result:
case mpr.inl
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Proof state:
case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
exact (h₁ a hba.le).trans_lt <| H a ha

Result:
no goals

Proof state:
case mpr.inl
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

Tactic:
exact (h₂ b hab).trans_lt <| H b hb

Result:
no goals

Proof state:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ (∀ a < o, op a a < o) → Principal op o

Tactic:
intro H a b ha hb

Result:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o
-- Mathlib/RingTheory/Polynomial/GaussLemma.lean
theorem IsPrimitive.irreducible_iff_irreducible_map_fraction_map {p : R[X]} (hp : p.IsPrimitive) :
    Irreducible p ↔ Irreducible (p.map (algebraMap R K))

Proof state:
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ∈ R⁰
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero] at c0 d0

Result:
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
⊢ IsUnit a ∨ IsUnit b

Proof state:
case intro.mk.intro.mk.intro.inl.h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (C ↑u * (integerNormalization R⁰ b).primPart)
⊢ IsUnit b

Tactic:
apply
  isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2
    (isUnit_of_mul_isUnit_right h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Basic.lean
theorem Cache.get?_bounds {decls : Array (Decl α)} {idx : Nat} (c : Cache α decls) (decl : Decl α)
    (hfound : c.val[decl]? = some idx) :
    idx < decls.size

Proof state:
case mk.push_cache.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
decl : Decl α
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
ih : ⟨cache✝, wf⟩.val[decl]? = some idx → idx < decls✝.size
h : decl' = decl
hfound : some decls✝.size = some idx
⊢ idx < (decls✝.push decl').size

Tactic:
subst h

Result:
case mk.push_cache.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
decls : Array (Decl α)
idx : Nat
cache : HashMap (Decl α) Nat
decls✝ : Array (Decl α)
cache✝ : HashMap (Decl α) Nat
decl' : Decl α
wf : WF decls✝ cache✝
hfound : some decls✝.size = some idx
ih : ⟨cache✝, wf⟩.val[decl']? = some idx → idx < decls✝.size
⊢ idx < (decls✝.push decl').size
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem affineSpan_eq_top_of_toMatrix_left_inv [Finite ι] [Fintype ι'] [DecidableEq ι]
    [Nontrivial k] (p : ι' → P) {A : Matrix ι ι' k} (hA : A * b.toMatrix p = 1) :
    affineSpan k (range p) = ⊤

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
this : ∀ (i : ι), b i ∈ affineSpan k (range p)
⊢ range ⇑b ⊆ ↑(affineSpan k (range p))

Tactic:
rintro q ⟨i, rfl⟩

Result:
case intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
this : ∀ (i : ι), b i ∈ affineSpan k (range p)
i : ι
⊢ b i ∈ ↑(affineSpan k (range p))
-- Mathlib/Logic/Basic.lean
theorem dite_mem {a : p → α} {b : ¬p → α} {s : β} :
    (if h : p then a h else b h) ∈ s ↔ (∀ h, a h ∈ s) ∧ (∀ h, b h ∈ s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
by_cases h : p <;> simp [h]

Result:
no goals