harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem periodicOrbit_chain' (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) :
    (periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n + 1] x)

Proof state:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
  ← iterate_succ_apply, minimalPeriod_apply hx]

Result:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)

Proof state:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
refine ⟨fun H n => ?_, fun H n _ => H n⟩

Result:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)

Proof state:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit_chain r]

Result:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Proof state:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)

Tactic:
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_union_le (s t : Finset α) :
    mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t :=
  let ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s ∪ t)
  calc
    mulRothNumber (s ∪ t) = #u := hcard.symm
    _ = #(u ∩ s ∪ u ∩ t)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : #u = mulRothNumber (s ∪ t)
hu : ThreeGPFree ↑u
⊢ #u = #(u ∩ s ∪ u ∩ t)

Tactic:
rw [← inter_union_distrib_left, inter_eq_left.2 hus]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X : C) ≅ A)
    (w : i.hom ≫ f = X.arrow) : X = mk f :=
  eq_of_comm (i.trans (underlyingIso f).symm) <| by simp [w]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : underlying.obj X ≅ A
w : i.hom ≫ f = X.arrow
⊢ (i ≪≫ (underlyingIso f).symm).hom ≫ (mk f).arrow = X.arrow

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
lemma nthRootsFinset_def (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] [DecidableEq R] :
    nthRootsFinset n R = Multiset.toFinset (nthRoots n (1 : R))

Proof state:
n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ (nthRoots n 1).toFinset = (nthRoots n 1).toFinset

Tactic:
convert rfl

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ nthRootsFinset n R = (nthRoots n 1).toFinset

Tactic:
unfold nthRootsFinset

Result:
n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ (nthRoots n 1).toFinset = (nthRoots n 1).toFinset
-- Mathlib/Data/Set/Insert.lean
theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t

Proof state:
α : Type u
s t : Set α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
refine ⟨fun h x hx => ?_, insert_subset_insert⟩

Result:
α : Type u
s t : Set α
a : α
ha : a ∉ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
⊢ x ∈ t

Proof state:
case inl
α : Type u
s t : Set α
x : α
hx : x ∈ s
ha : x ∉ s
h : insert x s ⊆ insert x t
⊢ x ∈ t

case inr
α : Type u
s t : Set α
a : α
ha : a ∉ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ t

Tactic:
exacts [(ha hx).elim, hxt]

Result:
no goals

Proof state:
α : Type u
s t : Set α
a : α
ha : a ∉ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
⊢ x ∈ t

Tactic:
rcases h (subset_insert _ _ hx) with (rfl | hxt)

Result:
case inl
α : Type u
s t : Set α
x : α
hx : x ∈ s
ha : x ∉ s
h : insert x s ⊆ insert x t
⊢ x ∈ t

case inr
α : Type u
s t : Set α
a : α
ha : a ∉ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ t
-- Mathlib/Logic/Encodable/Lattice.lean
theorem iUnion_decode₂_disjoint_on {f : β → Set α} (hd : Pairwise (Disjoint on f)) :
    Pairwise (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
⊢ x ∈ (fun i => ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i => ⋃ b ∈ decode₂ β i, f b) j

Tactic:
simpa [decode₂_eq_some]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False

Tactic:
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b

Tactic:
rintro a rfl ha b rfl hb

Result:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b) i j

Tactic:
refine disjoint_left.mpr fun x => ?_

Result:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i => ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i => ⋃ b ∈ decode₂ β i, f b) j

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i => ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i => ⋃ b ∈ decode₂ β i, f b) j

Tactic:
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]

Result:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
⊢ Pairwise (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b)

Tactic:
rintro i j ij

Result:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b) i j
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma sinZeta_neg (a : UnitAddCircle) (s : ℂ) :
    sinZeta (-a) s = -sinZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ sinZeta (-a) s = -sinZeta a s

Tactic:
simp_rw [sinZeta, completedSinZeta_neg, neg_div]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Ne.nhdsWithin_diff_singleton [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) :
    𝓝[s \ {y}] x = 𝓝[s] x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ {y}ᶜ ∈ 𝓝[s] x

Tactic:
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ {y}ᶜ ∈ 𝓝[s] x
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem neg_normalize (n d z) : -normalize n d z = normalize (-n) d z

Proof state:
n : Int
d : Nat
z : d ≠ 0
⊢ -normalize n d z = normalize (-n) d z

Tactic:
simp [normalize]

Result:
n : Int
d : Nat
z : d ≠ 0
⊢ -{ num := n.tdiv ↑(n.natAbs.gcd d), den := d / n.natAbs.gcd d, den_nz := ⋯, reduced := ⋯ } =
    { num := -n.tdiv ↑(n.natAbs.gcd d), den := d / n.natAbs.gcd d, den_nz := ⋯, reduced := ⋯ }

Proof state:
n : Int
d : Nat
z : d ≠ 0
⊢ -{ num := n.tdiv ↑(n.natAbs.gcd d), den := d / n.natAbs.gcd d, den_nz := ⋯, reduced := ⋯ } =
    { num := -n.tdiv ↑(n.natAbs.gcd d), den := d / n.natAbs.gcd d, den_nz := ⋯, reduced := ⋯ }

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_iff'₀ {p : α → Prop} (hs : NullMeasurableSet s μ) :
    (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff, ← compl_setOf, restrict_apply₀' hs]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Proof state:
case e_a.h.e_6.h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)

Tactic:
congr with x

Result:
case e_a.h.e_6.h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Tactic:
rw [iff_iff_eq]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
-- Mathlib/Data/Matrix/Mul.lean
theorem single_one_vecMul [Fintype m] [DecidableEq m] [NonAssocSemiring R]
    (i : m) (M : Matrix m n R) :
    Pi.single i 1 ᵥ* M = M i

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M i x✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
⊢ Pi.single i 1 ᵥ* M = M i

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M i x✝
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem span_gramSchmidtNormed_range (f : ι → E) :
    span 𝕜 (range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (range (gramSchmidt 𝕜 f))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (Set.range (gramSchmidt 𝕜 f))

Tactic:
simpa only [image_univ.symm] using span_gramSchmidtNormed f univ

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem HasDerivWithinAt.inv (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) :
    HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x

Proof state:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ -c' / c x ^ 2 = -(c x ^ 2)⁻¹ * c'

Tactic:
field_simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x

Tactic:
convert (hasDerivAt_inv hx).comp_hasDerivWithinAt x hc using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ -c' / c x ^ 2 = -(c x ^ 2)⁻¹ * c'
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma exists_isNIndepSet_indepNum [Fintype α] : ∃ s, G.IsNIndepSet G.indepNum s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ ∃ s, Gᶜ.IsNClique (sSup {n | ∃ s, Gᶜ.IsNClique n s}) s

Tactic:
exact exists_isNClique_cliqueNum

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ ∃ s, G.IsNIndepSet G.indepNum s

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ ∃ s, Gᶜ.IsNClique (sSup {n | ∃ s, Gᶜ.IsNClique n s}) s
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintype_uIcc : Fintype.card (Set.uIcc a b) = (b - a : ℤ).natAbs + 1

Proof state:
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
rw [← card_uIcc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem tprod_le_one (h : ∀ i, f i ≤ 1) : ∏' i, f i ≤ 1

Proof state:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f
⊢ ∏' (i : ι), f i ≤ 1

Tactic:
exact hf.hasProd.le_one h

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ≤ 1

Tactic:
rw [tprod_eq_one_of_not_multipliable hf]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
⊢ ∏' (i : ι), f i ≤ 1

Tactic:
by_cases hf : Multipliable f

Result:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f
⊢ ∏' (i : ι), f i ≤ 1

case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ≤ 1
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem image_op_inv : op '' s⁻¹ = (op '' s)⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

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

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.ball (f x) r ↔ y ∈ EMetric.ball x r

Tactic:
simp [h.edist_eq]

Result:
no goals

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

Tactic:
ext y

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.ball (f x) r ↔ y ∈ EMetric.ball x r
-- Mathlib/Data/Sym/Sym2.lean
theorem map_comp {g : β → γ} {f : α → β} : Sym2.map (g ∘ f) = Sym2.map g ∘ Sym2.map f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = map g ∘ map f

Tactic:
ext ⟨⟨x, y⟩⟩

Result:
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ : Sym2 α
x y : α
⊢ map (g ∘ f) (Quot.mk (Rel α) (x, y)) = (map g ∘ map f) (Quot.mk (Rel α) (x, y))

Proof state:
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ : Sym2 α
x y : α
⊢ map (g ∘ f) (Quot.mk (Rel α) (x, y)) = (map g ∘ map f) (Quot.mk (Rel α) (x, y))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_extract {as : Array α} {start stop : Nat}
    (h : i < (as.extract start stop).size) :
    (as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
  show (extract.loop as (min stop as.size - start) start #[])[i]
    = as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _

Proof state:
case hge
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ i ≥ #[].size

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ (extract.loop as (min stop as.size - start) start #[])[i] = as[start + i]

Tactic:
rw [getElem_extract_loop_ge]

Result:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ as[start + i - #[].size] = as[start + i]

case hge
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ i ≥ #[].size

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ as[start + i - #[].size] = as[start + i]

case hge
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ i ≥ #[].size

Tactic:
rfl

Result:
case hge
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ i ≥ #[].size
-- Mathlib/Computability/ContextFreeGrammar.lean
/-- A given word `w` belongs to the language generated by a given context-free grammar `g` iff
`g` can derive the word `w` (wrapped as a string) from the initial nonterminal of `g` in some
number of steps. -/
@[simp]
lemma mem_language_iff (g : ContextFreeGrammar T) (w : List T) :
    w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (w.map Symbol.terminal)

Proof state:
T : Type u_1
g : ContextFreeGrammar T
w : List T
⊢ w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem unpaired {f : ℕ → ℕ →. α} : Partrec (Nat.unpaired f) ↔ Partrec₂ f :=
  ⟨fun h => by simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp,
    fun h => h.comp Primrec.unpair.to_comp⟩

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f

Tactic:
simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_eraseP_of_mem {l : Array α} (al : a ∈ l) (pa : p a) :
    (l.eraseP p).size = l.size - 1

Proof state:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
⊢ (l.eraseP p).size = l.size - 1

Tactic:
let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa

Result:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ (l.eraseP p).size = l.size - 1

Proof state:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ l₁.size + l₂.size = l₁.size + 1 + l₂.size - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ (l₁ ++ l₂).size = l.size - 1

Tactic:
simp [size_append, e₁]

Result:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ l₁.size + l₂.size = l₁.size + 1 + l₂.size - 1

Proof state:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ (l.eraseP p).size = l.size - 1

Tactic:
rw [e₂]

Result:
α : Type u_1
a : α
p : α → Bool
l : Array α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : Array α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁.push w✝ ++ l₂
e₂ : l.eraseP p = l₁ ++ l₂
⊢ (l₁ ++ l₂).size = l.size - 1
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_lapply (i : ι) :
    comul ∘ₗ (lapply i : _ →ₗ[R] A) = TensorProduct.map (lapply i) (lapply i) ∘ₗ comul

Proof state:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case h.inl
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle i = TensorProduct.map (lapply i ∘ₗ lsingle i) (lapply i ∘ₗ lsingle i) ∘ₗ comul

case h.inr
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
hij : i ≠ j
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul

Proof state:
case h.inl
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle i = TensorProduct.map (lapply i ∘ₗ lsingle i) (lapply i ∘ₗ lsingle i) ∘ₗ comul

Tactic:
rw [comp_assoc, lapply_comp_lsingle_same, comp_id,  TensorProduct.map_id, id_comp]

Result:
no goals

Proof state:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = (TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j

Tactic:
conv_rhs => rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, ← TensorProduct.map_comp]

Result:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul

Proof state:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ comul ∘ₗ lapply i = TensorProduct.map (lapply i) (lapply i) ∘ₗ comul

Tactic:
ext j : 1

Result:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = (TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j

Proof state:
case h.inr
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i j : ι
hij : i ≠ j
⊢ (comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul

Tactic:
rw [comp_assoc, lapply_comp_lsingle_of_ne _ _ hij, comp_zero, TensorProduct.map_zero_left,
  zero_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem toL1_coeFn (f : α →₁[μ] β) (hf : Integrable f μ) : hf.toL1 f = f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
hf : Integrable (↑↑f) μ
⊢ toL1 (↑↑f) hf = f

Tactic:
simp [Integrable.toL1]

Result:
no goals