harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_pbind {o : Option α} {f : (a : α) → a ∈ o → Option β} {g : β → γ} :
    (o.pbind f).map g = o.pbind (fun a h => (f a h).map g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
o : Option α
f : (a : α) → a ∈ o → Option β
g : β → γ
⊢ Option.map g (o.pbind f) = o.pbind fun a h => Option.map g (f a h)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem le_boundedBy {μ : OuterMeasure α} : μ ≤ boundedBy m ↔ ∀ s, μ s ≤ m s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

Tactic:
rcases s.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ ⨆ (_ : a.Nonempty), m a ↔ μ a ≤ m a

Tactic:
intro s

Result:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s

Tactic:
rw [boundedBy , le_ofFunction, forall_congr']

Result:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ ⨆ (_ : a.Nonempty), m a ↔ μ a ≤ m a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_mkArray (n : Nat) (a : α) (p : α → Bool) :
    (mkArray n a).eraseP p = if p a then mkArray (n - 1) a else mkArray n a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ (if p a = true then List.replicate (n - 1) a else List.replicate n a).toArray =
    if p a = true then (List.replicate (n - 1) a).toArray else (List.replicate n a).toArray

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ (mkArray n a).eraseP p = if p a = true then mkArray (n - 1) a else mkArray n a

Tactic:
simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]

Result:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ (if p a = true then List.replicate (n - 1) a else List.replicate n a).toArray =
    if p a = true then (List.replicate (n - 1) a).toArray else (List.replicate n a).toArray
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma ncard_sdiff_of_mem (hrep : Represents s C) (h : c ∈ C) :
    (c.supp \ s).ncard = c.supp.ncard - 1

Proof state:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ {a} ⊆ c.supp

Tactic:
simp [← ha]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h

Result:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Proof state:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
rw [← Set.diff_inter_self_eq_diff, ha, Set.ncard_diff, Set.ncard_singleton]

Result:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ {a} ⊆ c.supp
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem mem_cylinder_comm (x y : ∀ n, E n) (n : ℕ) : y ∈ cylinder x n ↔ x ∈ cylinder y n

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ x ∈ cylinder y n

Tactic:
simp [mem_cylinder_iff_eq, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
@[reassoc]
lemma homologySequenceδ_naturality
    [F.ShiftSequence ℤ] (T T' : Triangle C) (φ : T ⟶ T') (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (F.shift n₀).map φ.hom₃ ≫ F.homologySequenceδ T' n₀ n₁ h =
      F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map φ.hom₁

Proof state:
C : Type u_1
A : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : HasShift C ℤ
inst✝¹ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁

Tactic:
rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : HasShift C ℤ
inst✝¹ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.homologySequenceδ T' n₀ n₁ h = F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map φ.hom₁

Tactic:
dsimp only [homologySequenceδ]

Result:
C : Type u_1
A : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : HasShift C ℤ
inst✝¹ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.one_le {a : A} (h : ∀ x ∈ spectrum R a, 1 ≤ x) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.754080) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
h : ∀ x ∈ spectrum R a, 1 ≤ x
ha : autoParam (p a) _auto✝
⊢ 1 ≤ a

Tactic:
simpa using algebraMap_le_of_le_spectrum h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENatAux_eq_nat {x : Cardinal} {n : ℕ} : toENatAux x = n ↔ x = n

Proof state:
x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux = ↑n ↔ x = ↑n

Tactic:
simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image₂ f s t = image₂ g t s :=
  (image₂_swap _ _ _).trans <| by simp_rw [h_comm]

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image₂ (fun a b => f b a) t s = image₂ g t s

Tactic:
simp_rw [h_comm]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem integral_exp_mul_eval (p : ℂ[X]) (s : ℂ) :
    s * ∫ x in (0)..1, exp (-(x • s)) * p.eval (x • s) =
      -(exp (-s) * p.sumIDeriv.eval s) + p.sumIDeriv.eval 0

Proof state:
p : ℂ[X]
s : ℂ
⊢ -(cexp (-(1 • s)) * eval (1 • s) (sumIDeriv p)) - -(cexp (-(0 • s)) * eval (0 • s) (sumIDeriv p)) =
    -(cexp (-s) * eval s (sumIDeriv p)) + eval 0 (sumIDeriv p)

Tactic:
simp

Result:
no goals

Proof state:
p : ℂ[X]
s : ℂ
⊢ ContinuousOn (fun x => s * (cexp (-(x • s)) * eval (x • s) p)) (Set.uIcc 0 1)

Tactic:
fun_prop

Result:
no goals

Proof state:
p : ℂ[X]
s : ℂ
⊢ s * ∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) p = -(cexp (-s) * eval s (sumIDeriv p)) + eval 0 (sumIDeriv p)

Tactic:
rw [← intervalIntegral.integral_const_mul,
  intervalIntegral.integral_eq_sub_of_hasDerivAt
    (fun x hx => hasDerivAt_cexp_mul_sumIDeriv p s x)
    (ContinuousOn.intervalIntegrable (by fun_prop))]

Result:
p : ℂ[X]
s : ℂ
⊢ -(cexp (-(1 • s)) * eval (1 • s) (sumIDeriv p)) - -(cexp (-(0 • s)) * eval (0 • s) (sumIDeriv p)) =
    -(cexp (-s) * eval s (sumIDeriv p)) + eval 0 (sumIDeriv p)
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma of_commsq {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : p.map φ ≫ eqToHom hb = (eqToHom ha) ≫ f) : p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p.map φ
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
⊢ p.IsHomLift f φ

Tactic:
subst ha hb

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ p.IsHomLift f φ

Tactic:
obtain rfl : f = p.map φ := by simpa using h.symm

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p.map φ
⊢ p.IsHomLift (p.map φ) φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ f = p.map φ

Tactic:
simpa using h.symm

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCircuit_eq_sInter (he : e ∈ M.closure I) :
    M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [fundCircuit]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ {e} ⊆ M.E

Tactic:
simpa using mem_ground_of_mem_closure he

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [inter_eq_self_of_subset_right (sInter_subset_of_mem (by simpa))]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
simp_rw [closure_subset_closure_iff_subset_closure
  (show {e} ⊆ M.E by simpa using mem_ground_of_mem_closure he), singleton_subset_iff]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem cg_iff_countable [Countable (Σl, L.Functions l)] : CG L M ↔ Countable M

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ CG L M ↔ Countable M

Tactic:
rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]

Result:
no goals
-- Mathlib/Order/Max.lean
theorem IsBot.isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i

Proof state:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i

Tactic:
simp_rw [le_antisymm_iff, h j, and_true]

Result:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i

Proof state:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i

Tactic:
exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean
private lemma adjRetraction_is_retraction (c : C) (d : D)
    [IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))] :
    adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      adj.unit.app ((ihom d).obj (R.obj c)) ▷ d ≫
        R.obj (L.obj ((ihom d).obj (R.obj c))) ◁ adj.unit.app d ≫
          adj.unit.app (R.obj (L.obj ((ihom d).obj (R.obj c))) ⊗ R.obj (L.obj d)) ≫
            inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))) ≫
              R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom) ≫
                R.map (L.map ((ihom.ev d).app (R.obj c))) ≫ inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
slice_lhs 2 3 =>
  simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, Category.id_comp, Category.comp_id]

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((((adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d) ≫
                adj.unit.app (R.obj (L.obj ((ihom d).obj (R.obj c))) ⊗ R.obj (L.obj d))) ≫
              inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((adj.unit.app ((ihom d).obj (R.obj c) ⊗ d) ≫
              R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.toPrefunctor.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ofMul_list_prod (s : List α) : ofMul s.prod = (s.map ofMul).sum

Proof state:
α : Type u_3
inst✝ : Monoid α
s : List α
⊢ ofMul s.prod = (List.map (⇑ofMul) s).sum

Tactic:
simp [ofMul]

Result:
α : Type u_3
inst✝ : Monoid α
s : List α
⊢ s.prod = s.sum

Proof state:
α : Type u_3
inst✝ : Monoid α
s : List α
⊢ s.prod = s.sum

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_subtype_subset {t : Set α} (s : Finset t) : ↑(s.map (Embedding.subtype _)) ⊆ t

Proof state:
α : Type u_1
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x => x ∈ t) s) ⊆ t

Tactic:
intro a ha

Result:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)
⊢ a ∈ t

Proof state:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s
⊢ a ∈ t

Tactic:
convert property_of_mem_map_subtype s ha

Result:
no goals

Proof state:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)
⊢ a ∈ t

Tactic:
rw [mem_coe] at ha

Result:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s
⊢ a ∈ t
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma image_comap_C_basicOpen (f : R[X]) :
    comap C '' basicOpen f = (zeroLocus (Set.range f.coeff))ᶜ

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ (∃ i, f.coeff i ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
simp [Set.range_subset_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ ⇑(comap C) '' ↑(basicOpen f) = (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
ext p

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ p ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ p ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
rw [mem_image_comap_C_basicOpen]

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ (∃ i, f.coeff i ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma rTensorAlgHom_apply_eq (p : MvPolynomial σ S ⊗[R] N) :
    rTensorAlgHom (S := S) p = rTensor p

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensor p = rTensor p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
⊢ rTensorAlgHom p = rTensor p

Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]

Result:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
⊢ ↑rTensor p = rTensor p
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIcc : Fintype.card (Set.Icc a b) = b + 1 - a

Proof state:
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a

Tactic:
rw [← card_Icc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp) nsmul_singleton]
lemma singleton_pow (a : α) : ∀ n, ({a} : Finset α) ^ n = {a ^ n}
  | 0 => by simp [singleton_one]
  | n + 1 => by simp [pow_succ, singleton_pow _ n]

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
⊢ {a} ^ 0 = {a ^ 0}

Tactic:
simp [singleton_one]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.append_left_iff : ∀ L, Step (L ++ L₁) (L ++ L₂) ↔ Step L₁ L₂
  | [] => by simp
  | p :: l => by simp [Step.append_left_iff l, Step.cons_cons_iff]

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
l : List (α × Bool)
⊢ Step (p :: l ++ L₁) (p :: l ++ L₂) ↔ Step L₁ L₂

Tactic:
simp [Step.append_left_iff l, Step.cons_cons_iff]

Result:
no goals

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ Step ([] ++ L₁) ([] ++ L₂) ↔ Step L₁ L₂

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.emultiplicity_eq_multiplicity (h : FiniteMultiplicity a b) :
    emultiplicity a b = multiplicity a b

Proof state:
case top
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
hm : emultiplicity a b = ⊤
⊢ ⊤ = ↑(multiplicity a b)

Tactic:
simp [h] at hm

Result:
no goals

Proof state:
case coe
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
a✝ : ℕ
hm : emultiplicity a b = ↑a✝
⊢ ↑a✝ = ↑(multiplicity a b)

Tactic:
rw [multiplicity_eq_of_emultiplicity_eq_some hm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑(multiplicity a b)

Tactic:
cases hm : emultiplicity a b

Result:
case top
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
hm : emultiplicity a b = ⊤
⊢ ⊤ = ↑(multiplicity a b)

case coe
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
a✝ : ℕ
hm : emultiplicity a b = ↑a✝
⊢ ↑a✝ = ↑(multiplicity a b)
-- Mathlib/Data/List/Intervals.lean
theorem pred_singleton {m : ℕ} (h : 0 < m) : Ico (m - 1) m = [m - 1]

Proof state:
m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]

Tactic:
simp [Ico, Nat.sub_sub_self (succ_le_of_lt h)]

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem tendsto_iff_tendstoLocallyUniformly [WeaklyLocallyCompactSpace α] :
    Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => F i a) f p

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V

Tactic:
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn] at h

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V

Proof state:
case intro.intro
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V

Tactic:
exact ⟨n, hn₂, h n hn₁ V hV⟩

Result:
no goals

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_compact_mem_nhds x

Result:
case intro.intro
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
⊢ Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p

Tactic:
refine ⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_at_natCast {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) :
    p.eval₂ f n = f (p.eval n)

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ eval₂ f (↑n) p = f (eval (↑n) p)

Tactic:
convert eval₂_at_apply (p := p) f n

Result:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ↑n = f ↑n

Proof state:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ↑n = f ↑n

Tactic:
simp

Result:
no goals