harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_one_add {f : ι → α} (s : Finset ι) :
    ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
classical simp only [add_comm (1 : α), prod_add, prod_const_one, mul_one]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
simp only [add_comm (1 : α), prod_add, prod_const_one, mul_one]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem iInf_empty [IsEmpty ι] (f : ι → ℝ≥0) : ⨅ i, f i = 0

Proof state:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ ⨅ i, f i = 0

Tactic:
rw [_root_.iInf_of_isEmpty, sInf_empty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem leadingCoeff_smul_of_smul_regular {S : Type*} [Monoid S] [DistribMulAction S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff

Proof state:
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).leadingCoeff = k • p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
  natDegree_smul_of_smul_regular p h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem hasBiproductsOfShape_of_equiv {K : Type w'} [HasBiproductsOfShape K C] (e : J ≃ K) :
    HasBiproductsOfShape J C :=
  ⟨fun F =>
    let ⟨⟨h⟩⟩ := HasBiproductsOfShape.has_biproduct (F ∘ e.symm)
    let ⟨c, hc⟩ := h
    HasBiproduct.mk <| by
      simpa only [Function.comp_def, e.symm_apply_apply] using
        LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)⟩

Proof state:
J : Type w
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
K : Type w'
inst✝ : HasBiproductsOfShape K C
e : J ≃ K
F : J → C
h : LimitBicone (F ∘ ⇑e.symm)
c : Bicone (F ∘ ⇑e.symm)
hc : c.IsBilimit
⊢ LimitBicone F

Tactic:
simpa only [Function.comp_def, e.symm_apply_apply] using
  LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isOpen_iff (hf : IsInducing f) {s : Set X} :
    IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isOpen_induced_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Coloring.colorable [Fintype α] (C : G.Coloring α) : G.Colorable (Fintype.card α) :=
  ⟨G.recolorOfCardLE (by simp) C⟩

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
C : G.Coloring α
⊢ card α ≤ card (Fin (card α))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem eval₂_modByMonic_eq_self_of_root [CommRing S] {f : R →+* S} {p q : R[X]} (hq : q.Monic)
    {x : S} (hx : q.eval₂ f x = 0) : (p %ₘ q).eval₂ f x = p.eval₂ f x

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
hq : q.Monic
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p

Tactic:
rw [modByMonic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem norm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖

Tactic:
simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsRelPrime.prod_right : (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)

Tactic:
simpa only [isRelPrime_comm] using IsRelPrime.prod_left (α := α)

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kreplace_nodupKeys (a : α) (b : β a) {l : List (Sigma β)} :
    (kreplace a b l).NodupKeys ↔ l.NodupKeys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ (kreplace a b l).NodupKeys ↔ l.NodupKeys

Tactic:
simp [NodupKeys, keys_kreplace]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem hasStrictTerminalObjects_of_terminal_is_strict (I : C) (h : ∀ (A) (f : I ⟶ A), IsIso f) :
    HasStrictTerminalObjects C :=
  { out := fun {I' A} f hI' =>
      haveI := h A (hI'.from _ ≫ f)
      ⟨⟨inv (hI'.from I ≫ f) ≫ hI'.from I, hI'.hom_ext _ _, by rw [assoc, IsIso.inv_hom_id]⟩⟩ }

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (hI'.from I ≫ f)
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A

Tactic:
rw [assoc, IsIso.inv_hom_id]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_tan_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
rcases h0 with (h0 | h0)

Result:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖

Tactic:
rw [tan_angle_add_of_inner_eq_zero h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Proof state:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Result:
no goals

Proof state:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖

Tactic:
simp [h0]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_inf_principal {f : Filter α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ x in f, x ∈ s ∧ p x

Proof state:
α : Type u
f : Filter α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Tactic:
simp only [Filter.Frequently, eventually_inf_principal, not_and]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem beq_eq_decide {α : Type*} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = decide (a = b)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = decide ((a == b) = true)

Tactic:
cases a == b <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = decide (a = b)

Tactic:
rw [← beq_iff_eq (a := a) (b := b)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = decide ((a == b) = true)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
    (x.bind f).map g = x.bind (Option.map g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
x : Option α
⊢ Option.map g (x.bind f) = x.bind (Option.map g ∘ f)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
@[simp]
lemma const_comp' (μ : Measure γ) (κ : Kernel α β) [IsMarkovKernel κ] :
    const β μ ∘ₖ κ = const α μ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝

Tactic:
simp_rw [const_comp, measure_univ, one_smul, const_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ const β μ ∘ₖ κ = const α μ

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝
-- Mathlib/Algebra/Category/Ring/Colimits.lean
theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
    (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
rw [← cocone_naturality F f, comp_apply]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem completeSpace_coe_iff_isComplete {s : Set α} : CompleteSpace s ↔ IsComplete s

Proof state:
α : Type u
inst✝ : UniformSpace α
s : Set α
⊢ CompleteSpace ↑s ↔ IsComplete s

Tactic:
rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
  Subtype.range_coe]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem sSup_apply {s : Set (Seminorm 𝕜 E)} (hp : BddAbove s) {x : E} :
    (sSup s) x = ⨆ p : s, (p : E → ℝ) x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hp : BddAbove s
x : E
⊢ (sSup s) x = ⨆ p, ↑p x

Tactic:
rw [Seminorm.coe_sSup_eq hp, iSup_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem singleton_apply (ι R : Type*) [Unique ι] [Semiring R] (i) : Basis.singleton ι R i = 1 :=
  apply_eq_iff.mpr (by simp [Basis.singleton])

Proof state:
ι : Type u_10
R : Type u_11
inst✝¹ : Unique ι
inst✝ : Semiring R
i : ι
⊢ (Basis.singleton ι R).repr 1 = single i 1

Tactic:
simp [Basis.singleton]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem lt_castPred_succ {a : Fin (n + 1)} (ha : succ a ≠ last (n + 1)) :
    a < (succ a).castPred ha

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a < a.succ.castPred ha

Tactic:
rw [lt_castPred_succ_iff, le_def]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
    (s_nth_eq_some : s.get? n = some aₙ) : ∃ aₘ : α, s.get? m = some aₘ :=
  have : s.get? n ≠ none

Proof state:
α : Type u
s : Seq α
aₙ : α
n m : ℕ
m_le_n : m ≤ n
s_nth_eq_some : s.get? n = some aₙ
⊢ s.get? n ≠ none

Tactic:
simp [s_nth_eq_some]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_div_zpow_mem_Ico {a : α} (ha : 1 < a) (b c : α) :
    ∃! m : ℤ, b / a ^ m ∈ Set.Ico c (c * a)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
b c : α
⊢ ∃! m, b / a ^ m ∈ Ico c (c * a)

Tactic:
simpa only [mem_Ico, le_div_iff_mul_le, one_mul, mul_comm c, div_lt_iff_lt_mul, mul_assoc] using
  existsUnique_zpow_near_of_one_lt' ha (b / c)

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsInt.neg_to_eq {α} [Ring α] {n} :
    {a a' : α} → IsInt a (.negOfNat n) → n = a' → a = -a'
  | _, _, ⟨rfl⟩, rfl => by simp [Int.negOfNat_eq, Int.cast_neg]

Proof state:
α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n

Tactic:
simp [Int.negOfNat_eq, Int.cast_neg]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mul_div_mul (A B C : Finset G) :
    #B * #(A * C) ≤ #(B / A) * #(B * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B / A) * #(B * C)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_invMul_mul_mul A⁻¹ B C

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
    ⟦aig.mkBEqCached input, assign⟧
      =
    (⟦aig, input.lhs, assign⟧
       ==
     ⟦aig, input.rhs, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkBEqCached input⟧ =
    (!(⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧) &&
      !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧))

Tactic:
simp [
  mkBEqCached,
  LawfulOperator.denote_mem_prefix (f := mkGateCached) input.lhs.hgate,
  LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate
]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkBEqCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ == ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
rw [← beq_as_aig]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkBEqCached input⟧ =
    (!(⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧) &&
      !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧))
-- Mathlib/Data/ENNReal/Holder.lean
protected lemma inv_le_inv : p⁻¹ ≤ r⁻¹

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ p⁻¹ ≤ r⁻¹

Tactic:
simp [ENNReal.inv_le_inv, le p q r]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofEpiOfIsIsoOfMono_p : (ofEpiOfIsIsoOfMono φ h).p = inv φ.τ₂ ≫ h.p

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).p = inv φ.τ₂ ≫ h.p

Tactic:
simp [ofEpiOfIsIsoOfMono, opMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem Prod.fst_comp_toSigma :
    Sigma.fst ∘ Prod.toSigma = @Prod.fst α β

Proof state:
case h
α : Type u
β : Type v
⊢ ∀ (x : α × β), (Sigma.fst ∘ toSigma) x = x.fst

Tactic:
simp [Prod.toSigma]

Result:
no goals

Proof state:
α : Type u
β : Type v
⊢ Sigma.fst ∘ toSigma = Prod.fst

Tactic:
apply funext

Result:
case h
α : Type u
β : Type v
⊢ ∀ (x : α × β), (Sigma.fst ∘ toSigma) x = x.fst
-- Mathlib/Algebra/Group/Commute/Basic.lean
@[to_additive]
lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * (b * a) = b

Tactic:
rw [← mul_assoc, h.inv_mul_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_mkArray_of_none {f : α → Option β} (h : f a = none) :
    (mkArray n a).filterMap f = #[]

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h : f a = none
⊢ filterMap f (mkArray n a) = #[]

Tactic:
simp [filterMap_mkArray, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_two_bne_zero : ((a % 2) != 0) = (a % 2 == 1)

Proof state:
a : Nat
⊢ (a % 2 != 0) = (a % 2 == 1)

Tactic:
cases mod_two_eq_zero_or_one a <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_empty : toList (@empty α) = []

Proof state:
α : Type u_1
⊢ empty.toList = []

Tactic:
simp [empty]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toReal = ⨅ i, (f i).toReal

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ (iInf f).toReal = ⨅ i, (f i).toReal

Tactic:
simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem rootMultiplicity_expand :
    (expand R p f).rootMultiplicity r = p * f.rootMultiplicity (r ^ p)

Proof state:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R p) f) = p * rootMultiplicity (r ^ p) f

Tactic:
rw [← pow_one p, rootMultiplicity_expand_pow]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem conjugates_subset_normal {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) :
    conjugatesOf a ⊆ N

Proof state:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ ↑N

Tactic:
exact tn.conj_mem a h c

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a✝ : G
h : a✝ ∈ N
a : G
hc : a ∈ conjugatesOf a✝
⊢ a ∈ ↑N

Tactic:
obtain ⟨c, rfl⟩ := isConj_iff.1 hc

Result:
case intro
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ ↑N

Proof state:
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
⊢ conjugatesOf a ⊆ ↑N

Tactic:
rintro a hc

Result:
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a✝ : G
h : a✝ ∈ N
a : G
hc : a ∈ conjugatesOf a✝
⊢ a ∈ ↑N
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap_id' (h : ∀ (a), ∀ b ∈ f a, a = b) (l : List α) : l.lookmap f = l

Proof state:
case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l

Tactic:
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]

Result:
case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_eq_iff_eq_mul {x} {y : S} {z} : f.mk' x y = z ↔ f.toMap x = z * f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
⊢ f.mk' x y = z ↔ f.toMap x = z * f.toMap ↑y

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mod_pow_succ {x b k : Nat} :
    x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b)

Proof state:
x b k : Nat
⊢ x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)

Tactic:
rw [Nat.pow_succ, Nat.mod_mul]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem Option.id_traverse {α} (x : Option α) : Option.traverse (pure : α → Id α) x = x

Proof state:
α : Type u_1
x : Option α
⊢ Option.traverse pure x = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_eq_one {a : R[X]} : a.toFinsupp = 1 ↔ a = 1

Proof state:
R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = 1 ↔ a = 1

Tactic:
rw [← toFinsupp_one, toFinsupp_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.min_zero {f : α → ℝ} (hf : HasFiniteIntegral f μ) :
    HasFiniteIntegral (fun a => min (f a) 0) μ :=
  hf.mono <| Eventually.of_forall fun x => by simpa [abs_le] using neg_abs_le _

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖f x ⊓ 0‖ ≤ ‖f x‖

Tactic:
simpa [abs_le] using neg_abs_le _

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem eventually_all {ι : Sort*} [Finite ι] {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x

Proof state:
α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

Tactic:
simpa only [Filter.Eventually, setOf_forall] using iInter_mem

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem appIso_hom (U) :
    (f.appIso U).hom = f.app (f ''ᵁ U) ≫ X.presheaf.map
      (eqToHom (preimage_image_eq f U).symm).op :=
  (PresheafedSpace.IsOpenImmersion.inv_invApp f.toPshHom U).trans (by rw [eqToHom_op])

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    f.app (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
rw [eqToHom_op]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKeyD k' (modifyKey k f l) fallback =
      if k == k' then
        if containsKey k l then k else fallback
      else
        getKeyD k' l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' fallback : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKeyD k' (modifyKey k f l) fallback =
    if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback

Tactic:
simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValueCast?, hl]

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem pure_seq_eq_map (f : α → β) (x : Comp F G α) : pure f <*> x = f <$> x :=
  Comp.ext <| by simp [Applicative.pure_seq_eq_map', functor_norm]

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : Comp F G α
⊢ (pure f <*> x).run = (f <$> x).run

Tactic:
simp [Applicative.pure_seq_eq_map', functor_norm]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem pellZd_sub {m n} (h : n ≤ m) : pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
let t := pellZd_add a1 n (m - n)

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
rw [add_tsub_cancel_of_le h] at t

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
-- Mathlib/Logic/Equiv/List.lean
theorem decode_list_zero : decode (α := List α) 0 = some [] :=
  show decodeList 0 = some [] by rw [decodeList]

Proof state:
α : Type u_1
inst✝ : Encodable α
⊢ decodeList 0 = some []

Tactic:
rw [decodeList]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_coe_def (p : K[X]) (q : K[X]⁰) :
    RatFunc.mk p q = ofFractionRing (IsLocalization.mk' _ p q)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
q : ↥K[X]⁰
⊢ RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p q }

Tactic:
simp only [mk_eq_div', ← Localization.mk_eq_mk', FractionRing.mk_eq_div]

Result:
no goals