harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem lift_comp_ι : (lift R A maps) ∘ₐ (ι R A i) = maps

Proof state:
case H
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
a : A i
⊢ (((lift R A) fun {i} => maps) ∘ₐ ι R A i) a = maps a

Tactic:
simp [lift_apply, ι]

Result:
no goals

Proof state:
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ((lift R A) fun {i} => maps) ∘ₐ ι R A i = maps

Tactic:
ext a

Result:
case H
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
a : A i
⊢ (((lift R A) fun {i} => maps) ∘ₐ ι R A i) a = maps a
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFoldr_cons (s : Multiset α) (a : α) (h h') (b : β) :
    noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Proof state:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
β : Type u_4
f : α → β → β
a : α
b : β
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
⊢ noncommFoldr f (a ::ₘ ⟦a✝⟧) h b = f a (noncommFoldr f ⟦a✝⟧ h' b)

Proof state:
case h
α : Type u_3
β : Type u_4
f : α → β → β
a : α
b : β
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
⊢ noncommFoldr f (a ::ₘ ⟦a✝⟧) h b = f a (noncommFoldr f ⟦a✝⟧ h' b)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem extend_apply' (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ a, f a = b) :
    extend f g e' b = e' b

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b

Tactic:
simp [Function.extend_def, hb]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem perm_insertionSort : ∀ l : List α, insertionSort r l ~ l
  | [] => Perm.nil
  | b :: l => by
    simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
b : α
l : List α
⊢ insertionSort r (b :: l) ~ b :: l

Tactic:
simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eraseIdx!_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) :
    (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx i) (by simp [h, hi])

Proof state:
α : Type ?u.7478
n : Nat
a : Array α
h : a.size = n
i : Nat
hi : i < n
⊢ (a.eraseIdx i ⋯).size = n - 1

Tactic:
simp [h, hi]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Array α
h : a.size = n
i : Nat
hi : i < n
⊢ { toArray := a, size_toArray := h }.eraseIdx! i = { toArray := a.eraseIdx i ⋯, size_toArray := ⋯ }

Tactic:
simp [Vector.eraseIdx!, hi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (ofList l).getD k' fallback = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.getD_insertMany_empty_list_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr₂_left_left (f₁ : γ → α → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd xs s₁)
    = let m := mapAccumr₂ (fun x y (s₁, s₂) =>
                let r₂ := f₂ x y s₂
                let r₁ := f₁ r₂.snd x s₁
                ((r₁.fst, r₂.fst), r₁.snd)
              )
            xs ys (s₁, s₂)
    (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_denom_neg (x : RatFunc K) : (-x).num * x.denom = -x.num * (-x).denom

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ (-x).num * x.denom = -x.num * (-x).denom

Tactic:
rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), _root_.map_neg, neg_div, num_div_denom]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_one_sub_nth_order (n : ℕ) :
    ∀ᶠ t in 𝓝 0, inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
  Metric.eventually_nhds_iff.2 ⟨1, one_pos, fun t ht ↦ inverse_one_sub_nth_order' n <| by
    rwa [← dist_zero_right]⟩

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : dist t 0 < 1
⊢ ‖t‖ < 1

Tactic:
rwa [← dist_zero_right]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem pmap_prev_eq_rotate_length_sub_one (h : Nodup l) :
    (l.pmap l.prev fun _ h => h) = l.rotate (l.length - 1)

Proof state:
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.prev l ⋯).length = (l.rotate (l.length - 1)).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.prev l ⋯).length) (h₂ : i < (l.rotate (l.length - 1)).length),
    (pmap l.prev l ⋯)[i] = (l.rotate (l.length - 1))[i]

Tactic:
intro n hn hn'

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]

Tactic:
rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.prev l ⋯ = l.rotate (l.length - 1)

Tactic:
apply List.ext_getElem

Result:
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.prev l ⋯).length = (l.rotate (l.length - 1)).length

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.prev l ⋯).length) (h₂ : i < (l.rotate (l.length - 1)).length),
    (pmap l.prev l ⋯)[i] = (l.rotate (l.length - 1))[i]
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformLeft.fst_mul_snd_subset :
    (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2

Tactic:
refine inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Tactic:
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem zero_scaleRoots (s : R) : scaleRoots 0 s = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
s : R
⊢ scaleRoots 0 s = 0

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
s : R
n✝ : ℕ
⊢ (scaleRoots 0 s).coeff n✝ = coeff 0 n✝

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
s : R
n✝ : ℕ
⊢ (scaleRoots 0 s).coeff n✝ = coeff 0 n✝

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_densityProcess_fst_atTop_ae_of_monotone (κ : Kernel α (γ × β)) [IsFiniteKernel κ]
    (n : ℕ) (a : α) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = univ) :
    ∀ᵐ x ∂(fst κ a), Tendsto (fun m ↦ densityProcess κ (fst κ) n a x (seq m)) atTop (𝓝 1)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)

Tactic:
rw [← hx]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
exact tendsto_densityProcess_fst_atTop_univ_of_monotone κ n a x seq hseq hseq_iUnion

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)

Tactic:
filter_upwards [densityProcess_fst_univ_ae κ n a] with x hx

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_eq_iSup_finset (s : ι → α) : ⨆ i, s i = ⨆ t : Finset ι, ⨆ i ∈ t, s i

Proof state:
case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i

Tactic:
exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i

Tactic:
exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i

case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i
-- Mathlib/Data/ENNReal/Inv.lean
theorem add_halves (a : ℝ≥0∞) : a / 2 + a / 2 = a

Proof state:
a : ℝ≥0∞
⊢ a / 2 + a / 2 = a

Tactic:
rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem upperClosure_singleton (a : α) : upperClosure ({a} : Set α) = UpperSet.Ici a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ upperClosure {a} = UpperSet.Ici a

Tactic:
ext

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(upperClosure {a}) ↔ x✝ ∈ ↑(UpperSet.Ici a)

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(upperClosure {a}) ↔ x✝ ∈ ↑(UpperSet.Ici a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem innerDualCone_sUnion (S : Set (Set H)) :
    (⋃₀ S).innerDualCone = sInf (Set.innerDualCone '' S)

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
S : Set (Set H)
⊢ (⋃₀ S).innerDualCone = sInf (innerDualCone '' S)

Tactic:
simp_rw [sInf_image, sUnion_eq_biUnion, innerDualCone_iUnion]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_neg (P : Fin 3 → A) :
    (W'.baseChange B).toProjective.neg (f ∘ P) = f ∘ (W'.baseChange A).toProjective.neg P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.neg (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toProjective.neg P

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eraseLead : #f.eraseLead.support = #f.support - 1

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
rw [hf, eraseLead_zero, support_zero, card_empty]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
by_cases hf : f = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ #f.eraseLead.support = #f.support - 1

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.support - 1
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_naturality_middle (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom = (α_ X Y Z).hom ≫ X ◁ f ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom = (α_ X Y Z).hom ≫ X ◁ f ▷ Z

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem _root_.BoxIntegral.Prepartition.distortion_biUnionTagged (π : Prepartition I)
    (πi : ∀ J, TaggedPrepartition J) :
    (π.biUnionTagged πi).distortion = π.boxes.sup fun J => (πi J).distortion

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
exact sup_biUnion _ _

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderiv_const (c : F) : (fderiv 𝕜 fun _ : E => c) = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
⊢ (fderiv 𝕜 fun x => c) = 0

Tactic:
rw [← fderivWithin_univ, fderivWithin_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_singleton (l : Array α) : #[l].flatten = l

Proof state:
α : Type u_1
l : Array α
⊢ #[] = #[]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : Array α
⊢ #[l].flatten = l

Tactic:
simp [flatten]

Result:
α : Type u_1
l : Array α
⊢ #[] = #[]
-- Mathlib/Data/Finset/Basic.lean
theorem erase_injOn' (a : α) : { s : Finset α | a ∈ s }.InjOn fun s => erase s a :=
  fun s hs t ht (h : s.erase a = _) => by rw [← insert_erase hs, ← insert_erase ht, h]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s => s.erase a) t
⊢ s = t

Tactic:
rw [← insert_erase hs, ← insert_erase ht, h]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem sqrt_normSq_eq_norm {z : K} : √(normSq z) = ‖z‖

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ √(normSq z) = ‖z‖

Tactic:
rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem toPrincipalIdeal_eq_iff {I : (FractionalIdeal R⁰ K)ˣ} {x : Kˣ} :
    toPrincipalIdeal R K x = I ↔ spanSingleton R⁰ (x : K) = I

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ (toPrincipalIdeal R K) x = I ↔ spanSingleton R⁰ ↑x = ↑I

Tactic:
simp only [toPrincipalIdeal]

Result:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ { toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
          map_one' := ⋯, map_mul' := ⋯ }
        x =
      I ↔
    spanSingleton R⁰ ↑x = ↑I

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ { toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
          map_one' := ⋯, map_mul' := ⋯ }
        x =
      I ↔
    spanSingleton R⁰ ↑x = ↑I

Tactic:
exact Units.ext_iff

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean
@[to_additive]
lemma prod_preimage (f : ι → κ) (s : Finset κ) (hf) (g : κ → β)
    (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) :
    ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Tactic:
rw [prod_preimage', prod_filter_of_ne]

Result:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝ : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f

Tactic:
exact fun x hx ↦ Not.imp_symm (hg x hx)

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic_source (hv : ‖v‖ = 1) : (stereographic hv).source = {⟨v, by simp [hv]⟩}ᶜ :=
  rfl

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ v ∈ sphere 0 1

Tactic:
simp [hv]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem chartedSpaceSelf_prod : prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')

Proof state:
case chartAt.h
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
x✝ : H × H'
⊢ ChartedSpace.chartAt x✝ = ChartedSpace.chartAt x✝

Tactic:
simp only [prodChartedSpace_chartAt, chartAt_self_eq, refl_prod_refl]

Result:
case chartAt.h
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
x✝ : H × H'
⊢ PartialHomeomorph.refl (H × H') = PartialHomeomorph.refl (ModelProd H H')

Proof state:
case chartAt.h
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
x✝ : H × H'
⊢ PartialHomeomorph.refl (H × H') = PartialHomeomorph.refl (ModelProd H H')

Tactic:
rfl

Result:
no goals

Proof state:
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
⊢ prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')

Tactic:
ext1

Result:
case atlas
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
⊢ ChartedSpace.atlas = ChartedSpace.atlas

case chartAt
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
⊢ ChartedSpace.chartAt = ChartedSpace.chartAt

Proof state:
case atlas
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
⊢ ChartedSpace.atlas = ChartedSpace.atlas

Tactic:
simp [prodChartedSpace, atlas, ChartedSpace.atlas]

Result:
no goals

Proof state:
case chartAt
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
⊢ ChartedSpace.chartAt = ChartedSpace.chartAt

Tactic:
ext1

Result:
case chartAt.h
H : Type u
H' : Type u_1
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
x✝ : H × H'
⊢ ChartedSpace.chartAt x✝ = ChartedSpace.chartAt x✝
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mulLECancellable_one [Monoid α] [LE α] : MulLECancellable (1 : α) := fun a b => by
  simpa only [one_mul] using id

Proof state:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b

Tactic:
simpa only [one_mul] using id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/LemmasAux.lean
theorem toNat_sub_max_self (a : Int) : (a - max a 0).toNat = 0

Proof state:
a : Int
⊢ (match a - max a 0 with
    | ofNat n => n
    | -[a+1] => 0) =
    0

Tactic:
split <;> simp_all <;> omega

Result:
no goals

Proof state:
a : Int
⊢ (a - max a 0).toNat = 0

Tactic:
simp [toNat]

Result:
a : Int
⊢ (match a - max a 0 with
    | ofNat n => n
    | -[a+1] => 0) =
    0