harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem order_pow {Γ} [LinearOrderedCancelAddCommMonoid Γ] [Semiring R] [NoZeroDivisors R]
    (x : HahnSeries Γ R) (n : ℕ) : (x ^ n).order = n • x.order

Proof state:
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
n : ℕ
⊢ (x ^ n).order = n • x.order

Tactic:
induction' n with h IH

Result:
case zero
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
⊢ (x ^ 0).order = 0 • x.order

case succ
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : (x ^ h).order = h • x.order
⊢ (x ^ (h + 1)).order = (h + 1) • x.order

Proof state:
case succ
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : (x ^ h).order = h • x.order
⊢ (x ^ (h + 1)).order = (h + 1) • x.order

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case succ.inl
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
h : ℕ
IH : (0 ^ h).order = h • order 0
⊢ (0 ^ (h + 1)).order = (h + 1) • order 0

case succ.inr
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : (x ^ h).order = h • x.order
hx : x ≠ 0
⊢ (x ^ (h + 1)).order = (h + 1) • x.order

Proof state:
case zero
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
⊢ (x ^ 0).order = 0 • x.order

Tactic:
simp

Result:
no goals

Proof state:
case succ.inr
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : (x ^ h).order = h • x.order
hx : x ≠ 0
⊢ (x ^ (h + 1)).order = (h + 1) • x.order

Tactic:
rw [pow_succ, order_mul (pow_ne_zero _ hx) hx, succ_nsmul, IH]

Result:
no goals

Proof state:
case succ.inl
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
h : ℕ
IH : (0 ^ h).order = h • order 0
⊢ (0 ^ (h + 1)).order = (h + 1) • order 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem natCast {f : ArithmeticFunction ℕ} [Semiring R] (h : f.IsMultiplicative) :
    IsMultiplicative (f : ArithmeticFunction R) :=
                                 -- Porting note: was `by simp [cop, h]`
  ⟨by simp [h], fun {m n} cop => by simp [h.2 cop]⟩

Proof state:
R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ↑f (m * n) = ↑f m * ↑f n

Tactic:
simp [h.2 cop]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_of_subset_range (f : α → β) (s : Set β) (h : s ⊆ range f) :
    #s ≤ #(f ⁻¹' s)

Proof state:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ #↑(f ⁻¹' s)

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]

Result:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)

Proof state:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)

Tactic:
exact mk_preimage_of_subset_range_lift f s h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem mapₗ_mk_apply_of_aemeasurable {f : α → β} (hf : AEMeasurable f μ) :
    mapₗ (hf.mk f) μ = map f μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = map f μ

Tactic:
simp [map, hf]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
lemma bitwise_zero : bitwise f 0 0 = 0

Proof state:
f : Bool → Bool → Bool
⊢ bitwise f 0 0 = 0

Tactic:
simp only [bitwise_zero_right, ite_self]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
private lemma LFunction_changeLevel_aux {M N : ℕ} [NeZero M] [NeZero N] (hMN : M ∣ N)
    (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : s ≠ 1) :
    LFunction (changeLevel hMN χ) s =
      LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))

Proof state:
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
refine AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (𝕜 := ℂ)
  (g := fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))) ?_ ?_ hpc hne ?_ hs

Result:
case refine_1
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ AnalyticOnNhd ℂ (LFunction ((changeLevel hMN) χ)) {1}ᶜ

case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ AnalyticOnNhd ℂ (fun s => LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) {1}ᶜ

case refine_3
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ LFunction ((changeLevel hMN) χ) =ᶠ[𝓝 2] fun s => LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
-- Mathlib/Data/ENNReal/Holder.lean
lemma sub_one_mul_inv (hp : p ≠ ⊤) : (p - 1) * p⁻¹ = q⁻¹

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ p ≠ ⊤

Tactic:
aesop

Result:
no goals

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ 1 - 1 * p⁻¹ = q⁻¹

Tactic:
simp [one_sub_inv p q]

Result:
no goals

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ 0 < 1 → 1 < p → p⁻¹ ≠ ⊤

Tactic:
aesop

Result:
no goals

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ (p - 1) * p⁻¹ = q⁻¹

Tactic:
rw [ENNReal.sub_mul (by aesop), ENNReal.mul_inv_cancel this (by aesop)]

Result:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ 1 - 1 * p⁻¹ = q⁻¹

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
⊢ (p - 1) * p⁻¹ = q⁻¹

Tactic:
have := pos p q |>.ne'

Result:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ⊤
this : p ≠ 0
⊢ (p - 1) * p⁻¹ = q⁻¹
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_monomial [DecidableEq R] (i : ℕ) (r : R) :
    natDegree (monomial i r) = if r = 0 then 0 else i

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).natDegree = 0

Tactic:
simp [hr]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i

Tactic:
rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
⊢ ((monomial i) r).natDegree = if r = 0 then 0 else i

Tactic:
split_ifs with hr

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).natDegree = 0

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : k == k') :
    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKeyD (insertManyIfNewUnit m l) k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' fallback : α
k_beq : (k == k') = true
⊢ ¬k ∈ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKeyD k' fallback = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' fallback : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKeyD k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' fallback : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem nat_mul (h : LiouvilleWith p x) (hn : n ≠ 0) : LiouvilleWith p (n * x)

Proof state:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)

Tactic:
exact h.mul_nat hn

Result:
no goals

Proof state:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x)

Tactic:
rw [mul_comm]

Result:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_append {K : Vector α n} {L : Vector α m} {f : (i : Nat) → α → (h : i < n + m) → β} :
    (K ++ L).mapFinIdx f =
      K.mapFinIdx (fun i a h => f i a (by omega)) ++
        L.mapFinIdx (fun i a h => f (i + n) a (by omega))

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
K L : Array α
f : (i : Nat) → α → i < K.size + L.size → β
⊢ ({ toArray := K, size_toArray := ⋯ } ++ { toArray := L, size_toArray := ⋯ }).mapFinIdx f =
    ({ toArray := K, size_toArray := ⋯ }.mapFinIdx fun i a h => f i a ⋯) ++
      { toArray := L, size_toArray := ⋯ }.mapFinIdx fun i a h => f (i + K.size) a ⋯

Tactic:
simp [Array.mapFinIdx_append]

Result:
no goals

Proof state:
α : Type ?u.18044
n m : Nat
β : Type ?u.18338
K : Vector α n
L : Vector α m
f : (i : Nat) → α → i < n + m → β
i : Nat
a : α
h : i < m
⊢ i + n < n + m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
β : Type u_2
K : Vector α n
L : Vector α m
f : (i : Nat) → α → i < n + m → β
⊢ (K ++ L).mapFinIdx f = (K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + n) a ⋯

Tactic:
rcases K with ⟨K, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
β : Type u_2
L : Vector α m
K : Array α
f : (i : Nat) → α → i < K.size + m → β
⊢ ({ toArray := K, size_toArray := ⋯ } ++ L).mapFinIdx f =
    ({ toArray := K, size_toArray := ⋯ }.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.size) a ⋯

Proof state:
α : Type ?u.18044
n m : Nat
β : Type ?u.18338
K : Vector α n
L : Vector α m
f : (i : Nat) → α → i < n + m → β
i : Nat
a : α
h : i < n
⊢ i < n + m

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
m : Nat
β : Type u_2
L : Vector α m
K : Array α
f : (i : Nat) → α → i < K.size + m → β
⊢ ({ toArray := K, size_toArray := ⋯ } ++ L).mapFinIdx f =
    ({ toArray := K, size_toArray := ⋯ }.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.size) a ⋯

Tactic:
rcases L with ⟨L, rfl⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
K L : Array α
f : (i : Nat) → α → i < K.size + L.size → β
⊢ ({ toArray := K, size_toArray := ⋯ } ++ { toArray := L, size_toArray := ⋯ }).mapFinIdx f =
    ({ toArray := K, size_toArray := ⋯ }.mapFinIdx fun i a h => f i a ⋯) ++
      { toArray := L, size_toArray := ⋯ }.mapFinIdx fun i a h => f (i + K.size) a ⋯
-- Mathlib/Data/Finsupp/Single.lean
theorem eq_single_iff {f : α →₀ M} {a b} : f = single a b ↔ f.support ⊆ {a} ∧ f a = b

Proof state:
case intro.h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ f x = (single a (f a)) x

Tactic:
by_cases hx : a = x <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ f x = 0

Proof state:
case intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a (f a)

Tactic:
ext x

Result:
case intro.h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ f x = (single a (f a)) x

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ f = single a b ↔ f.support ⊆ {a} ∧ f a = b

Tactic:
refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ f.support ⊆ {a} ∧ f a = b → f = single a b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ f.support ⊆ {a} ∧ f a = b → f = single a b

Tactic:
rintro ⟨h, rfl⟩

Result:
case intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a (f a)

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ f x = 0

Tactic:
exact not_mem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx)).symm) hx)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
    xs.findIdx p < xs.length

Proof state:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (∃ x, x ∈ xs ∧ p x = true) → findIdx p xs < xs.length
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true
h✝ : p x = true
⊢ findIdx p (x :: xs) < (x :: xs).length

Tactic:
simp_all only [forall_exists_index, and_imp, mem_cons, exists_eq_or_imp, true_or,
  findIdx_cons, cond_true, length_cons]

Result:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h✝ : p x = true
⊢ 0 < xs.length + 1

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h : ∃ a, a ∈ xs ∧ p a = true
h✝ : p x = false
⊢ findIdx p xs < xs.length

Tactic:
obtain ⟨x', m', h'⟩ := h

Result:
case neg.intro.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h✝ : p x = false
x' : α
m' : x' ∈ xs
h' : p x' = true
⊢ findIdx p xs < xs.length

Proof state:
case neg.intro.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h✝ : p x = false
x' : α
m' : x' ∈ xs
h' : p x' = true
⊢ findIdx p xs < xs.length

Tactic:
exact ih x' m' h'

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (∃ x, x ∈ xs ∧ p x = true) → findIdx p xs < xs.length
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true
h✝ : ¬p x = true
⊢ findIdx p (x :: xs) < (x :: xs).length

Tactic:
simp_all [findIdx_cons, Nat.succ_lt_succ_iff]

Result:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h : ∃ a, a ∈ xs ∧ p a = true
h✝ : p x = false
⊢ findIdx p xs < xs.length

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (∃ x, x ∈ xs ∧ p x = true) → findIdx p xs < xs.length
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true
⊢ findIdx p (x :: xs) < (x :: xs).length

Tactic:
by_cases p x

Result:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (∃ x, x ∈ xs ∧ p x = true) → findIdx p xs < xs.length
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true
h✝ : p x = true
⊢ findIdx p (x :: xs) < (x :: xs).length

case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (∃ x, x ∈ xs ∧ p x = true) → findIdx p xs < xs.length
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true
h✝ : ¬p x = true
⊢ findIdx p (x :: xs) < (x :: xs).length

Proof state:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ (x : α), x ∈ xs → p x = true → findIdx p xs < xs.length
h✝ : p x = true
⊢ 0 < xs.length + 1

Tactic:
apply Nat.succ_pos

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
h : ∃ x, x ∈ [] ∧ p x = true
⊢ findIdx p [] < [].length

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma List.iSup_mem_map_of_exists_sSup_empty_le {l : List ι} (f : ι → α)
    (h : ∃ x ∈ l, sSup ∅ ≤ f x) :
    ⨆ x ∈ l, f x ∈ l.map f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ⨆ x ∈ l, f x ∈ map f l

Tactic:
simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ⨆ x ∈ l, f x ∈ map f l

Tactic:
classical
simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem forM_toArray' [Monad m] (l : List α) (f : α → m PUnit) (h : stop = l.toArray.size) :
    (l.toArray.forM f 0 stop) = l.forM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ foldlM (fun x => f) PUnit.unit l.toArray = l.forM f

Tactic:
simp only [size_toArray, foldlM_toArray']

Result:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ List.foldlM (fun x => f) PUnit.unit l = l.forM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
stop : Nat
inst✝ : Monad m
l : List α
f : α → m PUnit
h : stop = l.toArray.size
⊢ Array.forM f l.toArray 0 stop = l.forM f

Tactic:
subst h

Result:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ Array.forM f l.toArray = l.forM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ List.foldlM (fun x => f) PUnit.unit l = l.forM f

Tactic:
induction l <;> simp_all

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ Array.forM f l.toArray = l.forM f

Tactic:
rw [Array.forM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
l : List α
f : α → m PUnit
⊢ foldlM (fun x => f) PUnit.unit l.toArray = l.forM f
-- Mathlib/RingTheory/Ideal/Defs.lean
theorem mul_sub_mul_mem [I.IsTwoSided]
    (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I

Proof state:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I

Tactic:
rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]

Result:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I

Proof state:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I

Tactic:
exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)

Tactic:
rw [sub_mul, mul_sub]

Result:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)

Proof state:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)

Tactic:
abel

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See also `le_inv_of_le_inv₀` for a one-sided implication with one fewer assumption. -/
lemma le_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 < a
hb : 0 < b
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem square_to_iso_invert (i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ Arrow.mk p.hom) :
    i.hom ≫ sq.right ≫ p.inv = sq.left

Proof state:
T : Type u
inst✝ : Category.{v, u} T
i : Arrow T
X Y : T
p : X ≅ Y
sq : i ⟶ mk p.hom
⊢ i.hom ≫ sq.right ≫ p.inv = sq.left

Tactic:
simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem iSup_edist_ne_top_aux {ι : Type*} [Finite ι] {α : ι → Type*}
    [∀ i, PseudoMetricSpace (α i)] (f g : PiLp ∞ α) : (⨆ i, edist (f i) (g i)) ≠ ⊤

Proof state:
case intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
⊢ ⨆ i, edist (f i) (g i) ≠ ⊤

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)

Result:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
⊢ ⨆ i, edist (f i) (g i) ≠ ⊤

Proof state:
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
⊢ ⨆ i, edist (f i) (g i) ≠ ⊤

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
⊢ ⨆ i, edist (f i) (g i) ≠ ⊤

Proof state:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
⊢ ⨆ i, edist (f i) (g i) ≠ ⊤

Tactic:
refine ne_of_lt ((iSup_le fun i => ?_).trans_lt (@ENNReal.coe_lt_top M))

Result:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
i : ι
⊢ edist (f i) (g i) ≤ ↑M

Proof state:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
i : ι
⊢ ↑⟨dist (f i) (g i), ⋯⟩ ≤ ↑M

Tactic:
exact mod_cast hM i

Result:
no goals

Proof state:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
i : ι
⊢ edist (f i) (g i) ≤ ↑M

Tactic:
simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]

Result:
case intro.intro
ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M
i : ι
⊢ ↑⟨dist (f i) (g i), ⋯⟩ ≤ ↑M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
   findSome? f (mkArray n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
x✝ : (f a).isSome = true
⊢ findSome? f (mkArray n a) = if n = 0 then none else f a

Tactic:
simp [findSome?_mkArray]

Result:
no goals