harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConcaveOn.exists_lipschitzOnWith_of_isBounded (hf : ConcaveOn ℝ (ball x₀ r) f) (hr : r' < r)
    (hf' : IsBounded (f '' ball x₀ r)) : ∃ K, LipschitzOnWith K f (ball x₀ r')

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert hf'.neg; ext; simp [neg_eq_iff_eq_neg]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ IsBounded ((-f) '' ball x₀ r)

Tactic:
convert hf'.neg

Result:
case h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ (-f) '' ball x₀ r = -f '' ball x₀ r

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
simpa using hf.neg.exists_lipschitzOnWith_of_isBounded hr hf'

Result:
no goals

Proof state:
case h.e'_3.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
x✝ : ℝ
⊢ x✝ ∈ (-f) '' ball x₀ r ↔ x✝ ∈ -f '' ball x₀ r

Tactic:
simp [neg_eq_iff_eq_neg]

Result:
no goals

Proof state:
case h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ (-f) '' ball x₀ r = -f '' ball x₀ r

Tactic:
ext

Result:
case h.e'_3.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
x✝ : ℝ
⊢ x✝ ∈ (-f) '' ball x₀ r ↔ x✝ ∈ -f '' ball x₀ r
-- Mathlib/Data/Stream/Init.lean
theorem mem_cycle {a : α} {l : List α} : ∀ h : l ≠ [], a ∈ l → a ∈ cycle l h := fun h ainl => by
  rw [cycle_eq]; exact mem_append_stream_left _ ainl

Proof state:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h

Tactic:
rw [cycle_eq]

Result:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h

Proof state:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h

Tactic:
exact mem_append_stream_left _ ainl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma id_apply (M : ModuleCat.{v} R) (x : M) :
    (𝟙 M : M ⟶ M) x = x

Proof state:
R : Type u
inst✝ : Ring R
M : ModuleCat R
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem right_vsub_lineMap (p₀ p₁ : P1) (c : k) : p₁ -ᵥ lineMap p₀ p₁ c = (1 - c) • (p₁ -ᵥ p₀)

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ p₁ -ᵥ (lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)

Tactic:
rw [← lineMap_apply_one_sub, left_vsub_lineMap]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma smul_def (a : α) (S : Submodule R M) : a • S = span R (a • S : Set M)

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Monoid α
inst✝¹ : DistribMulAction α M
inst✝ : SMulCommClass α R M
a : α
S : Submodule R M
⊢ a • S = span R (a • ↑S)

Tactic:
simp [← smul_span]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem smul_nonpos {f : ι → Ω → F} {c : ℝ} (hc : c ≤ 0) (hf : Supermartingale f ℱ μ) :
    Submartingale (c • f) ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ - -c • f = -(-c • f)

Tactic:
ext (i x)

Result:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(-c • f)) i x

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg c, (by ext (i x); simp : - -c • f = -(-c • f))]

Result:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ Submartingale (-(-c • f)) ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
⊢ Submartingale (-(-c • f)) ℱ μ

Tactic:
exact (hf.smul_nonneg <| neg_nonneg.2 hc).neg

Result:
no goals

Proof state:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Supermartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(-c • f)) i x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean
lemma exact_of_degreewise_exact (hS : ∀ (i : ι), (S.map (eval C c i)).Exact) :
    S.Exact

Proof state:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), (S.map (eval C c i)).Exact
⊢ S.Exact

Tactic:
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢

Result:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ IsZero S.homology

Proof state:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ 𝟙 S.homology = 0

Tactic:
ext i

Result:
case h
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
i : ι
⊢ (𝟙 S.homology).f i = Hom.f 0 i

Proof state:
case h
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
i : ι
⊢ (𝟙 S.homology).f i = Hom.f 0 i

Tactic:
apply (IsZero.of_iso (hS i) (S.mapHomologyIso (eval C c i)).symm).eq_of_src

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ IsZero S.homology

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ 𝟙 S.homology = 0
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma_cong_eq_self (N : ℕ) (g : ConjAct SL(2, ℤ)) : g • Gamma N = Gamma N

Proof state:
N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Γ(N) = Γ(N)

Tactic:
apply Subgroup.Normal.conjAct (Gamma_normal N)

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_eraseIdx_of_getElem?_eq {l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) :
    eraseIdx l₁ m ~ eraseIdx l₂ n ↔ l₁ ~ l₂

Proof state:
case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
  rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Result:
no goals

Proof state:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h

Result:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Proof state:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge m l₁.length with
| inl hm =>
  rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
  cases h with
  | intro hn hnm =>
    rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
      rel_congr_right (getElem_cons_eraseIdx_perm ..)]
| inr hm =>
  rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
  rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

Result:
no goals

Proof state:
case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h : ∃ h, l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
cases h with
| intro hn hnm =>
  rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
    rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Result:
no goals

Proof state:
case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m < l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h

Result:
case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h : ∃ h, l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem zero : padicValNat p 0 = 0

Proof state:
p : ℕ
⊢ padicValNat p 0 = 0

Tactic:
simp [padicValNat]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
lemma ProperSpace.of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E] :
    ProperSpace 𝕜 :=
  have : LocallyCompactSpace 𝕜

Proof state:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
L : 𝕜 → E := fun t => t • v
this : IsClosedEmbedding L
⊢ LocallyCompactSpace 𝕜

Tactic:
apply IsClosedEmbedding.locallyCompactSpace this

Result:
no goals

Proof state:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
L : 𝕜 → E := fun t => t • v
⊢ LocallyCompactSpace 𝕜

Tactic:
have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv

Result:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
L : 𝕜 → E := fun t => t • v
this : IsClosedEmbedding L
⊢ LocallyCompactSpace 𝕜

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
⊢ LocallyCompactSpace 𝕜

Tactic:
obtain ⟨v, hv⟩ : ∃ v : E, v ≠ 0 := exists_ne 0

Result:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
⊢ LocallyCompactSpace 𝕜

Proof state:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
⊢ LocallyCompactSpace 𝕜

Tactic:
let L : 𝕜 → E := fun t ↦ t • v

Result:
case intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : Nontrivial E
inst✝ : LocallyCompactSpace E
v : E
hv : v ≠ 0
L : 𝕜 → E := fun t => t • v
⊢ LocallyCompactSpace 𝕜
-- Mathlib/Control/Basic.lean
theorem seq_map_assoc (x : F (α → β)) (f : γ → α) (y : F γ) :
    x <*> f <$> y = (· ∘ f) <$> x <*> y

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h => h f) ∘ Function.comp) <$> x <*> y = (fun x => x ∘ f) <$> x <*> y

Tactic:
rfl

Result:
no goals

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> (pure f <*> y) = (pure fun x => x ∘ f) <*> x <*> y

Tactic:
simp only [seq_assoc, Function.comp, seq_pure, ← comp_map]

Result:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h => h f) ∘ Function.comp) <$> x <*> y = (pure fun x => x ∘ f) <*> x <*> y

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun x => x ∘ f) <$> x <*> y

Tactic:
simp only [← pure_seq]

Result:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> (pure f <*> y) = (pure fun x => x ∘ f) <*> x <*> y

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h => h f) ∘ Function.comp) <$> x <*> y = (pure fun x => x ∘ f) <*> x <*> y

Tactic:
simp [pure_seq]

Result:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h => h f) ∘ Function.comp) <$> x <*> y = (fun x => x ∘ f) <$> x <*> y
-- Mathlib/Data/Real/EReal.lean
lemma add_sub_cancel_right {a : EReal} {b : Real} : a + b - b = a

Proof state:
case h_real
b a✝ : ℝ
⊢ a✝ + b - b = a✝

Tactic:
exact _root_.add_sub_cancel_right _ _

Result:
no goals

Proof state:
a : EReal
b : ℝ
⊢ a + ↑b - ↑b = a

Tactic:
cases a <;> norm_cast

Result:
case h_real
b a✝ : ℝ
⊢ a✝ + b - b = a✝
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem of_subset_range_algebraMap (hf : f.LeftInverse (algebraMap R S))
    (h : quasispectrum S a ⊆ Set.range (algebraMap R S)) : QuasispectrumRestricts a f where
  rightInvOn := fun s hs => by obtain ⟨r, rfl⟩ := h hs; rw [hf r]
  left_inv := hf

Proof state:
case intro
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)
r : R
hs : (algebraMap R S) r ∈ quasispectrum S a
⊢ (algebraMap R S) (f ((algebraMap R S) r)) = (algebraMap R S) r

Tactic:
rw [hf r]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
obtain ⟨r, rfl⟩ := h hs

Result:
case intro
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)
r : R
hs : (algebraMap R S) r ∈ quasispectrum S a
⊢ (algebraMap R S) (f ((algebraMap R S) r)) = (algebraMap R S) r
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem rank_add_le (f g : V →ₗ[K] V') : rank (f + g) ≤ rank f + rank g :=
  calc
    rank (f + g) ≤ Module.rank K (LinearMap.range f ⊔ LinearMap.range g : Submodule K V')

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f g : V →ₗ[K] V'
⊢ range (f + g) ≤ range f ⊔ range g

Tactic:
exact LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun x =>
  show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
  mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f g : V →ₗ[K] V'
⊢ (f + g).rank ≤ Module.rank K ↥(range f ⊔ range g)

Tactic:
refine Submodule.rank_mono ?_

Result:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f g : V →ₗ[K] V'
⊢ range (f + g) ≤ range f ⊔ range g
-- Mathlib/Topology/NhdsSet.lean
theorem subset_interior_iff_mem_nhdsSet : s ⊆ interior t ↔ t ∈ 𝓝ˢ s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s

Tactic:
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem factors_eq_normalizedFactors {M : Type*} [CancelCommMonoidWithZero M]
    [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) : factors x = normalizedFactors x

Proof state:
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = Multiset.map (⇑normalize) (factors x)

Tactic:
convert (Multiset.map_id (factors x)).symm

Result:
case h.e'_3.a.h.e
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
⊢ ⇑normalize = id

Proof state:
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = normalizedFactors x

Tactic:
unfold normalizedFactors

Result:
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = Multiset.map (⇑normalize) (factors x)

Proof state:
case h.e'_3.a.h.e
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
⊢ ⇑normalize = id

Tactic:
ext p

Result:
case h.e'_3.a.h.e.h
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
p : M
⊢ normalize p = id p

Proof state:
case h.e'_3.a.h.e.h
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
p : M
⊢ normalize p = id p

Tactic:
exact normalize_eq p

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isRat_zpow_neg {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb : ℕ}
    {num : ℤ} {den : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsRat ((a^nb)⁻¹) num den) :
    IsRat (a^b) num den

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.and_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a && b) = a

Proof state:
a b : Bool
h : b = true
⊢ (a && b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem id_comp' (p : FormalMultilinearSeries 𝕜 E F) (x : F) (v0 : Fin 0 → E) (h : x = p 0 v0) :
    (id 𝕜 F x).comp p = p

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : F
v0 : Fin 0 → E
h : x = (p 0) v0
⊢ (id 𝕜 F x).comp p = p

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndepOn_biUnion_of_directed {η} {s : Set η} {t : η → Set ι}
    (hs : DirectedOn (t ⁻¹'o (· ⊆ ·)) s) (h : ∀ a ∈ s, LinearIndepOn R v (t a)) :
    LinearIndepOn R v (⋃ a ∈ s, t a)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ a ∈ s, t a)

Tactic:
rw [biUnion_eq_iUnion]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ x, t ↑x)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ ∀ (i : ↑s), LinearIndepOn R v (t ↑i)

Tactic:
simpa using h

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ x, t ↑x)

Tactic:
exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

Result:
no goals