harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_insert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.insert a b).1.2) (insertEntry a b (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insert a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [insert_eq_insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_eq_left (h : a < b) : projIcc a b h.le x = ⟨a, left_mem_Icc.mpr h.le⟩ ↔ x ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
simp [projIcc, Subtype.ext_iff, h.not_le]

Result:
no goals
-- Mathlib/Topology/Instances/ENat.lean
theorem mem_nhds_iff {x : ℕ∞} {s : Set ℕ∞} (hx : x ≠ ⊤) : s ∈ 𝓝 x ↔ x ∈ s

Proof state:
x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_lt (a b c : α) : ((Ico a b).filter fun x => x < c) = Ico a (min b c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (b ⊓ c)

Tactic:
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_iff_mem_unitary : ∀ {b : ℤ√d}, IsPell b ↔ b ∈ unitary (ℤ√d)
  | ⟨x, y⟩ => by rw [unitary.mem_iff, isPell_norm, mul_comm (star _), and_self_iff]

Proof state:
d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } ∈ unitary (ℤ√d)

Tactic:
rw [unitary.mem_iff, isPell_norm, mul_comm (star _), and_self_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma mul_mul_conjTranspose_same {A : Matrix n n R} (hA : PosSemidef A)
    {m : Type*} [Fintype m] (B : Matrix m n R) :
    PosSemidef (B * A * Bᴴ)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix m n R
⊢ (B * A * Bᴴ).PosSemidef

Tactic:
simpa only [conjTranspose_conjTranspose] using hA.conjTranspose_mul_mul_same Bᴴ

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n)

Proof state:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun x => x ^ n) '' σ a ⊆ σ (a ^ n)

Tactic:
simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_le_tsum_comp_of_surjective {f : α → β} (hf : Surjective f) (g : β → ℝ≥0∞) :
    ∑' y, g y ≤ ∑' x, g (f x) :=
  calc ∑' y, g y = ∑' y, g (f (surjInv hf y))

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))

Tactic:
simp only [surjInv_eq hf]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_coprod_of_isSeparator_right (G H : C) [HasBinaryCoproduct G H]
    (hH : IsSeparator H) : IsSeparator (G ⨿ H) :=
  (isSeparator_coprod _ _).2 <| IsSeparating.mono hH <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hH : IsSeparator H
⊢ {H} ⊆ {G, H}

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
theorem measurable_invariants_of_semiconj {fa : α → α} {fb : β → β} {g : α → β} (hg : Measurable g)
    (hfg : Semiconj g fa fb) : @Measurable _ _ (invariants fa) (invariants fb) g := fun s hs ↦
  ⟨hg hs.1, by rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]⟩

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ fa ⁻¹' (g ⁻¹' s) = g ⁻¹' s

Tactic:
rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
@[simp]
lemma range_eq_univ [Surjective f] : Set.range f.base = Set.univ

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : Surjective f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.univ

Tactic:
simpa [Set.range_eq_univ] using f.surjective

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_of_monotone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
    [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Monotone f) :
    Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Proof state:
ι : Type u_3
α : Type u_4
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Tactic:
exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Result:
no goals

Proof state:
ι : Type u_3
α : Type u_4
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)

Tactic:
classical
exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_bot_top [BoundedOrder α] [Fintype α] : Icc (⊥ : α) (⊤ : α) = univ

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Icc ⊥ ⊤ = univ

Tactic:
rw [Icc_bot, Iic_top]

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_coeff_zero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

Tactic:
rw [leftInv]

Result:
no goals
-- Mathlib/Combinatorics/Hindman.lean
theorem FP.singleton {M} [Semigroup M] (a : Stream' M) (i : ℕ) : a.get i ∈ FP a

Proof state:
case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ a.get 0 ∈ FP a

Tactic:
exact FP.head _

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : Semigroup M
i : ℕ
ih : ∀ (a : Stream' M), a.get i ∈ FP a
a : Stream' M
⊢ a.get (i + 1) ∈ FP a

Tactic:
exact FP.tail _ _ (ih _)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ a.get i ∈ FP a

Tactic:
induction i generalizing a with
| zero => exact FP.head _
| succ i ih => exact FP.tail _ _ (ih _)

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)]
lemma mulDissociated_singleton : MulDissociated ({a} : Set α) ↔ a ≠ 1

Proof state:
α : Type u_1
inst✝ : CommGroup α
a : α
⊢ MulDissociated {a} ↔ a ≠ 1

Tactic:
simp [MulDissociated, setOf_or, (Finset.singleton_ne_empty _).symm, -subset_singleton_iff,
  Finset.coe_subset_singleton]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem normal_of_normalizer_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (hn : P.normalizer.Normal) : P.Normal

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hn : (↑P).normalizer.Normal
⊢ (↑P).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← normalizer_sup_eq_top' P le_normalizer, sup_idem]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_X (n : ℕ) : coeff R n (X : R⟦X⟧) = if n = 1 then 1 else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (coeff R n) X = if n = 1 then 1 else 0

Tactic:
rw [X_eq, coeff_monomial]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2

Proof state:
x : ℤ
⊢ ↑x.natAbs ^ 2 = x ^ 2

Tactic:
simp [Int.pow_succ, Int.pow_zero, Int.natAbs_mul_self']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma leftHomologyπ_comp_leftHomologyIso_hom :
    S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π

Tactic:
rw [← leftHomologyπ_naturality']

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π

Tactic:
dsimp only [leftHomologyπ, leftHomologyIso, cyclesIso, leftHomologyMapIso',
  cyclesMapIso', Iso.refl]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_le : ∀ (x : Bool), false ≤ x

Proof state:
⊢ ∀ (x : Bool), false ≤ x

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_hom_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) (h : Y ≅ Z) : f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Y ≅ Z
⊢ f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_ofList [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α} :
    k ∈ (ofList l) ↔ (l.map Prod.fst).contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
⊢ k ∈ ofList l ↔ (List.map Prod.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
    {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a)

Proof state:
α : Type u_1
inst✝² : Min α
inst✝¹ : Std.IdempotentOp min
inst✝ : Std.Associative min
l : List α
a : α
⊢ foldl min a l = min a (l.min?.getD a)

Tactic:
cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ico_add_intCast : ⋃ n : ℤ, Ico (a + n) (a + n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
a : α
⊢ ⋃ n, Ico (a + ↑n) (a + ↑n + 1) = univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  iUnion_Ico_add_zsmul zero_lt_one a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_eq_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) : x ^ z⁻¹ = y ↔ x = y ^ z

Proof state:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_min_const_iff (hτ : IsStoppingTime f τ) (s : Set Ω) {i : ι} :
    MeasurableSet[(hτ.min_const i).measurableSpace] s ↔
      MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[f i] s

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
apply MeasurableSpace.measurableSet_inf

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_zero : B.polar ({0} : Set E) = Set.univ

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ B.polar {0} = Set.univ

Tactic:
simp only [polar_singleton, map_zero, zero_apply, norm_zero, zero_le_one, Set.setOf_true]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_sub_sub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b

Proof state:
a b c : ℕ
h : c ≤ b
⊢ a - c - (b - c) = a - b

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem back?_flatten {L : Array (Array α)} :
    (flatten L).back? = (L.findSomeRev? fun l => l.back?)

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.back? =
    findSomeRev? (fun l => l.back?) (List.map List.toArray xss✝).toArray

Tactic:
simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten.back? = findSomeRev? (fun l => l.back?) L

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.back? =
    findSomeRev? (fun l => l.back?) (List.map List.toArray xss✝).toArray
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
      (ha : a.size = n) (hb : b.size = n) : zipWith f (Vector.mk a ha) (Vector.mk b hb) =
        Vector.mk (Array.zipWith f a b) (by simp [ha, hb]) := rfl

Proof state:
α : Type ?u.17967
β : Type ?u.17970
γ : Type ?u.17992
n : Nat
f : α → β → γ
a : Array α
b : Array β
ha : a.size = n
hb : b.size = n
⊢ (Array.zipWith f a b).size = n

Tactic:
simp [ha, hb]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma pow_eq_divInt (q : ℚ) (n : ℕ) : q ^ n = q.num ^ n /. q.den ^ n

Proof state:
q : ℚ
n : ℕ
⊢ q ^ n = q.num ^ n /. ↑q.den ^ n

Tactic:
rw [pow_def, mk_eq_divInt, Int.natCast_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_le_count_map [DecidableEq β] (l : Vector α n) (f : α → β) (x : α) :
    count x l ≤ count (f x) (map f l)

Proof state:
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
n : Nat
inst✝ : DecidableEq β
l : Vector α n
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
f : α → β
x : α
l : Array α
⊢ count x { toArray := l, size_toArray := ⋯ } ≤ count (f x) (map f { toArray := l, size_toArray := ⋯ })

Proof state:
case mk
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
f : α → β
x : α
l : Array α
⊢ count x { toArray := l, size_toArray := ⋯ } ≤ count (f x) (map f { toArray := l, size_toArray := ⋯ })

Tactic:
simp [Array.count_le_count_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
  | [] => rfl
  | a :: l => by simp

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).head? = (a :: l)[0]?

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_pos_iff_mem_periodicPts : 0 < minimalPeriod f x ↔ x ∈ periodicPts f :=
  ⟨not_imp_not.1 fun h => by simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff],
    minimalPeriod_pos_of_mem_periodicPts⟩

Proof state:
α : Type u_1
f : α → α
x : α
h : x ∉ periodicPts f
⊢ ¬0 < minimalPeriod f x

Tactic:
simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma lintegral_toKernel_univ [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) :
    ∫⁻ b, hf.toKernel f (a, b) univ ∂(ν a) = κ a univ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_toKernel_univ hf a MeasurableSet.univ, univ_prod_univ]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem exists_of_update (self : Buckets α β) (i d h) :
    ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
      (self.update i d h).1.toList = l₁ ++ d :: l₂

Proof state:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d : AssocList α β
h : i.toNat < self.val.size
⊢ ∃ l₁ l₂,
    self.val.toList = l₁ ++ self.val[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.update i d h).val.toList = l₁ ++ d :: l₂

Tactic:
simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_toList]

Result:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d : AssocList α β
h : i.toNat < self.val.size
⊢ ∃ l₁ l₂,
    self.val.toList = l₁ ++ self.val[i.toNat] :: l₂ ∧
      l₁.length = i.toNat ∧ (self.update i d h).val.toList = l₁ ++ d :: l₂

Proof state:
α : Type u_1
β : Type u_2
self : Buckets α β
i : USize
d : AssocList α β
h : i.toNat < self.val.size
⊢ ∃ l₁ l₂,
    self.val.toList = l₁ ++ self.val[i.toNat] :: l₂ ∧
      l₁.length = i.toNat ∧ (self.update i d h).val.toList = l₁ ++ d :: l₂

Tactic:
exact List.exists_of_set h

Result:
no goals
-- Mathlib/Topology/Ultrafilter.lean
theorem continuous_iff_ultrafilter :
    Continuous f ↔ ∀ (x) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x))

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma add_sSup (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

Proof state:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
rw [sSup_eq_iSup, add_biSup hs]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_of_subbasis_of_inter {r : Set (Set α)} (hsg : t = generateFrom r)
    (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ t ∈ r) : IsTopologicalBasis (insert univ r) :=
  isTopologicalBasis_of_subbasis_of_finiteInter (by simpa using hsg) (FiniteInter.mk₂ hsi)

Proof state:
α : Type u
t : TopologicalSpace α
r : Set (Set α)
hsg : t = generateFrom r
hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r
⊢ t = generateFrom (insert univ r)

Tactic:
simpa using hsg

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem pos_eq_zero {l r it} (h : ValidFor l r it) : it.2 = 0 ↔ l = []

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.i = 0 ↔ l = []

Tactic:
simp [h.pos, Pos.ext_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem sigmaCongrRight_sigmaEquivProd :
    (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)
    = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)) ⟨a, b⟩ = ((sigmaEquivProd α₁ β₁).trans (prodCongrRight e)) ⟨a, b⟩

Tactic:
simp

Result:
no goals

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂) = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)) ⟨a, b⟩ = ((sigmaEquivProd α₁ β₁).trans (prodCongrRight e)) ⟨a, b⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_right_max {a b : Nat} : max (a + b) a = a + b

Proof state:
a b : Nat
⊢ max (a + b) a = a + b

Tactic:
rw [Nat.max_comm, max_add_right]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma coyoneda_exact₁ {X : C} (f : X ⟶ T.obj₁⟦(1 : ℤ)⟧) (hf : f ≫ T.mor₁⟦1⟧' = 0) :
    ∃ (g : X ⟶ T.obj₃), f = g ≫ T.mor₃ :=
  coyoneda_exact₂ _ (rot_of_distTriang _ (rot_of_distTriang _ hT)) f (by aesop_cat)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁
hf : f ≫ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
⊢ f ≫ T.rotate.rotate.mor₂ = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/RingTheory/Ideal/Height.lean
theorem Ideal.height_top : (⊤ : Ideal R).height = ⊤

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ ⊤.height = ⊤

Tactic:
simp [height, minimalPrimes_top, iInf₂_eq_top]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma mem_coeffs_iff {p : MvPolynomial σ R} {c : R} :
    c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem applicative_comp_id {F} [AF : Applicative F] [LawfulApplicative F] :
    @Comp.instApplicativeComp F Id _ _ = AF :=
  @Applicative.ext F _ _ (instLawfulApplicativeComp (G := Id)) _
    (fun _ => rfl) (fun f x => show id <$> f <*> x = f <*> x by rw [id_map])

Proof state:
F : Type u_1 → Type u_2
AF : Applicative F
inst✝ : LawfulApplicative F
α✝ β✝ : Type u_1
f : F (α✝ → β✝)
x : F α✝
⊢ id <$> f <*> x = f <*> x

Tactic:
rw [id_map]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem completeSpace_iff_isComplete_range {f : α → β} (hf : IsUniformInducing f) :
    CompleteSpace α ↔ IsComplete (range f)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ CompleteSpace α ↔ IsComplete (range f)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_eq_norm_sq_to_K (x : E) : ⟪x, x⟫ = (‖x‖ : 𝕜) ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, x⟫_𝕜 = ↑‖x‖ ^ 2

Tactic:
rw [← inner_self_ofReal_re, ← norm_sq_eq_inner, ofReal_pow]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma toSubspace_apply (l : Line (η → α) ι) (a ie) :
    ⇑l.toSubspace a ie = l a ie.1 ie.2

Proof state:
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
cases h : l.idxFun ie.1 <;> simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Center.lean
theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g

Proof state:
M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Result:
M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Proof state:
M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

Result:
no goals