harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
theorem innerRegularWRT_isCompact [UniformSpace α] [CompleteSpace α]
    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT IsCompact IsClosed

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
exact innerRegularWRT_isCompact_closure P

Result:
no goals

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsClosed

Tactic:
rw [← innerRegularWRT_isCompact_closure_iff]

Result:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
-- Mathlib/Probability/Distributions/Gamma.lean
lemma gammaPDF_of_neg {a r x : ℝ} (hx : x < 0) : gammaPDF a r x = 0

Proof state:
a r x : ℝ
hx : x < 0
⊢ gammaPDF a r x = 0

Tactic:
simp only [gammaPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_ofReal_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
    ContinuousAt (fun a => (a : ℂ) ^ y : ℝ → ℂ) x :=
  (continuousAt_ofReal_cpow x y h).comp₂_of_eq (by fun_prop) (by fun_prop) rfl

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun a => a) x

Tactic:
fun_prop

Result:
no goals

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun a => y) x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem intNorm_coe (a : integerSet K) :
    (intNorm a : ℝ) = mixedEmbedding.norm (a : mixedSpace K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑(intNorm a) = mixedEmbedding.norm ↑a

Tactic:
rw [intNorm, Int.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
  ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_append_right' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < n) :
    l₂[i] = (l₁ ++ l₂)[i + m]

Proof state:
α : Type u_1
m n : Nat
l₁ : Vector α m
l₂ : Vector α n
i : Nat
hi : i < n
⊢ l₂[i] = (l₁ ++ l₂)[i + m]

Tactic:
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem fg_closure {s : Set M} (hs : s.Finite) : FG (closure L s) :=
  ⟨hs.toFinset, by rw [hs.coe_toFinset]⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hs : s.Finite
⊢ (closure L).toFun ↑hs.toFinset = (closure L).toFun s

Tactic:
rw [hs.coe_toFinset]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic'_two (R : Type*) [CommRing R] [IsDomain R] (p : ℕ) [CharP R p] (hp : p ≠ 2) :
    cyclotomic' 2 R = X + 1

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1

Tactic:
simp only [prim_root_two, Finset.prod_singleton, RingHom.map_neg, RingHom.map_one, sub_neg_eq_add]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ primitiveRoots 2 R = {-1}

Tactic:
simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1

Tactic:
exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ cyclotomic' 2 R = X + 1

Tactic:
rw [cyclotomic']

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1

Tactic:
have prim_root_two : primitiveRoots 2 R = {(-1 : R)} := by
  simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
  exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1
-- Mathlib/Data/Nat/Init.lean
lemma not_pos_pow_dvd : ∀ {a n : ℕ} (_ : 1 < a) (_ : 1 < n), ¬ a ^ n ∣ a
  | succ a, succ n, hp, hk, h =>
    have : succ a * succ a ^ n ∣ succ a * 1

Proof state:
a n : ℕ
hp : 1 < a.succ
hk : 1 < n.succ
h : a.succ ^ n.succ ∣ a.succ
⊢ a.succ * a.succ ^ n ∣ a.succ * 1

Tactic:
simpa [pow_succ'] using h

Result:
no goals

Proof state:
a n : ℕ
hp : 1 < a.succ
hk : 1 < n.succ
h : a.succ ^ n.succ ∣ a.succ
this✝¹ : a.succ * a.succ ^ n ∣ a.succ * 1
this✝ : a.succ ^ n ∣ 1
he : a.succ ^ n = 1
this : n < a.succ ^ n
⊢ n < 1

Tactic:
rwa [he] at this

Result:
no goals

Proof state:
a n : ℕ
hp : 1 < a.succ
hk : 1 < n.succ
h : a.succ ^ n.succ ∣ a.succ
this✝³ : a.succ * a.succ ^ n ∣ a.succ * 1
this✝² : a.succ ^ n ∣ 1
he : a.succ ^ n = 1
this✝¹ : n < a.succ ^ n
this✝ : n < 1
this : n = 0
⊢ 1 < 1

Tactic:
rwa [this] at hk

Result:
no goals

Proof state:
a n : ℕ
hp : 1 < a.succ
hk : 1 < n.succ
h : a.succ ^ n.succ ∣ a.succ
this✝⁴ : a.succ * a.succ ^ n ∣ a.succ * 1
this✝³ : a.succ ^ n ∣ 1
he : a.succ ^ n = 1
this✝² : n < a.succ ^ n
this✝¹ : n < 1
this✝ : n = 0
this : 1 < 1
⊢ ¬1 < 1

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_singleton (a : α) : dens ({a} : Finset α) = (Fintype.card α : ℚ≥0)⁻¹

Proof state:
α : Type u_2
inst✝ : Fintype α
a : α
⊢ {a}.dens = (↑(Fintype.card α))⁻¹

Tactic:
simp [dens]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ofComplex_I : ofComplex Complex.I = ι Q 1 :=
  Complex.liftAux_apply_I _ (by simp)

Proof state:
⊢ ↑⟨(ι Q) 1, ofComplex.proof_1⟩ * ↑⟨(ι Q) 1, ofComplex.proof_1⟩ = -1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem mem_uIcc' : a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
simp [uIcc_eq_union]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
/-- This lemma allows to rewrite the compostion of a measure and a kernel as the composition
of two kernels, which allows to transfer properties of `∘ₖ` to `∘ₘ`. -/
lemma comp_eq_comp_const_apply : κ ∘ₘ μ = (κ ∘ₖ (Kernel.const Unit μ)) ()

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
⊢ ⇑κ ∘ₘ μ = (κ ∘ₖ Kernel.const Unit μ) ()

Tactic:
rw [Kernel.comp_apply, Kernel.const_apply]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Card.lean
theorem card_dvd_of_injective (f : α →* H) (hf : Function.Injective f) :
    Nat.card α ∣ Nat.card H

Proof state:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
hf : Function.Injective ⇑f
⊢ Nat.card α ∣ Nat.card H

Tactic:
calc
Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
_ ∣ Nat.card H := card_subgroup_dvd_card _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
hf : Function.Injective ⇑f
⊢ Nat.card α ∣ Nat.card H

Tactic:
classical calc
    Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
    _ ∣ Nat.card H := card_subgroup_dvd_card _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_ΨSq_pos [NoZeroDivisors R] {n : ℤ} (hn : 1 < n.natAbs) (h : (n : R) ≠ 0) :
    0 < (W.ΨSq n).natDegree

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
hn : 1 < n.natAbs
h : ↑n ≠ 0
⊢ 0 < (W.ΨSq n).natDegree

Tactic:
rwa [W.natDegree_ΨSq h, Nat.sub_pos_iff_lt, Nat.one_lt_pow_iff two_ne_zero]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem periodicOrbit_apply_iterate_eq (hx : x ∈ periodicPts f) (n : ℕ) :
    periodicOrbit f (f^[n] x) = periodicOrbit f x :=
  Eq.symm <| Cycle.coe_eq_coe.2 <| .intro n <|
    List.ext_get (by simp [minimalPeriod_apply_iterate hx]) fun m _ _ ↦ by
      simp [List.getElem_rotate, iterate_add_apply]

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n m : ℕ
x✝¹ : m < ((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).length
x✝ : m < (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).length
⊢ ((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).get ⟨m, x✝¹⟩ =
    (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).get ⟨m, x✝⟩

Tactic:
simp [List.getElem_rotate, iterate_add_apply]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ ((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).length =
    (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).length

Tactic:
simp [minimalPeriod_apply_iterate hx]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem eq_zero_of_squarefree_of_dvd_eq_zero [CommMonoidWithZero R] {f : ArithmeticFunction R}
    (hf : IsMultiplicative f) {m n : ℕ} (hn : Squarefree n) (hmn : m ∣ n)
    (h_zero : f m = 0) :
    f n = 0

Proof state:
case intro
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
hn : Squarefree (m * k)
⊢ f (m * k) = 0

Tactic:
simp only [MulZeroClass.zero_mul, eq_self_iff_true, hf.map_mul_of_coprime
  (coprime_of_squarefree_mul hn), h_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0

Tactic:
rcases hmn with ⟨k, rfl⟩

Result:
case intro
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
hn : Squarefree (m * k)
⊢ f (m * k) = 0
-- Mathlib/Topology/Bornology/Basic.lean
theorem cobounded_eq_bot_iff : cobounded α = ⊥ ↔ BoundedSpace α

Proof state:
α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma MonoidHomClass.isMulFreimanHom [FunLike F α β] [MonoidHomClass F α β] (f : F)
    (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f where
  mapsTo := hfAB
  map_prod_eq_map_prod s t _ _ _ _ h

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
x✝¹ : s.card = n
x✝ : t.card = n
h : s.prod = t.prod
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod

Tactic:
rw [← map_multiset_prod, h, map_multiset_prod]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_smul_ball (c : G) (x : X) (r : ℝ≥0∞) :
    (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r

Proof state:
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_ball]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem lor_bit (a m b n) : lor (bit a m) (bit b n) = bit (a || b) (lor m n)

Proof state:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).lor (bit b n) = bit (a || b) (m.lor n)

Tactic:
rw [← bitwise_or, bitwise_bit]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldr_eq_foldr (f : (i : Fin n) → α → α) (x) :
    dfoldr n (fun _ => α) f x = foldr n f x

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), dfoldr n (fun x => α) f x = foldr n f x
f : Fin (n + 1) → α → α
x : α
⊢ dfoldr (n + 1) (fun x => α) f x = foldr (n + 1) f x

Tactic:
simp only [dfoldr_succ, foldr_succ, Function.comp_def, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
f : Fin 0 → α → α
x : α
⊢ dfoldr 0 (fun x => α) f x = foldr 0 f x

Tactic:
simp only [dfoldr_zero, foldr_zero]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α → α
x : (fun x => α) (last n)
⊢ dfoldr n (fun x => α) f x = foldr n f x

Tactic:
induction n with
| zero => simp only [dfoldr_zero, foldr_zero]
| succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_def, ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_map (l : Vector α n) (k : Nat) (f : α → β) :
    zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id)

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
k : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).zipIdx k =
    map (Prod.map f id) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k)

Tactic:
simp [Array.zipIdx_map]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
k : Nat
f : α → β
⊢ (map f l).zipIdx k = map (Prod.map f id) (l.zipIdx k)

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
k : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).zipIdx k =
    map (Prod.map f id) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
    a ∈ v.setIfInBounds i a

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ (v.setIfInBounds i a)[i] = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ a ∈ v.setIfInBounds i a

Tactic:
simp [mem_iff_getElem]

Result:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ ∃ i_1 h, (v.setIfInBounds i a)[i_1] = a

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ i < n

Tactic:
simpa using hi

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ ∃ i_1 h, (v.setIfInBounds i a)[i_1] = a

Tactic:
exact ⟨i, (by simpa using hi), by simp⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} :
    ⟦aig.mkAndCached input, assign⟧
      =
    (⟦aig, input.lhs, assign⟧
      &&
    ⟦aig, input.rhs, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkAndCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
simp [mkAndCached]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_union (a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a

Tactic:
delta nhdsWithin

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t

Tactic:
rw [← inf_sup_left, sup_principal]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank [FiniteDimensional K V]
    [FiniteDimensional K V₂] (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} :
    LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
⊢ ker f = ⊥ ↔ range f = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem Option.admissible_eq_some (P : Prop) (y : α) :
    admissible (fun (x : Option α) => x = some y → P)

Proof state:
α : Type u_1
P : Prop
y : α
⊢ admissible fun x => x = some y → P

Tactic:
apply admissible_flatOrder

Result:
case hnot
α : Type u_1
P : Prop
y : α
⊢ none = some y → P

Proof state:
case hnot
α : Type u_1
P : Prop
y : α
⊢ none = some y → P

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem summable_measure_toReal [hμ : IsFiniteMeasure μ] {f : ℕ → Set α}
    (hf₁ : ∀ i : ℕ, MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
    Summable fun x => (μ (f x)).toReal

Proof state:
case hsum
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ μ (⋃ i, f i) ≠ ⊤

Tactic:
exact ne_of_lt (measure_lt_top _ _)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Summable fun x => (μ (f x)).toReal

Tactic:
apply ENNReal.summable_toReal

Result:
case hsum
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∑' (x : ℕ), μ (f x) ≠ ⊤

Proof state:
case hsum
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∑' (x : ℕ), μ (f x) ≠ ⊤

Tactic:
rw [← MeasureTheory.measure_iUnion hf₂ hf₁]

Result:
case hsum
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ μ (⋃ i, f i) ≠ ⊤
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem card_interedges_finpartition_left [DecidableEq α] (P : Finpartition s) (t : Finset β) :
    #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(P.parts.biUnion fun a => interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
rw [card_biUnion]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ ∀ x ∈ P.parts, ∀ y ∈ P.parts, x ≠ y → Disjoint (interedges r x t) (interedges r y t)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(P.parts.biUnion fun a => interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ ∀ x ∈ P.parts, ∀ y ∈ P.parts, x ≠ y → Disjoint (interedges r x t) (interedges r y t)

Tactic:
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

Result:
no goals
-- Mathlib/CategoryTheory/UnivLE.lean
theorem UnivLE.ofEssSurj (w : (uliftFunctor.{u, v} : Type v ⥤ Type max u v).EssSurj) :
    UnivLE.{max u v, v} :=
  fun α ↦ by
    obtain ⟨a', ⟨m⟩⟩ := w.mem_essImage α
    exact ⟨a', ⟨(Iso.toEquiv m).symm.trans Equiv.ulift⟩⟩

Proof state:
case intro.intro
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : uliftFunctor.{u, v}.obj a' ≅ α
⊢ Small.{v, max u v} α

Tactic:
exact ⟨a', ⟨(Iso.toEquiv m).symm.trans Equiv.ulift⟩⟩

Result:
no goals

Proof state:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
⊢ Small.{v, max u v} α

Tactic:
obtain ⟨a', ⟨m⟩⟩ := w.mem_essImage α

Result:
case intro.intro
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : uliftFunctor.{u, v}.obj a' ≅ α
⊢ Small.{v, max u v} α
-- Mathlib/Algebra/GroupWithZero/Action/Basic.lean
lemma IsUnit.smul_sub_iff_sub_inv_smul [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R]
    [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) :
    IsUnit (r • (1 : R) - a) ↔ IsUnit (1 - r⁻¹ • a)

Proof state:
G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)

Tactic:
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem takeWhile_eq_take_findIdx_not {xs : List α} {p : α → Bool} :
    takeWhile p xs = take (xs.findIdx (fun a => !p a)) xs

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : takeWhile p xs = take (findIdx (fun a => !p a) xs) xs
⊢ takeWhile p (x :: xs) = take (findIdx (fun a => !p a) (x :: xs)) (x :: xs)

Tactic:
simp only [takeWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : takeWhile p xs = take (findIdx (fun a => !p a) xs) xs
⊢ (if p x = true then x :: take (findIdx (fun a => !p a) xs) xs else []) =
    take (if p x = false then 0 else findIdx (fun a => !p a) xs + 1) (x :: xs)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ takeWhile p xs = take (findIdx (fun a => !p a) xs) xs

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [takeWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : takeWhile p xs = take (findIdx (fun a => !p a) xs) xs
⊢ (if p x = true then x :: take (findIdx (fun a => !p a) xs) xs else []) =
    take (if p x = false then 0 else findIdx (fun a => !p a) xs + 1) (x :: xs)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ takeWhile p [] = take (findIdx (fun a => !p a) []) []

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_apply_eq [Zero α] (d : n → α) (i : n) : (diagonal d) i i = d i

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i : n
⊢ diagonal d i i = d i

Tactic:
simp [diagonal]

Result:
no goals