harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Sort.lean
theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} :
    (s.sort (· ≤ ·))[0] = s.min' (card_pos.1 <| by rwa [length_sort] at h) :=
  sorted_zero_eq_min'_aux _ _ _

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
⊢ 0 < #s

Tactic:
rwa [length_sort] at h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_one (s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s), 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem injective_of_forall_ne_isSome (f : α ≃. β) (a₂ : α)
    (h : ∀ a₁ : α, a₁ ≠ a₂ → isSome (f a₁)) : Injective f :=
  HasLeftInverse.injective
    ⟨fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id, fun x => by
      classical
        cases hfx : f x
        · have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
          simp [this]
        · dsimp only
          rw [(eq_some_iff f).2 hfx]
          rfl⟩

Proof state:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) (f x) = x

Tactic:
cases hfx : f x

Result:
case none
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) none = x

case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) (some val✝) = x

Proof state:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
⊢ ¬none.isSome = true

Tactic:
simp

Result:
no goals

Proof state:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x

Tactic:
rfl

Result:
no goals

Proof state:
case none
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
this : x = a₂
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) none = x

Tactic:
simp [this]

Result:
no goals

Proof state:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (f.symm val✝) = x

Tactic:
rw [(eq_some_iff f).2 hfx]

Result:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x

Proof state:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) (some val✝) = x

Tactic:
dsimp only

Result:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (f.symm val✝) = x

Proof state:
case none
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) none = x

Tactic:
have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)

Result:
case none
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
this : x = a₂
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id) none = x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_append_of_length_le {l : Vector α n} {k : Nat} (hk : n ≤ k) (l' : Vector α n) (h) :
    eraseIdx (l ++ l') k = (l ++ eraseIdx l' (k - n)).cast (by omega)

Proof state:
α : Type u_1
n : Nat
l : Vector α n
k : Nat
hk : n ≤ k
l' : Vector α n
h : k < n + n
⊢ (l ++ l').eraseIdx k h = Vector.cast ⋯ (l ++ l'.eraseIdx (k - n) ⋯)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
n k : Nat
hk : n ≤ k
l' : Vector α n
h : k < n + n
l : Array α
size_toArray✝ : l.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝ } ++ l').eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := size_toArray✝ } ++ l'.eraseIdx (k - n) ⋯)

Proof state:
case mk.mk
α : Type u_1
n k : Nat
hk : n ≤ k
h : k < n + n
l : Array α
size_toArray✝¹ : l.size = n
l' : Array α
size_toArray✝ : l'.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝¹ } ++ { toArray := l', size_toArray := size_toArray✝ }).eraseIdx k h =
    Vector.cast ⋯
      ({ toArray := l, size_toArray := size_toArray✝¹ } ++
        { toArray := l', size_toArray := size_toArray✝ }.eraseIdx (k - n) ⋯)

Tactic:
simp [Array.eraseIdx_append_of_length_le, *]

Result:
no goals

Proof state:
case mk
α : Type u_1
n k : Nat
hk : n ≤ k
l' : Vector α n
h : k < n + n
l : Array α
size_toArray✝ : l.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝ } ++ l').eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := size_toArray✝ } ++ l'.eraseIdx (k - n) ⋯)

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
n k : Nat
hk : n ≤ k
h : k < n + n
l : Array α
size_toArray✝¹ : l.size = n
l' : Array α
size_toArray✝ : l'.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝¹ } ++ { toArray := l', size_toArray := size_toArray✝ }).eraseIdx k h =
    Vector.cast ⋯
      ({ toArray := l, size_toArray := size_toArray✝¹ } ++
        { toArray := l', size_toArray := size_toArray✝ }.eraseIdx (k - n) ⋯)

Proof state:
α : Type ?u.24801
n : Nat
l : Vector α n
k : Nat
hk : n ≤ k
l' : Vector α n
h : k < n + n
⊢ n + (n - 1) = n + n - 1

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem smallSets_comap_eq_comap_image (l : Filter β) (f : α → β) :
    (comap f l).smallSets = comap (image f) l.smallSets

Proof state:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟

Tactic:
simp [Function.comp_def, map_bind, bind_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_

Result:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟
-- Mathlib/LinearAlgebra/RootSystem/Base.lean
@[simp]
lemma span_int_root_support :
    span ℤ (P.root '' b.support) = span ℤ (range P.root)

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
i : ι
⊢ P.root i ∈ ↑(span ℤ (⇑P.root '' b.support))

Tactic:
exact b.root_mem_span_int i

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
⊢ range ⇑P.root ⊆ ↑(span ℤ (⇑P.root '' b.support))

Tactic:
rintro - ⟨i, rfl⟩

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
i : ι
⊢ P.root i ∈ ↑(span ℤ (⇑P.root '' b.support))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
⊢ span ℤ (⇑P.root '' b.support) = span ℤ (range ⇑P.root)

Tactic:
refine le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_)

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
⊢ range ⇑P.root ⊆ ↑(span ℤ (⇑P.root '' b.support))
-- Mathlib/CategoryTheory/Yoneda.lean
theorem obj_map_id {X Y : C} (f : op X ⟶ op Y) :
    (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app (op Y) (𝟙 Y)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app (op Y) (𝟙 Y)

Tactic:
dsimp

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Proof state:
C : ℝ
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)

Tactic:
simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_zero_nat

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem DirectSum.coeLinearMap_eq_finsum [DecidableEq M]
    (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) :
    (DirectSum.coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x =
      finsum fun m => x m

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)

Tactic:
apply DirectSum.support_subset

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)

Tactic:
classical
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
apply DirectSum.support_subset

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum, DFinsupp.sum, finsum_eq_sum_of_support_subset]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)
-- Mathlib/ModelTheory/Syntax.lean
theorem castLE_rfl {n} (h : n ≤ n) (φ : L.BoundedFormula α n) : φ.castLE h = φ

Proof state:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (rel R✝ ts✝) = rel R✝ ts✝

Tactic:
simp [Fin.castLE_of_eq]

Result:
no goals

Proof state:
case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (f₁✝.imp f₂✝) = f₁✝.imp f₂✝

Tactic:
simp [Fin.castLE_of_eq, ih1, ih2]

Result:
no goals

Proof state:
case falsum
L : Language
α : Type u'
n n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum

Tactic:
rfl

Result:
no goals

Proof state:
case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (h : n✝ + 1 ≤ n✝ + 1), castLE h f✝ = f✝
h : n✝ ≤ n✝
⊢ castLE h f✝.all = f✝.all

Tactic:
simp [Fin.castLE_of_eq, ih3]

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
⊢ castLE h φ = φ

Tactic:
induction φ with
| falsum => rfl
| equal => simp [Fin.castLE_of_eq]
| rel => simp [Fin.castLE_of_eq]
| imp _ _ ih1 ih2 => simp [Fin.castLE_of_eq, ih1, ih2]
| all _ ih3 => simp [Fin.castLE_of_eq, ih3]

Result:
no goals

Proof state:
case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
simp [Fin.castLE_of_eq]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_span_singleton (r s : R) :
    span {r} * span {s} = (span {r * s} : Ideal R)

Proof state:
R : Type u
inst✝ : CommSemiring R
r s : R
⊢ Submodule.span R {r} * Submodule.span R {s} = Submodule.span R {r * s}

Tactic:
rw [Submodule.span_mul_span, Set.singleton_mul_singleton]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
r s : R
⊢ span {r} * span {s} = span {r * s}

Tactic:
unfold span

Result:
R : Type u
inst✝ : CommSemiring R
r s : R
⊢ Submodule.span R {r} * Submodule.span R {s} = Submodule.span R {r * s}
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.toFinset_eq_toFinset {s : Set α} [Fintype s] (h : s.Finite) :
    h.toFinset = s.toFinset

Proof state:
α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ h.toFinset = s.toFinset

Tactic:
have : h.fintype = ‹_› := Subsingleton.elim _ _

Result:
α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
this : h.fintype = inst✝
⊢ h.toFinset = s.toFinset

Proof state:
α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
this : h.fintype = inst✝
⊢ h.toFinset = s.toFinset

Tactic:
rw [Finite.toFinset, this]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : F.map (inv f) = inv (F.map f)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) = inv (F.map f)

Tactic:
apply eq_inv_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Proof state:
case hom_inv_id
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_iff_forall {P : α → Prop} : ∀ {t}, All P t ↔ ∀ x, Emem x t → P x
  | nil => (iff_true_intro <| by rintro _ ⟨⟩).symm
  | node _ l x r => by simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]

Proof state:
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (node size✝ l x r) ↔ ∀ (x_1 : α), Emem x_1 (node size✝ l x r) → P x_1

Tactic:
simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
⊢ ∀ (x : α), Emem x nil → P x

Tactic:
rintro _ ⟨⟩

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem inv_hom_id : inv P ≫ hom P = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
dsimp [hom, inv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((λ_ P.X).inv ≫ R.one ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) ≫
      coequalizer.desc P.actLeft ⋯ =
    𝟙 P.X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (λ_ P.X).inv ≫ R.one ▷ P.X ≫ P.actLeft = 𝟙 P.X

Tactic:
rw [one_actLeft, Iso.inv_hom_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((λ_ P.X).inv ≫ R.one ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) ≫
      coequalizer.desc P.actLeft ⋯ =
    𝟙 P.X

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (λ_ P.X).inv ≫ R.one ▷ P.X ≫ P.actLeft = 𝟙 P.X
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_add_const_uIcc : (fun x => x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
simpa only [add_comm] using preimage_const_add_uIcc a b c

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[simp]
lemma pullback.lift_fst_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    lift (fst f g) (snd f g) condition = 𝟙 (pullback f g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)

Tactic:
apply hom_ext <;> simp

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem exists_finset_of_mem_supr' {ι : Type*} {f : ι → IntermediateField F E} {x : E}
    (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, F⟮(i.2 : E)⟯

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x✝ : E
hx : x✝ ∈ ⨆ i, f i
i : ι
x : E
h : x ∈ f i
⊢ F⟮x⟯ ≤ F⟮↑⟨i, ⟨x, h⟩⟩.snd⟯

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x✝ : E
hx : x✝ ∈ ⨆ i, f i
i : ι
x : E
h : x ∈ f i
⊢ x ∈ ⨆ i, F⟮↑i.snd⟯

Tactic:
exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯

Tactic:
refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x✝ : E
hx : x✝ ∈ ⨆ i, f i
i : ι
x : E
h : x ∈ f i
⊢ x ∈ ⨆ i, F⟮↑i.snd⟯
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem isOrtho_comm {x y : M} : IsOrtho Q x y ↔ IsOrtho Q y x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Q.IsOrtho x y ↔ Q.IsOrtho y x

Tactic:
simp_rw [isOrtho_def, add_comm]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem _root_.Topology.IsInducing.firstCountableTopology {β : Type*}
    [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsInducing f) :
    FirstCountableTopology α

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
exact firstCountableTopology_induced α β f

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_map {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d)

Proof state:
α : Type u
β : Type v
l : List α
d : α
n : ℕ
f : α → β
⊢ (map f l).getD n (f d) = f (l.getD n d)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem isImage_source_target : e.IsImage e.source e.target := fun x hx => by simp [hx]

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ e.target ↔ x ∈ e.source

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma lift_le_lift : lift a ≤ lift b ↔ a ≤ b := ⟨by rintro ⟨_⟩; assumption, LE.lift⟩

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ≤ lift b → a ≤ b

Tactic:
rintro ⟨_⟩

Result:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a ≤ b
⊢ a ≤ b

Proof state:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a ≤ b
⊢ a ≤ b

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_ofList (l : List α) : DList.toList (DList.ofList l) = l

Proof state:
case nil
α : Type u_1
⊢ (ofList []).toList = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Tactic:
rfl

Result:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Proof state:
α : Type u_1
l : List α
⊢ (ofList l).toList = l

Tactic:
cases l

Result:
case nil
α : Type u_1
⊢ (ofList []).toList = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Tactic:
simp [ofList]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem natCast_natAbs_norm {α : Type*} [Ring α] (x : ℤ[i]) : (x.norm.natAbs : α) = x.norm

Proof state:
α : Type u_1
inst✝ : Ring α
x : ℤ[i]
⊢ ↑(norm x).natAbs = ↑(norm x)

Tactic:
rw [← Int.cast_natCast, abs_natCast_norm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_sub_eq_left_of_lt (dg : q.natDegree < n) : (p - q).coeff n = p.coeff n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : q.natDegree < n
⊢ (p - q).coeff n = p.coeff n

Tactic:
rw [← natDegree_neg] at dg

Result:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n

Tactic:
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil),
    getLast (a :: l) (cons_ne_nil a l) = getLast l h

Proof state:
α : Type u_1
a : α
l : List α
⊢ ∀ (h : l ≠ []), (a :: l).getLast ⋯ = l.getLast h

Tactic:
induction l <;> intros

Result:
case nil
α : Type u_1
a : α
h✝ : [] ≠ []
⊢ [a].getLast ⋯ = [].getLast h✝

case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), (a :: tail✝).getLast ⋯ = tail✝.getLast h
h✝ : head✝ :: tail✝ ≠ []
⊢ (a :: head✝ :: tail✝).getLast ⋯ = (head✝ :: tail✝).getLast h✝

Proof state:
case nil
α : Type u_1
a : α
h✝ : [] ≠ []
⊢ [a].getLast ⋯ = [].getLast h✝

Tactic:
contradiction

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
h✝ : [] ≠ []
⊢ [a].getLast ⋯ = [].getLast h✝

case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), (a :: tail✝).getLast ⋯ = tail✝.getLast h
h✝ : head✝ :: tail✝ ≠ []
⊢ (a :: head✝ :: tail✝).getLast ⋯ = (head✝ :: tail✝).getLast h✝

Tactic:
{contradiction}

Result:
case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), (a :: tail✝).getLast ⋯ = tail✝.getLast h
h✝ : head✝ :: tail✝ ≠ []
⊢ (a :: head✝ :: tail✝).getLast ⋯ = (head✝ :: tail✝).getLast h✝

Proof state:
case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), (a :: tail✝).getLast ⋯ = tail✝.getLast h
h✝ : head✝ :: tail✝ ≠ []
⊢ (a :: head✝ :: tail✝).getLast ⋯ = (head✝ :: tail✝).getLast h✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[bound]
lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ ‖(↑x✝¹)⁻¹ • x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖

Tactic:
rw [norm_nnqsmul K]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Pi.lean
theorem edist_pi_le_iff [∀ b, EDist (π b)] {f g : ∀ b, π b} {d : ℝ≥0∞} :
    edist f g ≤ d ↔ ∀ b, edist (f b) (g b) ≤ d :=
  Finset.sup_le_iff.trans <| by simp only [Finset.mem_univ, forall_const]

Proof state:
β : Type v
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → EDist (π b)
f g : (b : β) → π b
d : ℝ≥0∞
⊢ (∀ b ∈ Finset.univ, edist (f b) (g b) ≤ d) ↔ ∀ (b : β), edist (f b) (g b) ≤ d

Tactic:
simp only [Finset.mem_univ, forall_const]

Result:
no goals