harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem CPolynomialOn.iterated_deriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
    CPolynomialOn 𝕜 (deriv^[n] f) s

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (deriv^[0] f) s

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
⊢ CPolynomialOn 𝕜 (deriv^[n] f) s

Tactic:
induction n with
| zero => exact h
| succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (deriv^[n] f) s
⊢ CPolynomialOn 𝕜 (deriv^[n + 1] f) s

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem partialProd_succ (f : Fin n → α) (j : Fin n) :
    partialProd f j.succ = partialProd f (Fin.castSucc j) * f j

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin n → α
j : Fin n
⊢ partialProd f j.succ = partialProd f j.castSucc * f j

Tactic:
simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem angle_eq_angle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) :
    ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂

Proof state:
case h.e'_2.h.e'_5
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)

Tactic:
exact (vsub_sub_vsub_cancel_left p₃ p₂ p₁).symm

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)

Tactic:
convert angle_sub_eq_angle_sub_rev_of_norm_eq h

Result:
case h.e'_2.h.e'_5
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)

case h.e'_3.h.e'_5
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Proof state:
case h.e'_3.h.e'_5
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_left p₂ p₃ p₁).symm

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂

Tactic:
rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂

Tactic:
unfold angle

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List α} {k : α}
    (h' : l.contains k = false) :
    getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k : α
h' : l.contains k = false
⊢ (insertManyIfNewUnit empty l).val.getKey! k = default

Tactic:
exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀
  contains_empty h'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem le_map_apply {f : α → β} (hf : AEMeasurable f μ) (s : Set β) : μ (f ⁻¹' s) ≤ μ.map f s :=
  calc
    μ (f ⁻¹' s) ≤ μ (f ⁻¹' toMeasurable (μ.map f) s)

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ s ⊆ toMeasurable (map f μ) s

Tactic:
apply subset_toMeasurable

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ μ (f ⁻¹' s) ≤ μ (f ⁻¹' toMeasurable (map f μ) s)

Tactic:
gcongr

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ s ⊆ toMeasurable (map f μ) s
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem image_eq_target_inter_inv_preimage {s : Set α} (h : s ⊆ e.source) :
    e '' s = e.target ∩ e.symm ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem MonotoneOn.integral_le_sum_Ico (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) :
    (∫ x in a..b, f x) ≤ ∑ i ∈ Finset.Ico a b, f (i + 1 : ℕ)

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico a b, -f ↑(x + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, -f x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico a b, -f ↑(x + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, -f x

Tactic:
exact hf.neg.sum_le_integral_Ico hab

Result:
no goals
-- Mathlib/Topology/Constructible.lean
lemma IsRetrocompact.finsetSup' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup' hs t)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
exact .finsetSup ht

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup' hs t)

Tactic:
rw [Finset.sup'_eq_sup]

Result:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_nil_iff [LawfulBEq α] {xs : List α} {a : α} :
    xs.erase a = [] ↔ xs = [] ∨ xs = [a]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ xs.erase a = [] ↔ xs = [] ∨ xs = [a]

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ eraseP (fun x => a == x) xs = [] ↔ xs = [] ∨ xs = [a]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
a : α
⊢ eraseP (fun x => a == x) xs = [] ↔ xs = [] ∨ xs = [a]

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_mul_param_pow_iff (hk : Tendsto k l atTop) (n : ℕ) :
    SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_one : conjneg (1 : G → R) = 1

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 1 x✝ = 1 x✝

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ conjneg 1 = 1

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 1 x✝ = 1 x✝
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_const (r : R) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => r, continuous_toFun := ⋯ } =
    (cfcHom ha) ((algebraMap R C(↑(spectrum R a), R)) r)

Tactic:
congr

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => r) a = (algebraMap R A) r

Tactic:
rw [cfc_apply (fun _ : R ↦ r) a, ← AlgHomClass.commutes (cfcHom ha (p := p)) r]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => r, continuous_toFun := ⋯ } =
    (cfcHom ha) ((algebraMap R C(↑(spectrum R a), R)) r)
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_right_Ioo (a b c : α) :
    (Ioo a b).map (addRightEmbedding c) = Ioo (a + c) (b + c)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ioo _ _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_le_pow_iff_dvd (r : R) (n : ℕ) :
    v.intValuationDef r ≤ Multiplicative.ofAdd (-(n : ℤ)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ (if r = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))) ≤
      ↑(ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
split_ifs with hr

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ 0 ≤ ↑(ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))) ≤ ↑(ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))) ≤ ↑(ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
rw [WithZero.coe_le_coe, ofAdd_le, neg_le_neg_iff, Int.ofNat_le, Ideal.dvd_span_singleton, ←
  Associates.le_singleton_iff,
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr)
    (by apply v.associates_irreducible)]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.intValuationDef r ≤ ↑(ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
rw [intValuationDef]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ (if r = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))) ≤
      ↑(ofAdd (-↑n)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ 0 ≤ ↑(ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
simp_rw [hr, Ideal.dvd_span_singleton, zero_le', Submodule.zero_mem]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_emetric_ball (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
    h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r

Tactic:
rw [← h.isometry.preimage_emetric_ball (h.symm x) r, h.apply_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma IsBlock.disjoint_smul_right (hB : IsBlock M B) (hs : ¬ B ⊆ s • B) : Disjoint B (s • B)

Proof state:
M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ ¬1 • B ⊆ s • B

Tactic:
simpa using hs

Result:
no goals

Proof state:
M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint B (s • B)

Tactic:
simpa using hB.disjoint_smul_set_smul (g := 1) (by simpa using hs)

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem existsUnique_const {b : Prop} (α : Sort*) [i : Nonempty α] [Subsingleton α] :
    (∃! _ : α, b) ↔ b

Proof state:
b : Prop
α : Sort u_2
i : Nonempty α
inst✝ : Subsingleton α
⊢ (∃! x, b) ↔ b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem AddMonoidHom.toIntLinearMap_injective [AddCommGroup M] [AddCommGroup M₂] :
    Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _)

Proof state:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
⊢ Injective toIntLinearMap

Tactic:
intro f g h

Result:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
⊢ f = g

Proof state:
case h
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

Result:
no goals

Proof state:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
⊢ f = g

Tactic:
ext x

Result:
case h
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
x : M
⊢ f x = g x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0

Proof state:
i : Nat
xs : IntList
h : List.length xs ≤ i
⊢ none.getD 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
i : Nat
xs : IntList
h : List.length xs ≤ i
⊢ xs.get i = 0

Tactic:
rw [get, List.get?_eq_none_iff.mpr h]

Result:
i : Nat
xs : IntList
h : List.length xs ≤ i
⊢ none.getD 0 = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem shiftLeft_mod_two_eq_one : x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1

Proof state:
x i : Nat
⊢ x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1

Tactic:
rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]

Result:
x i : Nat
⊢ (decide (0 ≥ i) && x.testBit (0 - i)) = true ↔ i = 0 ∧ x % 2 = 1

Proof state:
x i : Nat
⊢ (decide (0 ≥ i) && x.testBit (0 - i)) = true ↔ i = 0 ∧ x % 2 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem finite_of_finite_preimage (h : (f ⁻¹' s).Finite) (hs : s ⊆ range f) : s.Finite

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' (f ⁻¹' s)).Finite

Tactic:
exact Finite.image f h

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite

Tactic:
rw [← image_preimage_eq_of_subset hs]

Result:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' (f ⁻¹' s)).Finite
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive zsmul_add] lemma mul_zpow : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
  | (n : ℕ) => by simp_rw [zpow_natCast, mul_pow]
  | .negSucc n => by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
simp_rw [zpow_natCast, mul_pow]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilter_converges_iff {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α} :
    ↑u ≤ 𝓝 x ↔ x = joinM u

Proof state:
case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ s ∈ x, {v | s ∈ v} ∈ u) → ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u

Tactic:
rintro h a ⟨xi, a, rfl⟩

Result:
case mpr.intro.intro
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ s ∈ x, {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s => {u | s ∈ u}) a
⊢ (fun s => {u | s ∈ u}) a ∈ ↑u

Proof state:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) → ∀ s ∈ x, {v | s ∈ v} ∈ u

Tactic:
intro h a ha

Result:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u

Proof state:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u

Tactic:
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff,
  mem_setOf_eq]

Result:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u

Proof state:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u

Tactic:
exact h _ ⟨ha, a, rfl⟩

Result:
no goals

Proof state:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u

Tactic:
constructor

Result:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) → ∀ s ∈ x, {v | s ∈ v} ∈ u

case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ s ∈ x, {v | s ∈ v} ∈ u) → ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u

Proof state:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u

Tactic:
rw [eq_comm, ← Ultrafilter.coe_le_coe]

Result:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x

Proof state:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x

Tactic:
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, { v : Ultrafilter α | s ∈ v } ∈ u

Result:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u

Proof state:
case mpr.intro.intro
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ s ∈ x, {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s => {u | s ∈ u}) a
⊢ (fun s => {u | s ∈ u}) a ∈ ↑u

Tactic:
exact h _ xi

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
  | ⟨f, al⟩ => by
    unfold cons destruct Functor.map
    apply congr_arg fun s => some (a, s)
    apply Subtype.eq; dsimp [tail]

Proof state:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ instFunctorOption.1 (fun a' => (a', tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩)) (get? ⟨some a :: ↑⟨f, al⟩, ⋯⟩ 0) =
    some (a, ⟨f, al⟩)

Tactic:
apply congr_arg fun s => some (a, s)

Result:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩ = ⟨f, al⟩

Proof state:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩ = ⟨f, al⟩

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ ↑(tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩) = ↑⟨f, al⟩

Proof state:
case a
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ ↑(tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩) = ↑⟨f, al⟩

Tactic:
dsimp [tail]

Result:
no goals

Proof state:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ (cons a ⟨f, al⟩).destruct = some (a, ⟨f, al⟩)

Tactic:
unfold cons destruct Functor.map

Result:
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ instFunctorOption.1 (fun a' => (a', tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩)) (get? ⟨some a :: ↑⟨f, al⟩, ⋯⟩ 0) =
    some (a, ⟨f, al⟩)