harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_image_subset (t : τ) (ht : Tendsto (· + t) f f) :
    ω f ϕ (ϕ t '' s) ⊆ ω f ϕ s

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s

Tactic:
exact omegaLimit_subset_of_tendsto ϕ s ht

Result:
no goals

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f ϕ.toFun (ϕ.toFun t '' s) ⊆ ω f ϕ.toFun s

Tactic:
simp only [omegaLimit_image_eq, ← map_add]

Result:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_lt_top_of_isCompact_of_isMulLeftInvariant (U : Set G) (hU : IsOpen U)
    (h'U : U.Nonempty) (h : μ U ≠ ∞) {K : Set G} (hK : IsCompact K) : μ K < ∞

Proof state:
case intro
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : (interior U).Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' U
⊢ μ K < ⊤

Tactic:
exact (measure_mono hKt).trans_lt <| measure_biUnion_lt_top t.finite_toSet <| by simp [h.lt_top]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : (interior U).Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' U
⊢ ∀ i ∈ Membership.mem t.val, μ ((fun h => i * h) ⁻¹' U) < ⊤

Tactic:
simp [h.lt_top]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : U.Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ μ K < ⊤

Tactic:
rw [← hU.interior_eq] at h'U

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : (interior U).Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ μ K < ⊤

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : (interior U).Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ μ K < ⊤

Tactic:
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (fun h : G => g * h) ⁻¹' U :=
  compact_covered_by_mul_left_translates hK h'U

Result:
case intro
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen U
h'U : (interior U).Nonempty
h : μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' U
⊢ μ K < ⊤
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.linearCombination_surjective :
    Function.Surjective (Finsupp.linearCombination S (KaehlerDifferential.D R S))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Surjective ⇑(linearCombination S ⇑(D R S))

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x = r) ↔ ∀ φ : K →+* ℂ, ‖φ x‖ = r :=
  ⟨fun hw φ => hw (mk φ), by rintro hφ ⟨w, ⟨φ, rfl⟩⟩; exact hφ φ⟩

Proof state:
case mk.intro
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ = r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x = r

Tactic:
exact hφ φ

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖φ x‖ = r) → ∀ (w : InfinitePlace K), w x = r

Tactic:
rintro hφ ⟨w, ⟨φ, rfl⟩⟩

Result:
case mk.intro
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ = r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x = r
-- Mathlib/GroupTheory/Nilpotent.lean
lemma isNilpotent_congr {H : Type*} [Group H] (e : G ≃* H) : IsNilpotent G ↔ IsNilpotent H

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ (∃ n, upperCentralSeries G n = ⊤) ↔ ∃ n, upperCentralSeries H n = ⊤

Tactic:
refine exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ upperCentralSeries H n = ⊤

case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries H n = ⊤
⊢ upperCentralSeries G n = ⊤

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries H n = ⊤
⊢ upperCentralSeries G n = ⊤

Tactic:
simp [← Subgroup.comap_top e.toMonoidHom, ← h]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H

Tactic:
simp_rw [isNilpotent_iff]

Result:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ (∃ n, upperCentralSeries G n = ⊤) ↔ ∃ n, upperCentralSeries H n = ⊤

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ upperCentralSeries H n = ⊤

Tactic:
simp [← Subgroup.comap_top e.symm.toMonoidHom, ← h]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Surjective.lean
theorem surjective_stableUnderComposition : StableUnderComposition surjective

Proof state:
⊢ StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f

Tactic:
introv R hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(g.comp f)

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(g.comp f)

Tactic:
exact hg.comp hf

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem fiber_subset_ofLE {A B : DiscreteQuotient X} (h : A ≤ B) (a : A) :
    A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}

Tactic:
rcases A.proj_surjective a with ⟨a, rfl⟩

Result:
case intro
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}

Proof state:
case intro
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (A.toSetoid a) ⊆ setOf (B.toSetoid a)

Tactic:
exact fun _ h' => h h'

Result:
no goals

Proof state:
case intro
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ A.proj ⁻¹' {A.proj a} ⊆ B.proj ⁻¹' {ofLE h (A.proj a)}

Tactic:
rw [fiber_eq, ofLE_proj, fiber_eq]

Result:
case intro
X : Type u_2
inst✝ : TopologicalSpace X
A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (A.toSetoid a) ⊆ setOf (B.toSetoid a)
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add_eq_of_lt_left (h : v y < v x) : v (x + y) = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (y + x) = v x

Tactic:
exact map_add_eq_of_lt_right _ h

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (x + y) = v x

Tactic:
rw [add_comm]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (y + x) = v x
-- Mathlib/Data/List/Basic.lean
theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (by simp) = a

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
a : α
l : List α
⊢ l.concat a ≠ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
⊢ (l.concat a).getLast ⋯ = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_add_int (x : α) (y : ℤ) : round (x + y) = round x + y

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = round x + y

Tactic:
rw [round, round, Int.fract_add_int, Int.floor_add_int, Int.ceil_add_int, ← apply_ite₂, ite_self]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformly.tendstoUniformlyOnFilter (h : TendstoUniformly F f p) :
    TendstoUniformlyOnFilter F f p ⊤

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
⊢ TendstoUniformlyOnFilter F f p ⊤

Tactic:
rwa [← tendstoUniformly_iff_tendstoUniformlyOnFilter]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ℕ → ℂ} {m : ℝ}
    (h : ∀ n ≠ 0, ‖f n‖ ≤ m) {s : ℂ} (hs : 1 < s.re) :
    LSeriesSummable f s :=
  LSeriesSummable_of_le_const_mul_rpow hs ⟨m, fun n hn ↦ by simp [h n hn]⟩

Proof state:
f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖f n‖ ≤ m * ↑n ^ (1 - 1)

Tactic:
simp [h n hn]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_one [DecidableEq n] [Semiring α] [StarRing α] : (1 : Matrix n n α)ᴴ = 1

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
⊢ 1ᴴ = 1

Tactic:
simp [conjTranspose]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem has_iff_has_add_complement (assignment : Assignment) (b : Bool) :
    hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment)

Proof state:
assignment : Assignment
b : Bool
⊢ hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true

Tactic:
by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_addNeg, hasNeg_addPos]

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} [TopologicalSpace δ₁]
    [TopologicalSpace δ₂] (φ₁ : C(δ₁, α)) (φ₂ : C(δ₂, α)) (h_proper₁ : IsProperMap φ₁)
    (h_proper₂ : IsProperMap φ₂) (h_cover : range φ₁ ∪ range φ₂ = univ) :
    (inferInstanceAs <| UniformSpace C(α, β)) =
      .comap (comp · φ₁) inferInstance ⊓
      .comap (comp · φ₂) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
⊢ inferInstanceAs (UniformSpace C(α, β)) =
    UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance

Tactic:
set 𝔗₂ : Set (Set δ₂) := {K | IsCompact K}

Result:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
⊢ inferInstanceAs (UniformSpace C(α, β)) =
    UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_preimage_eq_opensRange_inter (U : Y.Opens) : f ''ᵁ f ⁻¹ᵁ U = f.opensRange ⊓ U

Proof state:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : Y.Opens
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑(f.opensRange ⊓ U)

Tactic:
simp [Set.image_preimage_eq_range_inter]

Result:
no goals

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : Y.Opens
⊢ f ''ᵁ f ⁻¹ᵁ U = f.opensRange ⊓ U

Tactic:
apply Opens.ext

Result:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : Y.Opens
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑(f.opensRange ⊓ U)
-- Mathlib/Data/Vector3.lean
theorem exists_vector_zero (f : Vector3 α 0 → Prop) : Exists f ↔ f [] :=
  ⟨fun ⟨v, fv⟩ => by rw [← eq_nil v]; exact fv, fun f0 => ⟨[], f0⟩⟩

Proof state:
α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f []

Tactic:
rw [← eq_nil v]

Result:
α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Proof state:
α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Tactic:
exact fv

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_sub {R : Type u} [Ring R] {a b} : (⟨a - b⟩ : R[X]) = ⟨a⟩ - ⟨b⟩

Proof state:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]

Result:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma sum_map_mul_left : sum (s.map fun i ↦ a * f i) = a * sum (s.map f) :=
  Multiset.induction_on s (by simp) fun i s ih => by simp [ih, mul_add]

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
a : α
s✝ : Multiset ι
f : ι → α
i : ι
s : Multiset ι
ih : (map (fun i => a * f i) s).sum = a * (map f s).sum
⊢ (map (fun i => a * f i) (i ::ₘ s)).sum = a * (map f (i ::ₘ s)).sum

Tactic:
simp [ih, mul_add]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
a : α
s : Multiset ι
f : ι → α
⊢ (map (fun i => a * f i) 0).sum = a * (map f 0).sum

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem image (h : IsGenericPoint x S) {f : α → β} (hf : Continuous f) :
    IsGenericPoint (f x) (closure (f '' S))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem diam_cthickening_le {α : Type*} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) :
    diam (cthickening ε s) ≤ diam s + 2 * ε

Proof state:
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (cthickening ε s) ≤ diam s + 2 * ε

Tactic:
lift ε to ℝ≥0 using hε

Result:
case intro
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε

Proof state:
case intro.refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

Tactic:
simp [mul_eq_top]

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε

Tactic:
refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_

Result:
case intro.refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

case intro.refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

case intro.refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (EMetric.diam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Proof state:
case intro.refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

Tactic:
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (self_subset_cthickening _)

Result:
no goals

Proof state:
case intro.refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (EMetric.diam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
simp [diam]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
@[simp]
lemma dualBasis_dualBasis_flip [FiniteDimensional K V]
    (B : BilinForm K V) (hB : B.Nondegenerate) {ι : Type*}
    [Finite ι] [DecidableEq ι] (b : Basis ι K V) :
    B.dualBasis hB (B.flip.dualBasis hB.flip b) = b

Proof state:
case a
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
ι : Type u_10
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K V
i : ι
⊢ (B.dualBasis hB (B.flip.dualBasis ⋯ b)) i = b i

Tactic:
refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))

Result:
case a
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
ι : Type u_10
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K V
i j : ι
⊢ (B ((B.dualBasis hB (B.flip.dualBasis ⋯ b)) i)) ((B.flip.dualBasis ⋯ b) j) = (B (b i)) ((B.flip.dualBasis ⋯ b) j)

Proof state:
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
ι : Type u_10
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K V
⊢ B.dualBasis hB (B.flip.dualBasis ⋯ b) = b

Tactic:
ext i

Result:
case a
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
ι : Type u_10
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K V
i : ι
⊢ (B.dualBasis hB (B.flip.dualBasis ⋯ b)) i = b i

Proof state:
case a
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
ι : Type u_10
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K V
i j : ι
⊢ (B ((B.dualBasis hB (B.flip.dualBasis ⋯ b)) i)) ((B.flip.dualBasis ⋯ b) j) = (B (b i)) ((B.flip.dualBasis ⋯ b) j)

Tactic:
simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mul_one_div_le_one {I : Submodule R A} : I * (1 / I) ≤ 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ n * m ∈ 1

Tactic:
exact hn m hm

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ ∀ m ∈ I, ∀ n ∈ 1 / I, m * n ∈ 1

Tactic:
intro m hm n hn

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ m * n ∈ 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ m * n ∈ 1

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ n * m ∈ 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I * (1 / I) ≤ 1

Tactic:
rw [Submodule.mul_le]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ ∀ m ∈ I, ∀ n ∈ 1 / I, m * n ∈ 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ m * n ∈ 1

Tactic:
rw [Submodule.mem_div_iff_forall_mul_mem] at hn

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ m * n ∈ 1
-- Mathlib/RingTheory/WittVector/Teichmuller.lean
theorem map_teichmullerFun (f : R →+* S) (r : R) :
    map f (teichmullerFun p r) = teichmullerFun p (f r)

Proof state:
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff n = (teichmullerFun p (f r)).coeff n

Tactic:
cases n

Result:
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ((map f) (teichmullerFun p r)).coeff 0 = (teichmullerFun p (f r)).coeff 0

case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff (n✝ + 1) = (teichmullerFun p (f r)).coeff (n✝ + 1)

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ (map f) (teichmullerFun p r) = teichmullerFun p (f r)

Tactic:
ext n

Result:
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff n = (teichmullerFun p (f r)).coeff n

Proof state:
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ((map f) (teichmullerFun p r)).coeff 0 = (teichmullerFun p (f r)).coeff 0

Tactic:
rfl

Result:
no goals

Proof state:
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff (n✝ + 1) = (teichmullerFun p (f r)).coeff (n✝ + 1)

Tactic:
exact f.map_zero

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp] lemma sq_le_one_iff_abs_le_one (a : α) : a ^ 2 ≤ 1 ↔ |a| ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ a ^ 2 ≤ 1 ↔ |a| ≤ 1

Tactic:
simpa only [one_pow, abs_one] using @sq_le_sq _ _ a 1

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem isClosed_range_of_spaced_out {ι} [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α)
    {f : ι → α} (hf : Pairwise fun x y => (f x, f y) ∉ V₀) : IsClosed (range f) :=
  isClosed_of_spaced_out V₀_in <| by
    rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
    exact hf (ne_of_apply_ne f h)

Proof state:
case intro.intro
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => (f x, f y) ∉ V₀
x y : ι
h : f x ≠ f y
⊢ (f x, f y) ∉ V₀

Tactic:
exact hf (ne_of_apply_ne f h)

Result:
no goals

Proof state:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => (f x, f y) ∉ V₀
⊢ (range f).Pairwise fun x y => (x, y) ∉ V₀

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h

Result:
case intro.intro
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => (f x, f y) ∉ V₀
x y : ι
h : f x ≠ f y
⊢ (f x, f y) ∉ V₀