harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_add_C_mul_X_pow (f : R[X]) :
    f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f

Tactic:
rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem pred_lt_iff_is_succ {o} : pred o < o ↔ ∃ a, o = succ a :=
  Iff.trans (by simp only [le_antisymm_iff, pred_le_self, true_and, not_le])
    (iff_not_comm.1 pred_eq_iff_not_succ).symm

Proof state:
o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬o.pred = o

Tactic:
simp only [le_antisymm_iff, pred_le_self, true_and, not_le]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc, simp]
lemma objMap_comp {f g h : Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h) :
    objMap I κ (φ ≫ ψ) = objMap I κ φ ≫ objMap I κ ψ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g h : Arrow C
φ : f ⟶ g
ψ : g ⟶ h
⊢ ((iteration I κ).map φ ≫ (iteration I κ).map ψ).left = ((iteration I κ).map φ).left ≫ ((iteration I κ).map ψ).left

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g h : Arrow C
φ : f ⟶ g
ψ : g ⟶ h
⊢ objMap I κ (φ ≫ ψ) = objMap I κ φ ≫ objMap I κ ψ

Tactic:
simp only [objMap, Functor.map_comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g h : Arrow C
φ : f ⟶ g
ψ : g ⟶ h
⊢ ((iteration I κ).map φ ≫ (iteration I κ).map ψ).left = ((iteration I κ).map φ).left ≫ ((iteration I κ).map ψ).left
-- Mathlib/Data/Set/Image.lean
@[gcongr]
lemma image_mono (h : s ⊆ t) : f '' s ⊆ f '' t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
a : α
ha : a ∈ s
⊢ f a ∈ f '' t

Tactic:
exact mem_image_of_mem f (h ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
⊢ f '' s ⊆ f '' t

Tactic:
rintro - ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
a : α
ha : a ∈ s
⊢ f a ∈ f '' t
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.map (h : S.Exact) (F : C ⥤ D)
    [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
    [F.PreservesRightHomologyOf S] : (S.map F).Exact

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).Exact

Tactic:
have := h.hasHomology

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
this : S.HasHomology
⊢ (S.map F).Exact

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
this : S.HasHomology
⊢ (S.map F).Exact

Tactic:
exact h.map_of_preservesLeftHomologyOf F

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem bind_inf_principal {f : Filter α} {g : α → Filter β} {s : Set β} :
    (f.bind fun x => g x ⊓ 𝓟 s) = f.bind g ⊓ 𝓟 s :=
  Filter.ext fun s => by simp only [mem_bind, mem_inf_principal]

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
s✝ s : Set β
⊢ (s ∈ f.bind fun x => g x ⊓ 𝓟 s✝) ↔ s ∈ f.bind g ⊓ 𝓟 s✝

Tactic:
simp only [mem_bind, mem_inf_principal]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.coneMorphism_π {F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) :
    (limit.coneMorphism c).hom ≫ limit.π F j = c.π.app j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
j : J
⊢ (coneMorphism c).hom ≫ π F j = c.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@[reassoc (attr := simp)]
lemma ι_colimitIsoOfIsLeftKanExtension_hom (i : C) :
    α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom =
      colimit.ι F i

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_3} H
inst✝³ : Category.{u_8, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom = colimit.ι F i

Tactic:
simp [colimitIsoOfIsLeftKanExtension]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem LocallyFinite.finite_of_compact [CompactSpace X] {f : ι → Set X}
    (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Finite

Proof state:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Finite

Tactic:
simpa only [hne] using hf.finite_nonempty_of_compact

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
private lemma pairMap_ne_self (t : Finset σ × σ) : pairMap σ t ≠ t

Proof state:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ MvPolynomial.NewtonIdentities.pairMap σ t ≠ t

Tactic:
rw [pairMap]

Result:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t

Tactic:
split_ifs with h1

Result:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
⊢ (t.1.erase t.2, t.2) ≠ t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
⊢ (cons t.2 t.1 h1, t.2) ≠ t

Proof state:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
⊢ (t.1.erase t.2, t.2) ≠ t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
⊢ (cons t.2 t.1 h1, t.2) ≠ t

Tactic:
all_goals by_contra ht; rw [← ht] at h1; simp_all

Result:
no goals

Proof state:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ False

Tactic:
rw [← ht] at h1

Result:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False

Proof state:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
⊢ (cons t.2 t.1 h1, t.2) ≠ t

Tactic:
by_contra ht

Result:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Vector α n) :
    l.foldr f b = l.foldrM (m := Id) f b

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β → β
b : β
l : Vector α n
⊢ foldr f b l = foldrM f b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : Array α
⊢ foldr f b { toArray := l, size_toArray := ⋯ } = foldrM f b { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : Array α
⊢ foldr f b { toArray := l, size_toArray := ⋯ } = foldrM f b { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldr_eq_foldrM]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem toOuterMeasure_map_apply : (p.map f).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ (∑' (a : α), if f a ∈ s then p a else 0) = ∑' (x : α), if x ∈ f ⁻¹' s then p x else 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ (map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)

Tactic:
simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ (∑' (a : α), if f a ∈ s then p a else 0) = ∑' (x : α), if x ∈ f ⁻¹' s then p x else 0
-- Mathlib/Algebra/Group/Support.lean
theorem image_inter_mulSupport_eq {s : Set β} {g : β → α} :
    g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
f : α → M
s : Set β
g : β → α
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Tactic:
rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem iUnion_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    [(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α}
    (hsm : Monotone s) (hs : ∀ i, MeasurableSet (s i)) : MeasurableSet (⋃ i, s i)

Proof state:
case inl
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ i, s i)

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ i, s i)

Tactic:
exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
cases isEmpty_or_nonempty ι with
| inl _ => simp
| inr _ => exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem fst_mem_divisors_of_mem_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) :
    x.fst ∈ divisors n

Proof state:
n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 ∈ n.divisors

Tactic:
rw [mem_divisorsAntidiagonal] at h

Result:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors

Proof state:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors

Tactic:
simp [Dvd.intro _ h.1, h.2]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean
theorem banach_steinhaus_iSup_nnnorm {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}
    (h : ∀ x, (⨆ i, ↑‖g i x‖₊) < ∞) : (⨆ i, ↑‖g i‖₊) < ∞

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))

Tactic:
simpa [← NNReal.bddAbove_coe, ← Set.range_comp] using ENNReal.iSup_coe_lt_top.1 (h x)

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤
⊢ UniformEquicontinuous (DFunLike.coe ∘ g)

Tactic:
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Result:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))

Proof state:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤
⊢ ⨆ i, ↑‖g i‖₊ < ⊤

Tactic:
rw [show ((⨆ i, ↑‖g i‖₊) < ∞) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 8 2]

Result:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤
⊢ UniformEquicontinuous (DFunLike.coe ∘ g)
-- Mathlib/Topology/Order/Basic.lean
theorem pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioc a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)

Result:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioc_mem_nhds (ha i) (hb i)

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem linearProjOfIsCompl_apply_left (h : IsCompl p q) (x : p) :
    linearProjOfIsCompl p q h x = x

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥p
⊢ (p.linearProjOfIsCompl q h) ↑x = x

Tactic:
simp [linearProjOfIsCompl]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedMul_one (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) :
    gradedMul R 𝒜 ℬ x 1 = x

Proof state:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ ((gradedMul R 𝒜 ℬ) x) 1 = x

Tactic:
simpa only [RingHom.map_one, one_smul] using gradedMul_algebraMap 𝒜 ℬ x 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β}
    (h : m.WF) : Const.get! (Const.modify m k f) k' =
      if k == k' then
        Const.get? m k |>.map f |>.get!
      else
        Const.get! m k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
k k' : α
inst✝ : Inhabited β
f : β → β
h : m.WF
⊢ get! (modify m k f) k' = if (k == k') = true then (Option.map f (get? m k)).get! else get! m k'

Tactic:
simp_to_raw using Raw₀.Const.get!_modify

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_pair [DecidableEq α] {a b : α} (h : a ≠ b) :
    (∏ x ∈ ({a, b} : Finset α), f x) = f a * f b

Proof state:
α : Type u_3
β : Type u_4
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ ∏ x ∈ {a, b}, f x = f a * f b

Tactic:
rw [prod_insert (not_mem_singleton.2 h), prod_singleton]

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem ofEquiv_ofNat (α) {β} [Denumerable α] (e : β ≃ α) (n) :
    @ofNat β (ofEquiv _ e) n = e.symm (ofNat α n)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (e.symm (ofNat α n))

Tactic:
rw [decode_ofEquiv e]

Result:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
refine ofNat_of_decode ?_

Result:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (e.symm (ofNat α n))

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
letI := ofEquiv _ e

Result:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = e.symm (ofNat α n)
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_id (X : C) : adj.homEquiv X _ (𝟙 _) = adj.unit.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
⊢ (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X)) = adj.unit.app X

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem subset_toFinset {s : Finset α} : s ⊆ ht.toFinset ↔ ↑s ⊆ t

Proof state:
α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊆ ht.toFinset ↔ ↑s ⊆ t

Tactic:
rw [← Finset.coe_subset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Lemmas.lean
theorem minimalPeriod_eq_prime_pow {p k : ℕ} [hp : Fact p.Prime] (hk : ¬IsPeriodicPt f (p ^ k) x)
    (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) : minimalPeriod f x = p ^ (k + 1)

Proof state:
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x = p ^ (k + 1)

Tactic:
apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out <;>
  rwa [← isPeriodicPt_iff_minimalPeriod_dvd]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem succ_nmul (a b) : succ a ⨳ b = a ⨳ b ♯ b

Proof state:
a b : Ordinal.{u_1}
⊢ succ a ⨳ b = a ⨳ b ♯ b

Tactic:
rw [← nadd_one, nadd_one_nmul]

Result:
no goals
-- Mathlib/Algebra/Lie/Quotient.lean
theorem map_mk'_eq_bot_le : map (mk' N) N' = ⊥ ↔ N' ≤ 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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ map (mk' N) N' = ⊥ ↔ N' ≤ N

Tactic:
rw [← LieModuleHom.le_ker_iff_map, mk'_ker]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem subsingleton_reverse_iff {s : Cycle α} : s.reverse.Subsingleton ↔ s.Subsingleton

Proof state:
α : Type u_1
s : Cycle α
⊢ s.reverse.Subsingleton ↔ s.Subsingleton

Tactic:
simp [length_subsingleton_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.mono (hψφ : ψ ≤ φ) (hf : UniformConvexOn s φ f) : UniformConvexOn s ψ f :=
  ⟨hf.1, fun x hx y hy a b ha hb hab ↦ (hf.2 hx hy ha hb hab).trans <| by gcongr; apply hψφ⟩

Proof state:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖

Tactic:
apply hψφ

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y - a * b * φ ‖x - y‖ ≤ a • f x + b • f y - a * b * ψ ‖x - y‖

Tactic:
gcongr

Result:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma fourierTransform_eq_gaussSum_mulShift (χ : DirichletCharacter ℂ N) (k : ZMod N) :
    𝓕 χ k = gaussSum χ (stdAddChar.mulShift (-k))

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
⊢ 𝓕 (⇑χ) k = gaussSum χ (stdAddChar.mulShift (-k))

Tactic:
simp only [dft_apply, smul_eq_mul]

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
⊢ ∑ x : ZMod N, stdAddChar (-(x * k)) * χ x = gaussSum χ (stdAddChar.mulShift (-k))

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k : ZMod N
⊢ ∑ x : ZMod N, stdAddChar (-(x * k)) * χ x = gaussSum χ (stdAddChar.mulShift (-k))

Tactic:
congr 1 with j

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ stdAddChar (-(j * k)) * χ j = χ j * (stdAddChar.mulShift (-k)) j

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ stdAddChar (-(j * k)) * χ j = χ j * (stdAddChar.mulShift (-k)) j

Tactic:
rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
lemma of_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n]

Proof state:
n a b m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a

Tactic:
exact (dvd_mul_left n m).trans h

Result:
no goals

Proof state:
n a b m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]

Tactic:
rw [modEq_iff_dvd] at *

Result:
n a b m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ne_of_lt {a b : Int} (h : a < b) : a ≠ b := fun e => by
  cases e; exact Int.lt_irrefl _ h

Proof state:
case refl
a : Int
h : a < a
⊢ False

Tactic:
exact Int.lt_irrefl _ h

Result:
no goals

Proof state:
a b : Int
h : a < b
e : a = b
⊢ False

Tactic:
cases e

Result:
case refl
a : Int
h : a < a
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False

Proof state:
a b : Prop
h : b = False
⊢ (a ∧ b) = False

Tactic:
simp [h]

Result:
no goals