harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Lean/EStateM.lean
theorem ext {ε σ α} {x y : EStateM ε σ α} (h : ∀ s, x.run s = y.run s) : x = y

Proof state:
ε σ α : Type u_1
x y : EStateM ε σ α
h : ∀ (s : σ), x.run s = y.run s
⊢ x = y

Tactic:
funext s

Result:
case h
ε σ α : Type u_1
x y : EStateM ε σ α
h : ∀ (s : σ), x.run s = y.run s
s : σ
⊢ x s = y s

Proof state:
case h
ε σ α : Type u_1
x y : EStateM ε σ α
h : ∀ (s : σ), x.run s = y.run s
s : σ
⊢ x s = y s

Tactic:
exact h s

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem inl_comp_pushoutObjIso_inv (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    pushout.inl (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inl f g).app d

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ pushout.inl (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inl f g).app d

Tactic:
simp [pushoutObjIso]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma curry_obj_injective {F₁ F₂ : C × D ⥤ E} (h : curry.obj F₁ = curry.obj F₂) :
    F₁ = F₂

Proof state:
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ F₁ = F₂

Tactic:
rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]

Result:
no goals
-- Mathlib/Condensed/Discrete/LocallyConstant.lean
lemma incl_of_counitAppApp [PreservesFiniteProducts Y] [HasExplicitFiniteCoproducts.{u} P]
    (a : Fiber f) : Y.map (sigmaIncl f a).op (counitAppApp S Y f) = counitAppAppImage f a

Proof state:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ sigmaComparison Y (fun a => ↑(fiber f a).toTop)
      (inv (sigmaComparison Y fun a => ↑(fiber f a).toTop) (counitAppAppImage f)) a =
    counitAppAppImage f a

Tactic:
exact congrFun (inv_hom_id_apply (asIso (sigmaComparison Y (fun a ↦ (fiber f a).1)))
  (counitAppAppImage f)) _

Result:
no goals

Proof state:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ ((sigmaComparison Y fun a => ↑(fiber f a).toTop) ≫ fun g => g a) (Y.map (sigmaIso f).hom.op (counitAppApp S Y f)) =
    counitAppAppImage f a

Tactic:
simp only [counitAppApp, Functor.mapIso_inv, ← Iso.op_hom, types_comp_apply,
  ← FunctorToTypes.map_comp_apply, Iso.inv_hom_id, FunctorToTypes.map_id_apply]

Result:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ sigmaComparison Y (fun a => ↑(fiber f a).toTop)
      (inv (sigmaComparison Y fun a => ↑(fiber f a).toTop) (counitAppAppImage f)) a =
    counitAppAppImage f a

Proof state:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ Y.map (sigmaIncl f a).op (counitAppApp S Y f) = counitAppAppImage f a

Tactic:
rw [← sigmaComparison_comp_sigmaIso, Functor.mapIso_hom, Iso.op_hom, types_comp_apply]

Result:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ ((sigmaComparison Y fun a => ↑(fiber f a).toTop) ≫ fun g => g a) (Y.map (sigmaIso f).hom.op (counitAppApp S Y f)) =
    counitAppAppImage f a
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem bot_prod_bot : (⊥ : Submonoid M).prod (⊥ : Submonoid N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]

Proof state:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_of_natDegree_zero {p : R[X]} (hp : p.natDegree = 0) : derivative p = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero hp, derivative_C]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem induction_on {C : Cycle α → Prop} (s : Cycle α) (H0 : C nil)
    (HI : ∀ (a) (l : List α), C ↑l → C ↑(a :: l)) : C s :=
  Quotient.inductionOn' s fun l => by
    refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]
    assumption'

Proof state:
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C (Quotient.mk'' l)

Tactic:
refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]

Result:
case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C nil

case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C ↑tail → C ↑(head :: tail)

Proof state:
case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C nil

case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C ↑tail → C ↑(head :: tail)

Tactic:
assumption'

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Ioo : (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
-- Mathlib/Data/Multiset/Filter.lean
theorem monotone_filter_right (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q]
    (h : ∀ b, p b → q b) :
    s.filter p ≤ s.filter q :=
  Quotient.inductionOn s fun l => (l.monotone_filter_right <| by simpa using h).subperm

Proof state:
α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem divOf_add (x : k[G]) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a b x✝ : G
⊢ (x /ᵒᶠ (a + b)) x✝ = (x /ᵒᶠ a /ᵒᶠ b) x✝

Tactic:
simp only [AddMonoidAlgebra.divOf_apply, add_assoc]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b

Tactic:
ext

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a b x✝ : G
⊢ (x /ᵒᶠ (a + b)) x✝ = (x /ᵒᶠ a /ᵒᶠ b) x✝
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_zero : arg 0 = 0

Proof state:
⊢ arg 0 = 0

Tactic:
simp [arg, le_refl]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_iSup {ι} {m : ι → MeasurableSpace α} {s : Set α} :
    MeasurableSet[iSup m] s ↔ GenerateMeasurable { s : Set α | ∃ i, MeasurableSet[m i] s } s

Proof state:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ i, MeasurableSet s} s

Tactic:
simp only [iSup, measurableSet_sSup, exists_range_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_sup_left {S T : Submonoid M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/ParallelComp.lean
lemma parallelComp_apply (κ : Kernel α β) [IsSFiniteKernel κ]
    (η : Kernel γ δ) [IsSFiniteKernel η] (x : α × γ) :
    (κ ∥ₖ η) x = (κ x.1).prod (η x.2)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
x : α × γ
⊢ (κ ∥ₖ η) x = (κ x.1).prod (η x.2)

Tactic:
rw [parallelComp, prod_apply, prodMkRight_apply, prodMkLeft_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem inf_lie : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆

Tactic:
constructor <;>
apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆

Tactic:
rw [le_inf_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Icc_pred_right {b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b

Proof state:
a b : ℕ
h : 0 < b
⊢ Icc a (b - 1) = Ico a b

Tactic:
ext x

Result:
case h
a b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b

Proof state:
case h
a b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b

Tactic:
rw [mem_Icc, mem_Ico, lt_iff_le_pred h]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma mu'_apply (a b : α) : mu' 𝕜 a b = if a = b then 1 else -∑ x ∈ Ioc a b, mu' 𝕜 x b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (IncidenceAlgebra.mu' 𝕜) a b = if a = b then 1 else -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b

Tactic:
rw [mu', coe_mk, muFun'_apply, sum_attach]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Module/AEval.lean
@[simp] lemma C_smul (t : R) (m : AEval R M a) : C t • m = t • m :=
  (of R M a).symm.injective <| by simp

Proof state:
R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
t : R
m : AEval R M a
⊢ (of R M a).symm (C t • m) = (of R M a).symm (t • m)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = true ↔
      (l₁.isEqv (l₂.take l₁.size) (· == ·) ∧ l₁.size < l₂.size) ∨
        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i])

Proof state:
case mk.mk
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.lex { toList := toList✝ } lt = true ↔
    ({ toList := toList✝¹ }.isEqv ({ toList := toList✝ }.take { toList := toList✝¹ }.size) fun x1 x2 => x1 == x2) =
          true ∧
        { toList := toList✝¹ }.size < { toList := toList✝ }.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), ({ toList := toList✝¹ }[j] == { toList := toList✝ }[j]) = true) ∧
          lt { toList := toList✝¹ }[i] { toList := toList✝ }[i] = true

Tactic:
simp [List.lex_eq_true_iff_exists]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Array α
inst✝ : BEq α
lt : α → α → Bool
⊢ l₁.lex l₂ lt = true ↔
    (l₁.isEqv (l₂.take l₁.size) fun x1 x2 => x1 == x2) = true ∧ l₁.size < l₂.size ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

Tactic:
cases l₁

Result:
case mk
α : Type u_1
l₂ : Array α
inst✝ : BEq α
lt : α → α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.lex l₂ lt = true ↔
    ({ toList := toList✝ }.isEqv (l₂.take { toList := toList✝ }.size) fun x1 x2 => x1 == x2) = true ∧
        { toList := toList✝ }.size < l₂.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), ({ toList := toList✝ }[j] == l₂[j]) = true) ∧
          lt { toList := toList✝ }[i] l₂[i] = true

Proof state:
case mk
α : Type u_1
l₂ : Array α
inst✝ : BEq α
lt : α → α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.lex l₂ lt = true ↔
    ({ toList := toList✝ }.isEqv (l₂.take { toList := toList✝ }.size) fun x1 x2 => x1 == x2) = true ∧
        { toList := toList✝ }.size < l₂.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), ({ toList := toList✝ }[j] == l₂[j]) = true) ∧
          lt { toList := toList✝ }[i] l₂[i] = true

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.lex { toList := toList✝ } lt = true ↔
    ({ toList := toList✝¹ }.isEqv ({ toList := toList✝ }.take { toList := toList✝¹ }.size) fun x1 x2 => x1 == x2) =
          true ∧
        { toList := toList✝¹ }.size < { toList := toList✝ }.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), ({ toList := toList✝¹ }[j] == { toList := toList✝ }[j]) = true) ∧
          lt { toList := toList✝¹ }[i] { toList := toList✝ }[i] = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_succ_ne_nil (n : Nat) (a : α) : replicate (n+1) a ≠ []

Proof state:
α : Type u_1
n : Nat
a : α
⊢ replicate (n + 1) a ≠ []

Tactic:
simp [replicate_succ]

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem sigma_ofNat_val (n : ℕ) :
    ofNat (Sigma γ) n = ⟨ofNat α (unpair n).1, ofNat (γ _) (unpair n).2⟩ :=
  Option.some.inj <| by rw [← decode_eq_ofNat, decode_sigma_val]; simp

Proof state:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
rw [← decode_eq_ofNat, decode_sigma_val]

Result:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_flatMap {β} (l : List α) (f : α → List β) : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (flatMap f l).reverse = flatMap (reverse ∘ f) l.reverse

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
@[simp] lemma powersetCard_card_add (s : Finset α) (hn : 0 < n) :
    s.powersetCard (s.card + n) = ∅

Proof state:
α : Type u_1
n : ℕ
s : Finset α
hn : 0 < n
⊢ powersetCard (#s + n) s = ∅

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem DvdNotUnit.not_unit [CommMonoidWithZero M] {p q : M} (hp : DvdNotUnit p q) : ¬IsUnit q

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hp : DvdNotUnit p q
⊢ ¬IsUnit q

Tactic:
obtain ⟨-, x, hx, rfl⟩ := hp

Result:
case intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p x : M
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p x : M
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)

Tactic:
exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))

Result:
no goals
-- Mathlib/RingTheory/Derivation/ToSquareZero.lean
theorem liftOfDerivationToSquareZero_mk_apply' (d : Derivation R A I) (x : A) :
    (Ideal.Quotient.mk I) (d x) + (algebraMap A (B ⧸ I)) x = algebraMap A (B ⧸ I) x

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : Algebra A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x

Tactic:
simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Indep.of_isRestriction (hI : N.Indep I) (hNM : N ≤r M) : M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.Indep I
hNM : N ≤r M
⊢ M.Indep I

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
exact hI.of_restrict

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem KernelFork.app_one (s : KernelFork f) : s.π.app one = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ s.π.app one = 0

Tactic:
simp [Fork.app_one_eq_ι_comp_right]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem zero_mul' [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ 0 * k = 0

Tactic:
simp [Fin.ext_iff, mul_def]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma leadingCoeff_add_eq_right (h : p.supDegree D < q.supDegree D) :
    (p + q).leadingCoeff D = q.leadingCoeff D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ leadingCoeff D (p + q) = leadingCoeff D q

Tactic:
rw [add_comm, leadingCoeff_add_eq_left h]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem nil_bagInter (l : List α) : [].bagInter l = []

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ [].bagInter l = []

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem zero_rpow_nonneg (x : ℝ) : 0 ≤ (0 : ℝ) ^ x

Proof state:
x : ℝ
⊢ 0 ≤ 0 ^ x

Tactic:
by_cases h : x = 0 <;> simp [h, zero_le_one]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_biUnion_le_tsum {ι : Type*} (f : α → ℝ≥0∞) (s : Set ι) (t : ι → Set α) :
    ∑' x : ⋃ i ∈ s , t i, f x ≤ ∑' i : s, ∑' x : t i, f x :=
  calc ∑' x : ⋃ i ∈ s, t i, f x = ∑' x : ⋃ i : s, t i, f x := tsum_congr_set_coe _ <| by simp
  _ ≤ ∑' i : s, ∑' x : t i, f x := tsum_iUnion_le_tsum _ _

Proof state:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Set ι
t : ι → Set α
⊢ ⋃ i ∈ s, t i = ⋃ i, t ↑i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma le_div_iff_mul_le (h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c

Proof state:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]

Result:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Proof state:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Result:
no goals

Proof state:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Tactic:
rw [mul_div b a b, mul_comm a b]

Result:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_uIcc : Fintype.card (Set.uIcc a b) = (b - a).natAbs + 1

Proof state:
a b : ℤ
⊢ Fintype.card ↑(Set.uIcc a b) = (b - a).natAbs + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ico_succ_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (succ b) = Icc a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (succ b) = Icc a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b

Tactic:
rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]

Result:
no goals