harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/AList.lean
theorem insert_union {a} {b : β a} {s₁ s₂ : AList β} :
    insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂

Tactic:
ext

Result:
case a.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
i✝ : ℕ
a✝ : Sigma β
⊢ a✝ ∈ (insert a b (s₁ ∪ s₂)).entries[i✝]? ↔ a✝ ∈ (insert a b s₁ ∪ s₂).entries[i✝]?

Proof state:
case a.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
i✝ : ℕ
a✝ : Sigma β
⊢ a✝ ∈ (insert a b (s₁ ∪ s₂)).entries[i✝]? ↔ a✝ ∈ (insert a b s₁ ∪ s₂).entries[i✝]?

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_one : primeFactorsList 1 = []

Proof state:
⊢ primeFactorsList 1 = []

Tactic:
rw [primeFactorsList]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem contentRegular_exists_compact (H : ContentRegular μ) (K : TopologicalSpace.Compacts G)
    {ε : NNReal} (hε : ε ≠ 0) :
    ∃ K' : TopologicalSpace.Compacts G, K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ε

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
⊢ False

Tactic:
have lower_bound_iInf : μ K + ε ≤
    ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
  le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), μ K'
⊢ False

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ False

Tactic:
simp only [not_exists, not_and, not_le] at hc

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
⊢ False

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ μ K
⊢ False

Tactic:
exact (lt_self_iff_false (μ K)).mp (lt_of_le_of_lt' lower_bound_iInf
  (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))

Result:
no goals

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε

Tactic:
by_contra hc

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ False

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), μ K'
⊢ False

Tactic:
rw [← H] at lower_bound_iInf

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → μ K + ↑ε < μ x
lower_bound_iInf : μ K + ↑ε ≤ μ K
⊢ False
-- Mathlib/Order/KrullDimension.lean
@[simp]
lemma height_enat (n : ℕ∞) : height n = n

Proof state:
n : ℕ∞
⊢ height n = n

Tactic:
cases n with
| top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
| coe n => exact (height_coe_withTop _).trans (height_nat _)

Result:
no goals

Proof state:
case coe
n : ℕ
⊢ height ↑n = ↑n

Tactic:
exact (height_coe_withTop _).trans (height_nat _)

Result:
no goals

Proof state:
case top

⊢ height ⊤ = ⊤

Tactic:
simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem mk_intCast (m : ℤ) : (mk m 1 : Localization M) = m

Proof state:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
m : ℤ
⊢ mk (↑m) 1 = ↑m

Tactic:
simpa using mk_algebraMap (R := R) (A := ℤ) _

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem _root_.Equiv.Perm.prod_comp' (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β)
    (hs : { a | σ a ≠ a } ⊆ s) : (∏ x ∈ s, f (σ x) x) = ∏ x ∈ s, f x (σ.symm x)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → α → β
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

Tactic:
convert σ.prod_comp s (fun x => f x (σ.symm x)) hs

Result:
case h.e'_2.h.e'_5.h.h.e'_2
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → α → β
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : α
⊢ x✝ = (Equiv.symm σ) (σ x✝)

Proof state:
case h.e'_2.h.e'_5.h.h.e'_2
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → α → β
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : α
⊢ x✝ = (Equiv.symm σ) (σ x✝)

Tactic:
rw [Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem coe_lt [Preorder β] {f g : α → β} : (f : β*) < g ↔ ∀* x, f x < g x

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
f g : α → β
⊢ ↑f < ↑g ↔ ∀* (x : α), f x < g x

Tactic:
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLE]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem graph_eq_ker_coprod : g.graph = ker ((-g).coprod LinearMap.id)

Proof state:
case h
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x.2 = g x.1 ↔ -g x.1 + x.2 = 0

Tactic:
rw [add_comm, add_neg_eq_zero]

Result:
no goals

Proof state:
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
⊢ g.graph = ker ((-g).coprod id)

Tactic:
ext x

Result:
case h
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x ∈ g.graph ↔ x ∈ ker ((-g).coprod id)

Proof state:
case h
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x ∈ g.graph ↔ x ∈ ker ((-g).coprod id)

Tactic:
change _ = _ ↔ -g x.1 + x.2 = _

Result:
case h
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x.2 = g x.1 ↔ -g x.1 + x.2 = 0
-- Mathlib/Data/Matroid/Circuit.lean
/-- A generalization of the strong circuit elimination axiom `Matroid.IsCircuit.strong_elimination`
to an infinite collection of isCircuits.

It states that, given a circuit `C₀`, a arbitrary collection `C : ι → Set α` of circuits,
an element `x i` of `C₀ ∩ C i` for each `i`, and an element `z ∈ C₀` outside all the `C i`,
the union of `C₀` and the `C i` contains a circuit containing `z` but none of the `x i`.

This is one of the axioms when defining infinite matroids via circuits.

TODO : A similar statement will hold even when all mentions of `z` are removed. -/
lemma IsCircuit.strong_multi_elimination (hC₀ : M.IsCircuit C₀) (x : ι → α) (C : ι → Set α) (z : α)
    (hC : ∀ i, M.IsCircuit (C i)) (h_mem_C₀ : ∀ i, x i ∈ C₀) (h_mem : ∀ i, x i ∈ C i)
    (h_unique : ∀ ⦃i i'⦄, x i ∈ C i' → i = i') (hzC₀ : z ∈ C₀) (hzC : ∀ i, z ∉ C i) :
    ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Proof state:
case refine_2
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ range x ⊆ C₀

Tactic:
rintro _ ⟨i, hi, rfl⟩

Result:
case refine_2.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
i : ι
⊢ x i ∈ C₀

Proof state:
case refine_2
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ M.IsCircuit (C₀ \ range x ∪ range x)

Tactic:
rwa [diff_union_self, union_eq_self_of_subset_right]

Result:
case refine_2
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ range x ⊆ C₀
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem glueDist_triangle_inl_inr_inr (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x : X) (y z : Y) :
    glueDist Φ Ψ ε (.inl x) (.inr z) ≤
      glueDist Φ Ψ ε (.inl x) (.inr y) + glueDist Φ Ψ ε (.inr y) (.inr z)

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + dist y z

Tactic:
rw [add_right_comm, add_le_add_iff_right]

Result:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ p, dist x (Φ p) + dist z (Ψ p) ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z

Proof state:
case refine_1
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ 0 ∈ lowerBounds (range fun p => dist x (Φ p) + dist z (Ψ p))

Tactic:
exact forall_mem_range.2 fun _ => add_nonneg dist_nonneg dist_nonneg

Result:
no goals

Proof state:
case refine_2
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z

Tactic:
linarith [dist_triangle_left z (Ψ p) y]

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)

Tactic:
simp only [glueDist]

Result:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + dist y z

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ p, dist x (Φ p) + dist z (Ψ p) ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z

Tactic:
refine le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_

Result:
case refine_1
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ 0 ∈ lowerBounds (range fun p => dist x (Φ p) + dist z (Ψ p))

case refine_2
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
lemma Topology.IsEmbedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} {s : Set α}
    (hf : IsEmbedding f) : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u.Subsingleton

Tactic:
obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
  ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected (f '' v)
⊢ (f '' v).Subsingleton

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ u.Subsingleton

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected (f '' v)
⊢ (f '' v).Subsingleton

Tactic:
rw [hf.isInducing.isPreconnected_image] at hu

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected v
⊢ (f '' v).Subsingleton

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ f '' (f ⁻¹' u ∩ s) = u

Tactic:
rwa [image_preimage_inter, inter_eq_left]

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected v
⊢ (f '' v).Subsingleton

Tactic:
exact (hs v hvs hu).image _

Result:
no goals
-- Mathlib/Topology/JacobsonSpace.lean
lemma preimage_closedPoints_subset (hf : Function.Injective f) (hf' : Continuous f) :
    f ⁻¹' closedPoints Y ⊆ closedPoints X

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ x ∈ closedPoints X

Tactic:
rw [mem_closedPoints_iff]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed {x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
⊢ f ⁻¹' closedPoints Y ⊆ closedPoints X

Tactic:
intros x hx

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ x ∈ closedPoints X

Proof state:
case h.e'_3
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' {f x}

Tactic:
rw [← Set.image_singleton, Set.preimage_image_eq _ hf]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed {x}

Tactic:
convert continuous_iff_isClosed.mp hf' _ hx

Result:
case h.e'_3
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' {f x}
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonnegg_neg_pos {c d} : ∀ {a b : ℕ}, Nonnegg c d (-a) b ↔ SqLe a d b c
  | 0, b => ⟨by simp [SqLe, Nat.zero_le], fun _ => trivial⟩
  | a + 1, b => by rw [← Int.negSucc_coe]; rfl

Proof state:
c d a b : ℕ
⊢ Nonnegg c d (-↑(a + 1)) ↑b ↔ SqLe (a + 1) d b c

Tactic:
rw [← Int.negSucc_coe]

Result:
c d a b : ℕ
⊢ Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c

Proof state:
c d a b : ℕ
⊢ Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c

Tactic:
rfl

Result:
no goals

Proof state:
c d b : ℕ
⊢ Nonnegg c d (-↑0) ↑b → SqLe 0 d b c

Tactic:
simp [SqLe, Nat.zero_le]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
/-- The defining property of the weak operator topology: a function `f` tends to
`A : E →WOT[𝕜] F` along filter `l` iff `⟪y, (f a) x⟫` tends to `⟪y, A x⟫` along the same filter. -/
lemma tendsto_iff_forall_inner_apply_tendsto [CompleteSpace F] {α : Type*} {l : Filter α}
    {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} :
    Tendsto f l (𝓝 A) ↔ ∀ x y, Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ (∀ (x : E) (y : F →L[𝕜] 𝕜), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))) ↔
    ∀ (x : E) (y : F),
      Tendsto (fun a => ((InnerProductSpace.toDual 𝕜 F) y) ((f a) x)) l (𝓝 (((InnerProductSpace.toDual 𝕜 F) y) (A x)))

Tactic:
exact .symm <| forall_congr' fun _ ↦
  Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)

Tactic:
simp_rw [tendsto_iff_forall_dual_apply_tendsto, ← InnerProductSpace.toDual_apply]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ (∀ (x : E) (y : F →L[𝕜] 𝕜), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))) ↔
    ∀ (x : E) (y : F),
      Tendsto (fun a => ((InnerProductSpace.toDual 𝕜 F) y) ((f a) x)) l (𝓝 (((InnerProductSpace.toDual 𝕜 F) y) (A x)))
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_Ioo_same (h : a ≤ b) : Icc a b \ Ioo a b = {a, b}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b

Tactic:
simp [insert_subset_iff, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
rw [← Icc_diff_both, diff_diff_cancel_left]

Result:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBySet_iff_subset_annihilator {s : Set R} :
    IsTorsionBySet R M s ↔ s ⊆ annihilator R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)

Tactic:
simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0

Tactic:
rw [forall_comm, SetCoe.forall]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
rw [← h, tsub_pos_iff_lt] at h₁

Result:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a

Tactic:
refine tsub_le_self.lt_of_ne fun h => ?_

Result:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem IsSemisimpleRing.ideal_eq_span_idempotent [IsSemisimpleRing R] (I : Ideal R) :
    ∃ e : R, IsIdempotentElem e ∧ I = .span {e}

Proof state:
case intro
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I J : Ideal R
h : IsCompl I J
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)

Result:
case intro.mk.intro
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ ∃ e, IsIdempotentElem e ∧ LinearMap.range f = Ideal.span {e}

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I : Ideal R
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨J, h⟩ := exists_isCompl I

Result:
case intro
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I J : Ideal R
h : IsCompl I J
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}

Proof state:
case intro.mk.intro
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ ∃ e, IsIdempotentElem e ∧ LinearMap.range f = Ideal.span {e}

Tactic:
exact ⟨f 1, LinearMap.isIdempotentElem_apply_one_iff.mpr idem, by
  erw [LinearMap.range_eq_map, ← Ideal.span_one, LinearMap.map_span, Set.image_singleton]; rfl⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Submodule.span R {f 1} = Ideal.span {f 1}

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ LinearMap.range f = Ideal.span {f 1}

Tactic:
erw [LinearMap.range_eq_map, ← Ideal.span_one, LinearMap.map_span, Set.image_singleton]

Result:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Submodule.span R {f 1} = Ideal.span {f 1}
-- Mathlib/Order/Concept.lean
theorem snd_ssubset_snd_iff : c.snd ⊂ d.snd ↔ d < c

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.toProd.2 ⊂ d.toProd.2 ↔ d < c

Tactic:
rw [ssubset_iff_subset_not_subset, lt_iff_le_not_le, snd_subset_snd_iff, snd_subset_snd_iff]

Result:
no goals