harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/UpperLower.lean
theorem Set.OrdConnected.smul (hs : s.OrdConnected) : (a • s).OrdConnected

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s)).OrdConnected

Tactic:
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • s).OrdConnected

Tactic:
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s)).OrdConnected
-- Mathlib/Order/DirectedInverseSystem.lean
theorem piLTLim_symm_apply {f} (k : Iio i) {l : Iio i} (hl : l.1 < k.1) :
    (piLTLim (X := X) hi).symm f l = f.1 k ⟨l, hl⟩

Proof state:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑f k ⟨↑l, hl⟩

Tactic:
conv_rhs => rw [← (piLTLim hi).right_inv f]

Result:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩

Proof state:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transAssocReparamAux_one : transAssocReparamAux 1 = 1

Proof state:
⊢ transAssocReparamAux 1 = 1

Tactic:
norm_num [transAssocReparamAux]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem inv_ae : (ae μ)⁻¹ = ae μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ ae μ ≤ (ae μ)⁻¹

Tactic:
nth_rewrite 1 [← inv_inv (ae μ)]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹ = ae μ

Tactic:
refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ ae μ ≤ (ae μ)⁻¹

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹

Tactic:
exact Filter.map_mono (quasiMeasurePreserving_inv μ).tendsto_ae

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_mkRat_of_ne_zero (a : ℤ) {b : ℕ} (hb : (b : α) ≠ 0) : (mkRat a b : α) = a / b

Proof state:
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(mkRat a b) = ↑a / ↑b

Tactic:
rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]

Result:
case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0

Proof state:
case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0

Tactic:
rwa [Int.cast_natCast]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
lemma mdifferentiableAt_iff {f : ℍ → ℂ} {τ : ℍ} :
    MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f τ ↔ DifferentiableAt ℂ (f ∘ ofComplex) ↑τ

Proof state:
f : ℍ → ℂ
τ : ℍ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ ↔ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Result:
case refine_1
f : ℍ → ℂ
τ : ℍ
hf : MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ

case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ

Proof state:
case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ

Tactic:
simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (mdifferentiable_coe τ)

Result:
no goals

Proof state:
case refine_1
f : ℍ → ℂ
τ : ℍ
hf : MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ

Tactic:
exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)

Result:
no goals

Proof state:
f : ℍ → ℂ
τ : ℍ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

Tactic:
rw [← mdifferentiableAt_iff_differentiableAt]

Result:
f : ℍ → ℂ
τ : ℍ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f τ ↔ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (f ∘ ↑ofComplex) ↑τ
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_two_mul : cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Proof state:
x : ℂ
⊢ cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Tactic:
rw [two_mul, cosh_add, sq, sq]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem piMap_image_univ_pi (f : ∀ i, α i → β i) (t : ∀ i, Set (α i)) :
    Pi.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i :=
  piMap_image_pi (by simp) t

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
t : (i : ι) → Set (α i)
⊢ ∀ i ∉ univ, Surjective (f i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
    m.getKeyD a fallback = (m.getKey? a).getD fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ m.getKeyD a fallback = (m.getKey? a).getD fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_eq_getD_getKey?

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then some i else none

Proof state:
n i : Nat
⊢ (range n)[i]? = if i < n then some i else none

Tactic:
simp [getElem?_def, getElem_range]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_sub_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
    term (f - g) s n = term f s n - term g s n

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f - g) s n = term f s n - term g s n

Tactic:
rw [term_sub, Pi.sub_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma rootForm_apply_apply (x y : M) : P.RootForm x y =
    ∑ i, P.coroot' i x * P.coroot' i y

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x y : M
⊢ (P.RootForm x) y = ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y

Tactic:
simp [RootForm]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem isOpen_sSup_iff {s : Set α} {T : Set (TopologicalSpace α)} :
    IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen[t] s

Proof state:
α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsOpen s ↔ ∀ t ∈ T, IsOpen s

Tactic:
simp only [sSup_eq_iSup, isOpen_iSup_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.affine_image (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : IsOpenMap f) :
    StrictConvex 𝕜 (f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ⇑f
⊢ StrictConvex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ∈ interior (⇑f '' s)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ∈ interior (⇑f '' s)

Tactic:
exact
  hf.image_interior_subset _
    ⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma odd_iff_imp {n : ℕ} [NeZero n] {k : Fin n} : Odd k ↔ (Even n → Odd k.val)

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ Odd k ↔ Odd n ∨ Odd ↑k

Tactic:
exact odd_iff

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ Odd k ↔ Even n → Odd ↑k

Tactic:
rw [imp_iff_not_or, Nat.not_even_iff_odd]

Result:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ Odd k ↔ Odd n ∨ Odd ↑k
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
theorem intCast_mem_zmultiples_one : ↑(k : ℤ) ∈ zmultiples (1 : R) :=
  mem_zmultiples_iff.mp ⟨k, by simp⟩

Proof state:
R : Type u_4
inst✝ : Ring R
k : ℤ
⊢ (fun x => x • 1) k = ↑k

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem one_coeff_zero : (1 : 𝕎 R).coeff 0 = 1 :=
  show (aeval _ (wittOne p 0) : R) = 1 by simp only [wittOne_zero_eq_one, map_one]

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ (aeval (Function.uncurry fun i => (![] i).coeff)) (wittOne p 0) = 1

Tactic:
simp only [wittOne_zero_eq_one, map_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_monomial_le : natTrailingDegree (monomial n a) ≤ n :=
  letI := Classical.decEq R
  if ha : a = 0 then by simp [ha] else (natTrailingDegree_monomial ha).le

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ((monomial n) a).natTrailingDegree ≤ n

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem revAtFun_invol {N i : ℕ} : revAtFun N (revAtFun N i) = i

Proof state:
case neg
N i : ℕ
h : ¬i ≤ N
⊢ i = i

Tactic:
rfl

Result:
no goals

Proof state:
case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i = i

Tactic:
exfalso

Result:
case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ False

Proof state:
case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ False

Tactic:
apply j

Result:
case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i ≤ N

Proof state:
case pos
N i : ℕ
h : i ≤ N
j : N - i ≤ N
⊢ N - (N - i) = i

Tactic:
exact tsub_tsub_cancel_of_le h

Result:
no goals

Proof state:
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i

Tactic:
split_ifs with h j

Result:
case pos
N i : ℕ
h : i ≤ N
j : N - i ≤ N
⊢ N - (N - i) = i

case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i = i

case neg
N i : ℕ
h : ¬i ≤ N
⊢ i = i

Proof state:
case neg
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i ≤ N

Tactic:
exact Nat.sub_le N i

Result:
no goals

Proof state:
N i : ℕ
⊢ revAtFun N (revAtFun N i) = i

Tactic:
unfold revAtFun

Result:
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem of_d_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) :
    P.toPoly = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ P.toPoly = 0

Tactic:
rw [of_c_eq_zero ha hb hc, hd, C_0]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
/-- See also `ENNReal.limsup_mul_le`. -/
lemma limsup_mul_le' {α : Type*} {f : Filter α} {u v : α → ℝ≥0∞}
    (h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞) (h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0) :
    limsup (u * v) f ≤ limsup u f * limsup v f

Proof state:
case h
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c

Tactic:
exact (mul_lt_mul a_x b_x).trans c_ab

Result:
no goals

Proof state:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c

Proof state:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x

Result:
case h
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilter_pure_injective : Function.Injective (pure : α → Ultrafilter α)

Proof state:
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y

Tactic:
exact (mem_singleton_iff.mp (mem_pure.mp this)).symm

Result:
no goals

Proof state:
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y

Tactic:
rw [h] at this

Result:
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y

Proof state:
α : Type u
⊢ Function.Injective pure

Tactic:
intro x y h

Result:
α : Type u
x y : α
h : pure x = pure y
⊢ x = y

Proof state:
α : Type u
x y : α
h : pure x = pure y
⊢ x = y

Tactic:
have : {x} ∈ (pure x : Ultrafilter α) := singleton_mem_pure

Result:
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y
-- Mathlib/LinearAlgebra/Pi.lean
theorem piRing_symm_apply (f : ι → M) (g : ι → R) : (piRing R M ι S).symm f g = ∑ i, g i • f i

Proof state:
R : Type u
M : Type v
ι : Type x
inst✝⁷ : Semiring R
S : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ι → M
g : ι → R
⊢ ((piRing R M ι S).symm f) g = ∑ i : ι, g i • f i

Tactic:
simp [piRing, LinearMap.lsum_apply]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) :
    ker (codRestrict p f hf) = ker f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ comap f ⊥ = ker f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ ker (codRestrict p f hf) = ker f

Tactic:
rw [ker, comap_codRestrict, Submodule.map_bot]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₂₁ : R₂ →+* R
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ comap f ⊥ = ker f
-- Mathlib/Data/Nat/Nth.lean
theorem count_eq_zero (h : ∃ n, p n) {n : ℕ} : count p n = 0 ↔ n ≤ nth p 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ count p n = 0 ↔ n ≤ nth p 0

Tactic:
rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sub_cosh : sinh x - cosh x = -exp (-x)

Proof state:
x : ℝ
⊢ sinh x - cosh x = -rexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma posPart_eq_zero_iff (a : A) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ = 0 ↔ -a = a⁻

Tactic:
nth_rw 2 [← posPart_sub_negPart a]

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ = 0 ↔ -(a⁺ - a⁻) = a⁻

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ = 0 ↔ a ≤ 0

Tactic:
rw [← negPart_eq_neg, eq_comm (b := -a)]

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ = 0 ↔ -a = a⁻

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁺ = 0 ↔ -(a⁺ - a⁻) = a⁻

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem colorable_chromaticNumber {m : ℕ} (hc : G.Colorable m) :
    G.Colorable (ENat.toNat G.chromaticNumber)

Proof state:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]

Result:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.23876)).toNat

V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
exact colorable_set_nonempty_of_colorable hc

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.23876)).toNat

Tactic:
apply Nat.find_spec

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem support_pure : (pure a).support = {a} :=
  Set.ext fun a' => by simp [mem_support_iff]

Proof state:
α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ a' ∈ {a}

Tactic:
simp [mem_support_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem pentagon_hom_inv {W X Y Z : C} :
    (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) =
      (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem _root_.ENNReal.count_const_le_le_of_tsum_le [MeasurableSingletonClass α] {a : α → ℝ≥0∞}
    (a_mble : Measurable a) {c : ℝ≥0∞} (tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0)
    (ε_ne_top : ε ≠ ∞) : Measure.count { i : α | ε ≤ a i } ≤ c / ε

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε

Tactic:
exact ENNReal.div_le_div tsum_le_c rfl.le

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
rw [← lintegral_count] at tsum_le_c

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ count {i | ε ≤ a i} ≤ c / ε
-- Mathlib/Order/Interval/Set/Image.lean
lemma AntitoneOn.mapsTo_Iic (h : AntitoneOn f (Iic b)) : MapsTo f (Iic b) (Ici (f b)) :=
  fun _ _ ↦ by aesop

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : AntitoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Ici (f b)

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem mono_inr_of_isColimit [Mono f] {s : PushoutCocone f g} (hs : IsColimit s) : Mono s.inr

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inr

Tactic:
haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) :=
  Abelian.mono_pushout_of_mono_f f g

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)
⊢ Mono s.inr

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)
⊢ Mono s.inr

Tactic:
apply
  mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

Result:
no goals