harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Defs.lean
theorem ext_fun (h : ∀ a f, Measurable f → ∫⁻ b, f b ∂κ a = ∫⁻ b, f b ∂η a) :
    κ = η

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) s = (η a) s

Tactic:
specialize h a (s.indicator fun _ => 1) (Measurable.indicator measurable_const hs)

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : ∫⁻ (b : β), s.indicator (fun x => 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x => 1) b ∂η a
⊢ (κ a) s = (η a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : ∫⁻ (b : β), s.indicator (fun x => 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x => 1) b ∂η a
⊢ (κ a) s = (η a) s

Tactic:
simp_rw [lintegral_indicator_const hs, one_mul] at h

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : (κ a) s = (η a) s
⊢ (κ a) s = (η a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : (κ a) s = (η a) s
⊢ (κ a) s = (η a) s

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a
⊢ κ = η

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) s = (η a) s
-- Mathlib/NumberTheory/SiegelsLemma.lean
/-- The sup norm of a non-zero integer matrix is at least one -/
lemma one_le_norm_A_of_ne_zero (hA : A ≠ 0) : 1 ≤ ‖A‖

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ False

Tactic:
apply hA

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ A = 0

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : ‖A i j‖ < 1
⊢ A i j = 0

Tactic:
rw [Int.norm_eq_abs] at h

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |↑(A i j)| < 1
⊢ A i j = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
⊢ 1 ≤ ‖A‖

Tactic:
by_contra! h

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ False

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |↑(A i j)| < 1
⊢ A i j = 0

Tactic:
norm_cast at h

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |A i j| < 1
⊢ A i j = 0

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0

Tactic:
rw [norm_lt_iff Real.zero_lt_one] at h

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ∀ (i : α) (j : β), ‖A i j‖ < 1
i : α
j : β
⊢ A i j = 0

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0 i j

Tactic:
simp only [zero_apply]

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ A = 0

Tactic:
ext i j

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0 i j

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |A i j| < 1
⊢ A i j = 0

Tactic:
exact Int.abs_lt_one_iff.1 h

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ∀ (i : α) (j : β), ‖A i j‖ < 1
i : α
j : β
⊢ A i j = 0

Tactic:
specialize h i j

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : ‖A i j‖ < 1
⊢ A i j = 0
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem eq_C_content_mul_primPart (p : R[X]) : p = C p.content * p.primPart

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * p.primPart

Tactic:
rw [primPart, if_neg h, ← Classical.choose_spec (C_content_dvd p)]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = C p.content * p.primPart

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * p.primPart
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem submonoid_map_le_is_unit : M.map (algebraMap R S) ≤ IsUnit.submonoid S

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ (algebraMap R S) a ∈ IsUnit.submonoid S

Tactic:
exact IsLocalization.map_units S ⟨_, ha⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ (algebraMap R S) a ∈ IsUnit.submonoid S
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_subset_Icc_self : Ioc a b ⊆ Icc a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ioc, coe_Icc]

Result:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Icc a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Icc a b

Tactic:
exact Set.Ioc_subset_Icc_self

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivAt.lim_real (hf : HasFDerivAt f f' x) (v : E) :
    Tendsto (fun c : ℝ => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v))

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖

Tactic:
exact fun b => ⟨b, fun a ha => le_trans ha (le_abs_self _)⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun n => ‖n‖) atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun c => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v))

Tactic:
apply hf.lim v

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun n => ‖n‖) atTop atTop
-- Mathlib/Order/WellFoundedSet.lean
theorem BddBelow.wellFoundedOn_lt : BddBelow s → s.WellFoundedOn (· < ·)

Proof state:
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → ∀ (f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2), ¬∀ (n : ℕ), f n ∈ s

Tactic:
rintro ⟨a, ha⟩ f hf

Result:
case intro
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ False

Proof state:
case intro
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ (range ⇑f).Finite

Tactic:
exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
  ⟨ha <| hf _,
    antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Result:
no goals

Proof state:
case intro
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ False

Tactic:
refine infinite_range_of_injective f.injective ?_

Result:
case intro
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ (range ⇑f).Finite

Proof state:
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun x1 x2 => x1 < x2

Tactic:
rw [wellFoundedOn_iff_no_descending_seq]

Result:
α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → ∀ (f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2), ¬∀ (n : ℕ), f n ∈ s
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} : f =o[l] g' ↔ ∀ i, (fun x => f x i) =o[l] g'

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith c l (fun x => f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f x i) g'

Tactic:
exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =o[l] g' ↔ ∀ (i : ι), (fun x => f x i) =o[l] g'

Tactic:
simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]

Result:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith c l (fun x => f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f x i) g'
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma isIso_homologyπ : IsIso (K.homologyπ j) :=
  ShortComplex.isIso_homologyπ _ (by aesop_cat)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst✝ : K.HasHomology j
⊢ (K.sc j).f = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_eq_bot_iff : ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅(x : L), m⁆ = 0

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 : LieIdeal R L
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0) → ∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0

Tactic:
rintro h - ⟨⟨x, hx⟩, ⟨⟨n, hn⟩, rfl⟩⟩

Result:
case intro.mk.intro.mk
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 : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = 0

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 : LieIdeal R L
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_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 : LieIdeal R L
⊢ (∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Proof state:
case intro.mk.intro.mk
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 : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = 0

Tactic:
exact h x hx n hn

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 : LieIdeal R L
⊢ (∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
refine ⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩

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 : LieIdeal R L
⊢ (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0) → ∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0
-- Mathlib/Data/Nat/PartENat.lean
theorem dom_of_le_natCast {x : PartENat} {y : ℕ} (h : x ≤ y) : x.Dom

Proof state:
x : PartENat
y : ℕ
h : x ≤ ↑y
⊢ x.Dom

Tactic:
exact dom_of_le_some h

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem differentiable_tsum' (hu : Summable u) (hg : ∀ n y, HasDerivAt (g n) (g' n y) y)
    (hg' : ∀ n y, ‖g' n y‖ ≤ u n) : Differentiable 𝕜 fun z => ∑' n, g n z

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ Differentiable 𝕜 fun z => ∑' (n : α), g n z

Tactic:
refine differentiable_tsum hu hg ?_

Result:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α) (x : 𝕜), ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α) (x : 𝕜), ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Tactic:
simpa? says simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
⊢ Differentiable 𝕜 fun z => ∑' (n : α), g n z

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg

Result:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ Differentiable 𝕜 fun z => ∑' (n : α), g n z

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α) (x : 𝕜), ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Tactic:
simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem continuous_circleMap_inv {R : ℝ} {z w : ℂ} (hw : w ∈ ball z R) :
    Continuous fun θ => (circleMap z R θ - w)⁻¹

Proof state:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => circleMap z R θ - w

Tactic:
fun_prop

Result:
no goals

Proof state:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0

Tactic:
simp_rw [sub_ne_zero]

Result:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w

Proof state:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹

Tactic:
have : ∀ θ, circleMap z R θ - w ≠ 0 := by
  simp_rw [sub_ne_zero]
  exact fun θ => circleMap_ne_mem_ball hw θ

Result:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹

Proof state:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹

Tactic:
exact Continuous.inv₀ (by fun_prop) this

Result:
no goals

Proof state:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w

Tactic:
exact fun θ => circleMap_ne_mem_ball hw θ

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_one_right [NatPowAssoc R] (r : R) : choose r 1 = r

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ choose r 1 = r

Tactic:
rw [choose_one_right', npow_one]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion₂_eq_univ_iff {s : ∀ i, κ i → Set α} :
    ⋃ (i) (j), s i j = univ ↔ ∀ a, ∃ i j, a ∈ s i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋃ i, ⋃ j, s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j

Tactic:
simp only [iUnion_eq_univ_iff, mem_iUnion]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset_iff_segment_subset (hx : x ∈ s) (hy : y ∈ s) :
    openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x-[𝕜]y] ⊆ s

Tactic:
simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem mapsTo_iInter₂ {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} :
    MapsTo f s (⋂ (i) (j), t i j) ↔ ∀ i j, MapsTo f s (t i j)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
f : α → β
⊢ MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

Tactic:
simp only [mapsTo_iInter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_filter {l : List α} (p : α → Bool) :
    (l.filter p).attach = l.attach.filterMap
      fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ filterMap
      (fun x =>
        Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x.val = true then some x.val else none).pbind fun b m => some ⟨b, ⋯⟩))
      l.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Tactic:
congr

Result:
case e_f
α : Type u_1
l : List α
p : α → Bool
⊢ (fun x =>
      Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x.val = true then some x.val else none).pbind fun b m => some ⟨b, ⋯⟩)) =
    fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ filterMap
      (fun x =>
        Option.map (fun x => ⟨x.val, ⋯⟩)
          (match x with
          | ⟨x, h⟩ => (Option.guard (fun x => p x = true) x).pbind fun b m => some ⟨b, ⋯⟩))
      l.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Tactic:
simp only [Option.guard]

Result:
α : Type u_1
l : List α
p : α → Bool
⊢ filterMap
      (fun x =>
        Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x.val = true then some x.val else none).pbind fun b m => some ⟨b, ⋯⟩))
      l.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Proof state:
case e_f
α : Type u_1
l : List α
p : α → Bool
⊢ (fun x =>
      Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x.val = true then some x.val else none).pbind fun b m => some ⟨b, ⋯⟩)) =
    fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none

Tactic:
ext1

Result:
case e_f.h
α : Type u_1
l : List α
p : α → Bool
x✝ : { x // x ∈ l }
⊢ Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x✝.val = true then some x✝.val else none).pbind fun b m => some ⟨b, ⋯⟩) =
    if w : p x✝.val = true then some ⟨x✝.val, ⋯⟩ else none

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ (filter p l).attach = filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Tactic:
rw [attach_congr (congrFun (filterMap_eq_filter _).symm _), attach_filterMap, map_filterMap]

Result:
α : Type u_1
l : List α
p : α → Bool
⊢ filterMap
      (fun x =>
        Option.map (fun x => ⟨x.val, ⋯⟩)
          (match x with
          | ⟨x, h⟩ => (Option.guard (fun x => p x = true) x).pbind fun b m => some ⟨b, ⋯⟩))
      l.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Proof state:
case e_f.h
α : Type u_1
l : List α
p : α → Bool
x✝ : { x // x ∈ l }
⊢ Option.map (fun x => ⟨x.val, ⋯⟩) ((if p x✝.val = true then some x✝.val else none).pbind fun b m => some ⟨b, ⋯⟩) =
    if w : p x✝.val = true then some ⟨x✝.val, ⋯⟩ else none

Tactic:
split <;> simp

Result:
no goals