harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem mem_extChartAt_source_of_eq_one {i : ι} {x : M} (h : fs i x = 1) :
    x ∈ (extChartAt I (fs.c i)).source

Proof state:
ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(fs.toFun i) x = 1
⊢ x ∈ (chartAt H (fs.c i)).source

Tactic:
exact fs.mem_chartAt_source_of_eq_one h

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(fs.toFun i) x = 1
⊢ x ∈ (extChartAt I (fs.c i)).source

Tactic:
rw [extChartAt_source]

Result:
ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(fs.toFun i) x = 1
⊢ x ∈ (chartAt H (fs.c i)).source
-- Mathlib/MeasureTheory/Covering/OneDim.lean
theorem Icc_mem_vitaliFamily_at_right {x y : ℝ} (hxy : x < y) :
    Icc x y ∈ (vitaliFamily (volume : Measure ℝ) 1).setsAt x

Proof state:
x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
rw [dist_comm, Real.dist_eq, abs_of_nonneg] <;> linarith

Result:
no goals

Proof state:
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2

Tactic:
linarith

Result:
no goals

Proof state:
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt x

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Result:
x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Proof state:
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ (vitaliFamily volume 1).setsAt x

Tactic:
rw [Icc_eq_closedBall]

Result:
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt x
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[reassoc (attr := simp)]
lemma map_ofInv_hom_id (s : Y ⟶ X) (hs : W s) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    (ofInv s hs).map L hL ≫ L.map s = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
letI := hL _ hs

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
simp [map]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanSingleton_isIdempotentElem_iff {e : R} :
    IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e

Proof state:
R : Type u_1
inst✝ : Semiring R
e : R
h : e * e = e
x✝ : R
⊢ x✝ * (e * e) = x✝ * e

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
e : R
⊢ (∀ (x : R), x * (e * e) = x * e) ↔ e * e = e

Tactic:
exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
⊢ e * e = e

Tactic:
conv_rhs => rw [← one_mul e, ← h, one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
e : R
⊢ IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e

Tactic:
simp_rw [IsIdempotentElem, LinearMap.ext_iff, mul_apply, toSpanSingleton_apply, smul_eq_mul,
  mul_assoc]

Result:
R : Type u_1
inst✝ : Semiring R
e : R
⊢ (∀ (x : R), x * (e * e) = x * e) ↔ e * e = e
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem indicator_ae_eq_zero_of_restrict_ae_eq_zero (hs : MeasurableSet s)
    (hf : f =ᵐ[μ.restrict s] 0) : s.indicator f =ᵐ[μ] 0

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
⊢ s.indicator f x = 0 x

Tactic:
by_cases hxs : x ∈ s

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = 0 x

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] 0

Tactic:
filter_upwards [hf] with x hx

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
⊢ s.indicator f x = 0 x

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = 0 x

Tactic:
simp only [hxs, hx hxs, Set.indicator_of_mem]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
⊢ s.indicator f =ᶠ[ae μ] 0

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] 0

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x

Tactic:
simp [hx, hxs]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_range_range_eq {m₁ : α → γ} {m₂ : β → δ} :
    range m₁ ×ˢ range m₂ = range fun p : α × β => (m₁ p.1, m₂ p.2) :=
  ext <| by simp [range]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ range m₁ ×ˢ range m₂ ↔ x ∈ range fun p => (m₁ p.1, m₂ p.2)

Tactic:
simp [range]

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem classes_eqv_classes {r : Setoid α} (a) : ∃! b ∈ r.classes, a ∈ b :=
  ExistsUnique.intro { x | r x a } ⟨r.mem_classes a, r.refl' _⟩ <| by
    rintro y ⟨⟨_, rfl⟩, ha⟩
    ext x
    exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩

Proof state:
case intro.intro.h
α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
x : α
⊢ x ∈ {x | r x w✝} ↔ x ∈ {x | r x a}

Tactic:
exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩

Result:
no goals

Proof state:
α : Type u_1
r : Setoid α
a : α
⊢ ∀ (y : Set α), y ∈ r.classes ∧ a ∈ y → y = {x | r x a}

Tactic:
rintro y ⟨⟨_, rfl⟩, ha⟩

Result:
case intro.intro
α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
⊢ {x | r x w✝} = {x | r x a}

Proof state:
case intro.intro
α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
⊢ {x | r x w✝} = {x | r x a}

Tactic:
ext x

Result:
case intro.intro.h
α : Type u_1
r : Setoid α
a w✝ : α
ha : a ∈ {x | r x w✝}
x : α
⊢ x ∈ {x | r x w✝} ↔ x ∈ {x | r x a}
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_eq_top : G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v

Tactic:
simp only [ediam, iSup_eq_top, lt_iSup_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
lemma mul_delta {n : ℕ} (χ : DirichletCharacter ℂ n) : ↗χ * δ = δ :=
  LSeries.mul_delta <| by rw [cast_one, map_one]

Proof state:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ χ ↑1 = 1

Tactic:
rw [cast_one, map_one]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c` -/
lemma cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m / gcd m c]

Proof state:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
apply cancel_left_div_gcd hm

Result:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Proof state:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa [mul_comm] using h

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_option' :
    LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
⊢ (LinearIndependent K fun o => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u', _} ι).symm, linearIndependent_sum,
  @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
⊢ LinearIndependent K (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ≠ 0 ∧
        ((((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ∈
            span K (range (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) →
          (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
h : LinearIndependent K v ∧ x ∉ span K (range v)
⊢ ¬x = 0

Tactic:
rintro rfl

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
⊢ LinearIndependent K (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      ¬x = 0 ∧
        (x ∈ span K (range (((fun o => o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) → x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
h : LinearIndependent K v ∧ x ∉ span K (range v)
⊢ ¬x = 0

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False

Tactic:
exact h.2 (zero_mem _)

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_image_left (f : γ → β → δ) (g : α → γ) :
    image₂ f (s.image g) t = image₂ (fun a b => f (g a) b) s t :=
  coe_injective <| by
    push_cast
    exact image2_image_left _ _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ ↑(image₂ f (image g s) t) = ↑(image₂ (fun a b => f (g a) b) s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' ↑s) ↑t = image2 (fun a b => f (g a) b) ↑s ↑t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' ↑s) ↑t = image2 (fun a b => f (g a) b) ↑s ↑t

Tactic:
exact image2_image_left _ _

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem comap_coclosedCompact (h : X ≃ₜ Y) : comap h (coclosedCompact Y) = coclosedCompact X :=
  (hasBasis_coclosedCompact.comap h).eq_of_same_basis <| by
    simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ (coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun i => ⇑h ⁻¹' iᶜ

Tactic:
simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1

Proof state:
n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_zsmul [AddGroup α] [StarAddMonoid α] (c : ℤ) (M : Matrix m n α) :
    (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma leftRel_pi {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
    leftRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ leftRel (s' i)

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (leftRel (Subgroup.pi univ s')) x y ↔ piSetoid x y

Tactic:
simp [Setoid.piSetoid_apply, leftRel_apply, Subgroup.mem_pi]

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ leftRel (Subgroup.pi univ s') = piSetoid

Tactic:
refine Setoid.ext fun x y ↦ ?_

Result:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (leftRel (Subgroup.pi univ s')) x y ↔ piSetoid x y
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem eq_one_iff {N : Subgroup G} [N.Normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N

Tactic:
rw [mul_one, Subgroup.inv_mem_iff]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ ↑x = 1 ↔ x ∈ N

Tactic:
refine QuotientGroup.eq.trans ?_

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem FiniteDimensional.proper [FiniteDimensional 𝕜 E] : ProperSpace E

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
⊢ ProperSpace E

Tactic:
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ ProperSpace E

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ ProperSpace E

Tactic:
exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ ProperSpace E

Tactic:
have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
⊢ ProperSpace E
-- Mathlib/Data/Nat/Size.lean
theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n

Proof state:
m : ℕ
h : m ≠ 0
n : ℕ
⊢ (m <<< n).size = m.size + n

Tactic:
simp only [size_shiftLeft' (shiftLeft'_ne_zero_left _ h _), ← shiftLeft'_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_div_self (m n : Nat) : m % n / n = 0

Proof state:
m n : Nat
⊢ m % (n + 1) / (n + 1) = 0

Tactic:
exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)

Result:
no goals

Proof state:
case succ
m n✝ : Nat
⊢ m % (n✝ + 1) / (n✝ + 1) = 0

Tactic:
case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)

Result:
no goals

Proof state:
case zero
m : Nat
⊢ m % 0 / 0 = 0

Tactic:
exact (m % 0).div_zero

Result:
no goals

Proof state:
m n : Nat
⊢ m % n / n = 0

Tactic:
cases n

Result:
case zero
m : Nat
⊢ m % 0 / 0 = 0

case succ
m n✝ : Nat
⊢ m % (n✝ + 1) / (n✝ + 1) = 0
-- Mathlib/Topology/Separation/Basic.lean
theorem nhdsSet_inj_iff [T1Space X] {s t : Set X} : 𝓝ˢ s = 𝓝ˢ t ↔ s = t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s = 𝓝ˢ t ↔ s = t

Tactic:
simp_rw [le_antisymm_iff]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s

Tactic:
exact and_congr nhdsSet_le_iff nhdsSet_le_iff

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_unique [h : Unique ι] : range f = {f default}

Proof state:
case h
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ (∃ y, f y = x) ↔ x ∈ {f default}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ (∃ y, f y = x) → x ∈ {f default}

case h.mpr
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ x ∈ {f default} → ∃ y, f y = x

Proof state:
case h.mp.intro
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
i : ι
hi : f i = x
⊢ x ∈ {f default}

Tactic:
rw [h.uniq i] at hi

Result:
case h.mp.intro
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
i : ι
hi : f default = x
⊢ x ∈ {f default}

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
⊢ range f = {f default}

Tactic:
ext x

Result:
case h
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ x ∈ range f ↔ x ∈ {f default}

Proof state:
case h.mp.intro
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
i : ι
hi : f default = x
⊢ x ∈ {f default}

Tactic:
exact hi ▸ mem_singleton _

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ x ∈ {f default} → ∃ y, f y = x

Tactic:
exact fun h => ⟨default, h.symm⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ (∃ y, f y = x) → x ∈ {f default}

Tactic:
rintro ⟨i, hi⟩

Result:
case h.mp.intro
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
i : ι
hi : f i = x
⊢ x ∈ {f default}

Proof state:
case h
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ x ∈ range f ↔ x ∈ {f default}

Tactic:
rw [mem_range]

Result:
case h
α : Type u_1
ι : Sort u_4
f : ι → α
h : Unique ι
x : α
⊢ (∃ y, f y = x) ↔ x ∈ {f default}
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) : s.affineCombination k p₁ w₁ = s.affineCombination k p₂ w₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
⊢ (affineCombination k s p₁) w₁ = (affineCombination k s p₂) w₂

Tactic:
simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_comp_one_sub_X (p : R[X]) (k : ℕ) :
    derivative^[k] (p.comp (1 - X)) = (-1) ^ k * (derivative^[k] p).comp (1 - X)

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ (⇑derivative)^[0] (p.comp (1 - X)) = (-1) ^ 0 * ((⇑derivative)^[0] p).comp (1 - X)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)

Tactic:
induction' k with k ih generalizing p

Result:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ (⇑derivative)^[0] (p.comp (1 - X)) = (-1) ^ 0 * ((⇑derivative)^[0] p).comp (1 - X)

case succ
R : Type u
inst✝ : CommRing R
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)
p : R[X]
⊢ (⇑derivative)^[k + 1] (p.comp (1 - X)) = (-1) ^ (k + 1) * ((⇑derivative)^[k + 1] p).comp (1 - X)

Proof state:
case succ
R : Type u
inst✝ : CommRing R
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)
p : R[X]
⊢ (⇑derivative)^[k + 1] (p.comp (1 - X)) = (-1) ^ (k + 1) * ((⇑derivative)^[k + 1] p).comp (1 - X)

Tactic:
simp [ih (derivative p), iterate_derivative_neg, derivative_comp, pow_succ]

Result:
no goals
-- Mathlib/Algebra/Order/Chebyshev.lean
theorem sq_sum_le_card_mul_sum_sq : (∑ i ∈ s, f i) ^ 2 ≤ #s * ∑ i ∈ s, f i ^ 2

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ (∑ i ∈ s, f i) ^ 2 ≤ ↑(#s) * ∑ i ∈ s, f i ^ 2

Tactic:
simp_rw [sq]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ x ∈ s, f x * f x

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ x ∈ s, f x * f x

Tactic:
exact (monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_fmod (b : Int) : fmod 0 b = 0

Proof state:
b : Int
⊢ fmod 0 b = 0

Tactic:
cases b <;> rfl

Result:
no goals