harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem set_getElem_succ_eraseIdx_succ
    {l : Array α} {i : Nat} (h : i + 1 < l.size) :
    (l.eraseIdx (i + 1)).set i l[i + 1] (by simp; omega) = l.eraseIdx i

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h : i + 1 < { toList := l }.size
⊢ ({ toList := l }.eraseIdx (i + 1) h).set i { toList := l }[i + 1] ⋯ = { toList := l }.eraseIdx i ⋯

Tactic:
simp [List.set_getElem_succ_eraseIdx_succ, *]

Result:
no goals

Proof state:
α : Type ?u.77844
l : Array α
i : Nat
h : i + 1 < l.size
⊢ i < l.size - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.77844
l : Array α
i : Nat
h : i + 1 < l.size
⊢ i < (l.eraseIdx (i + 1) h).size

Tactic:
simp

Result:
α : Type ?u.77844
l : Array α
i : Nat
h : i + 1 < l.size
⊢ i < l.size - 1

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i + 1 < l.size
⊢ (l.eraseIdx (i + 1) h).set i l[i + 1] ⋯ = l.eraseIdx i ⋯

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i : Nat
l : List α
h : i + 1 < { toList := l }.size
⊢ ({ toList := l }.eraseIdx (i + 1) h).set i { toList := l }[i + 1] ⋯ = { toList := l }.eraseIdx i ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_mkArray_empty : (mkArray n (#[] : Array α)).flatten = #[]

Proof state:
n : Nat
α : Type u_1
⊢ (mkArray n #[]).flatten.toList = #[].toList

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α : Type u_1
⊢ (mkArray n #[]).flatten = #[]

Tactic:
rw [← toList_inj]

Result:
n : Nat
α : Type u_1
⊢ (mkArray n #[]).flatten.toList = #[].toList
-- Mathlib/Topology/PartitionOfUnity.lean
theorem sum_finsupport_smul_eq_finsum {M : Type*} [AddCommGroup M] [Module ℝ M] (φ : ι → X → M) :
    ∑ i ∈ ρ.finsupport x₀, ρ i x₀ • φ i x₀ = ∑ᶠ i, ρ i x₀ • φ i x₀

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀
⊢ ((support fun i => (ρ i) x₀) ∩ support fun i => φ i x₀) ⊆ support fun i => (ρ i) x₀

Tactic:
exact inter_subset_left

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
⊢ (support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)

Tactic:
have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
  funext fun _ => (Pi.smul_apply' _ _ _).symm

Result:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀
⊢ (support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀

Tactic:
apply (finsum_eq_sum_of_support_subset _ _).symm

Result:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
⊢ (support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀
⊢ (support fun i => (ρ i) x₀ • φ i x₀) ⊆ ↑(ρ.finsupport x₀)

Tactic:
rw [ρ.coe_finsupport x₀, this, support_smul]

Result:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module ℝ M
φ : ι → X → M
this : (fun i => (ρ i) x₀ • φ i x₀) = (fun i => (ρ i) x₀) • fun i => φ i x₀
⊢ ((support fun i => (ρ i) x₀) ∩ support fun i => φ i x₀) ⊆ support fun i => (ρ i) x₀
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem smul_left' (f g : α →₂[μ] E) (r : 𝕜) : ⟪r • f, g⟫ = conj r * inner f g

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
⊢ inner (r • f) g = (starRingEnd 𝕜) r * inner f g

Tactic:
rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
⊢ ∫ (a : α), inner (↑↑(r • f) a) (↑↑g a) ∂μ = ∫ (a : α), (starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a) ∂μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ inner (↑↑(r • f) x) (↑↑g x) = (starRingEnd 𝕜) r • inner (↑↑f x) (↑↑g x)

Tactic:
rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ (fun a => inner (↑↑(r • f) a) (↑↑g a)) x = (fun a => (starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a)) x

Tactic:
simp only

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ inner (↑↑(r • f) x) (↑↑g x) = (starRingEnd 𝕜) r • inner (↑↑f x) (↑↑g x)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
⊢ ∫ (a : α), inner (↑↑(r • f) a) (↑↑g a) ∂μ = ∫ (a : α), (starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a) ∂μ

Tactic:
refine integral_congr_ae ((coeFn_smul r f).mono fun x hx => ?_)

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ (fun a => inner (↑↑(r • f) a) (↑↑g a)) x = (fun a => (starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a)) x
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_prod_list_swap {l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) :
    sign l.prod = (-1) ^ l.length

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ sign l.prod = (-1) ^ l.length

Tactic:
have h₁ : l.map sign = List.replicate l.length (-1) :=
  List.eq_replicate_iff.2
    ⟨by simp, fun u hu =>
      let ⟨g, hg⟩ := List.mem_map.1 hu
      hg.2 ▸ (hl _ hg.1).sign_eq⟩

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
h₁ : List.map (⇑sign) l = List.replicate l.length (-1)
⊢ sign l.prod = (-1) ^ l.length

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ (List.map (⇑sign) l).length = l.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
h₁ : List.map (⇑sign) l = List.replicate l.length (-1)
⊢ sign l.prod = (-1) ^ l.length

Tactic:
rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem ofZNum_toNat : ∀ n : ZNum, (ofZNum n : ℕ) = Int.toNat n
  | 0 => rfl
  | ZNum.pos p => show _ = Int.toNat p by rw [← PosNum.to_nat_to_int p]; rfl
  | ZNum.neg p =>
    (congr_arg fun x => Int.toNat (-x)) <|
      show ((p.pred' + 1 : ℕ) : ℤ) = p by rw [← succ'_to_nat]; simp

Proof state:
p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑p).toNat

Tactic:
rw [← PosNum.to_nat_to_int p]

Result:
p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑↑p).toNat

Proof state:
p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p

Tactic:
simp

Result:
no goals

Proof state:
p : PosNum
⊢ ↑(↑p.pred' + 1) = ↑p

Tactic:
rw [← succ'_to_nat]

Result:
p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p

Proof state:
p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑↑p).toNat

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_ofFn (f : Fin n → α) : (Vector.ofFn f).toList = List.ofFn f

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_map_coe (l : List α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ pmap (fun a h => f ⟨a, h⟩.val) l ⋯ = map f l

Tactic:
exact pmap_eq_map _ _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun i => f i.val) l.attach = map f l

Tactic:
rw [attach, attachWith, map_pmap]

Result:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ pmap (fun a h => f ⟨a, h⟩.val) l ⋯ = map f l
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma right_mul_prod_Ico (h : a ≤ b) : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ico h, prod_cons]

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem nodup_ofFn {n} {f : Fin n → α} : Nodup (ofFn f) ↔ Function.Injective f

Proof state:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Tactic:
intro h

Result:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ Function.Injective (Fin.cons x₀ xs)

Proof state:
case refine_1
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn Fin.elim0).Nodup → Function.Injective Fin.elim0

Tactic:
intro _

Result:
case refine_1
α : Type u
n : ℕ
f : Fin n → α
a✝ : (ofFn Fin.elim0).Nodup
⊢ Function.Injective Fin.elim0

Proof state:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ Function.Injective (Fin.cons x₀ xs)

Tactic:
rw [Fin.cons_injective_iff]

Result:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ x₀ ∉ Set.range xs ∧ Function.Injective xs

Proof state:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ x₀ ∉ Set.range xs ∧ Function.Injective xs

Tactic:
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h

Result:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬∃ i, xs i = x₀) ∧ (ofFn fun i => xs i).Nodup
⊢ x₀ ∉ Set.range xs ∧ Function.Injective xs

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f

Tactic:
refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f

Result:
case refine_1
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn Fin.elim0).Nodup → Function.Injective Fin.elim0

case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
refine ⟨?_, nodup_ofFn_ofInjective⟩

Result:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f

Proof state:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬∃ i, xs i = x₀) ∧ (ofFn fun i => xs i).Nodup
⊢ x₀ ∉ Set.range xs ∧ Function.Injective xs

Tactic:
exact h.imp_right ih

Result:
no goals

Proof state:
case refine_1
α : Type u
n : ℕ
f : Fin n → α
a✝ : (ofFn Fin.elim0).Nodup
⊢ Function.Injective Fin.elim0

Tactic:
exact Function.injective_of_subsingleton _

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
@[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
⊢ card (AddChar G R) ≤ card G

Tactic:
simpa only [Module.finrank_fintype_fun_eq_card] using
  (AddChar.linearIndependent G R).fintype_card_le_finrank

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.mul_right {k m n : ℕ+} : k.Coprime m → k.Coprime n → k.Coprime (m * n)

Proof state:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → k.Coprime (m * n)

Tactic:
rw [← coprime_coe]

Result:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)

Proof state:
k m n : ℕ+
⊢ k.Coprime m → k.Coprime n → k.Coprime (m * n)

Tactic:
repeat rw [← coprime_coe]

Result:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)

Proof state:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)

Tactic:
rw [mul_coe]

Result:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime (↑m * ↑n)

Proof state:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime (↑m * ↑n)

Tactic:
apply Nat.Coprime.mul_right

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem irreducible_iff_prime_iff :
    (∀ a : M, Irreducible a ↔ Prime a) ↔ ∀ a : Associates M, Irreducible a ↔ Prime a

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a

Tactic:
simp_rw [forall_associated, irreducible_mk, prime_mk]

Result:
no goals
-- Mathlib/Logic/Encodable/Lattice.lean
theorem iUnion_decode₂_cases {f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
    C (⋃ b ∈ decode₂ β n, f b) :=
  match decode₂ β n with
  | none => by
    simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]
    apply H0
  | some b => by
    convert H1 b
    simp [Set.ext_iff]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ b ∈ none, f b)

Tactic:
simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]

Result:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ C (⋃ b_1 ∈ some b, f b_1)

Tactic:
convert H1 b

Result:
case h.e'_1
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ b_1 ∈ some b, f b_1 = f b

Proof state:
case h.e'_1
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ b_1 ∈ some b, f b_1 = f b

Tactic:
simp [Set.ext_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅

Tactic:
apply H0

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem swap_mul_self_mul (i j : α) (σ : Perm α) : Equiv.swap i j * (Equiv.swap i j * σ) = σ

Proof state:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * (swap i j * σ) = σ

Tactic:
simp [← mul_assoc]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem not_mem_idealOfSet {s : Set X} {f : C(X, R)} : f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
simp_rw [mem_idealOfSet]

Result:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
push_neg

Result:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (∃ x ∈ sᶜ, f x ≠ 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (∃ x ∈ sᶜ, f x ≠ 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.balanceR {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
    (H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
    Valid' o₁ (@balanceR α l x r) o₂

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
exact hr.dual.balanceL hl.dual (balance_sz_dual H)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]

Result:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Bitwise/Lemmas.lean
theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
    m >>> n = m / ((2 ^ n) : Nat)

Proof state:
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ 0 < 2 ^ n

Tactic:
exact Nat.pow_pos (Nat.zero_lt_two)

Result:
no goals

Proof state:
case h_2
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ -[n✝ / 2 ^ n+1] = -((↑n✝).ediv ↑(2 ^ n) + 1)

Tactic:
rfl

Result:
no goals

Proof state:
m : Int
n : Nat
⊢ (match m, n with
    | ofNat n, s => ofNat (n / 2 ^ s)
    | -[n+1], s => -[n / 2 ^ s+1]) =
    m / ↑(2 ^ n)

Tactic:
split

Result:
case h_1
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ ofNat (n✝ / 2 ^ n) = ofNat n✝ / ↑(2 ^ n)

case h_2
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ -[n✝ / 2 ^ n+1] = -[n✝+1] / ↑(2 ^ n)

Proof state:
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ 0 < ↑(2 ^ n)

Tactic:
norm_cast

Result:
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ 0 < 2 ^ n

Proof state:
case h_1
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ ofNat (n✝ / 2 ^ n) = ofNat n✝ / ↑(2 ^ n)

Tactic:
simp

Result:
no goals

Proof state:
m : Int
n : Nat
⊢ m >>> n = m / ↑(2 ^ n)

Tactic:
simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]

Result:
m : Int
n : Nat
⊢ (match m, n with
    | ofNat n, s => ofNat (n / 2 ^ s)
    | -[n+1], s => -[n / 2 ^ s+1]) =
    m / ↑(2 ^ n)

Proof state:
case h_2
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ -[n✝ / 2 ^ n+1] = -[n✝+1] / ↑(2 ^ n)

Tactic:
rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]

Result:
case h_2
n : Nat
x✝¹ : Int
x✝ n✝ : Nat
⊢ -[n✝ / 2 ^ n+1] = -((↑n✝).ediv ↑(2 ^ n) + 1)
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_self_apply (j) [Decidable (i = j)] : b.repr (b i) j = if i = j then 1 else 0

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (b.repr (b i)) j = if i = j then 1 else 0

Tactic:
rw [repr_self, Finsupp.single_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_empty [Inhabited β] {a : α} {c} :
    get! (empty c : Raw₀ α (fun _ => β)) a = default

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : Inhabited β
a : α
c : Nat
⊢ get! (empty c) a = default

Tactic:
simp [get!, empty]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem comp_cons {α : Sort*} {β : Sort*} (g : α → β) (y : α) (q : Fin n → α) :
    g ∘ cons y q = cons (g y) (g ∘ q)

Proof state:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
have : j'.succ = j := succ_pred j h

Result:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Proof state:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
by_cases h : j = 0

Result:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Proof state:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
let j' := pred j h

Result:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Proof state:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

Result:
no goals

Proof state:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)

Tactic:
ext j

Result:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Proof state:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0