harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Indization/IndObject.lean
/-- Presheaves over a small finitely cocomplete category `C : Type u` are Ind-objects if and only if
they are left-exact. -/
lemma isIndObject_iff_preservesFiniteLimits [HasFiniteColimits C] (A : Cᵒᵖ ⥤ Type u) :
    IsIndObject A ↔ PreservesFiniteLimits A :=
  (isIndObject_iff A).trans <| by
    refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
    · apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
    · exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A
    · have := essentiallySmallSelf (CostructuredArrow yoneda A)
      apply finallySmall_of_essentiallySmall

Proof state:
case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A

Result:
no goals

Proof state:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩

Result:
case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
x✝ : IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A)
h₁ : IsFiltered (CostructuredArrow yoneda A)
h₂ : FinallySmall (CostructuredArrow yoneda A)
⊢ PreservesFiniteLimits A

case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)

Proof state:
case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
x✝ : IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A)
h₁ : IsFiltered (CostructuredArrow yoneda A)
h₂ : FinallySmall (CostructuredArrow yoneda A)
⊢ PreservesFiniteLimits A

Tactic:
apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda

Result:
no goals

Proof state:
case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
this : EssentiallySmall.{max ?u.49445 u, u, u} (CostructuredArrow yoneda A)
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
apply finallySmall_of_essentiallySmall

Result:
no goals

Proof state:
case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
have := essentiallySmallSelf (CostructuredArrow yoneda A)

Result:
case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
this : EssentiallySmall.{max ?u.49445 u, u, u} (CostructuredArrow yoneda A)
⊢ FinallySmall (CostructuredArrow yoneda A)
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_rpow_eq_tsum (hp : 0 < p.toReal) (f : lp E p) :
    ‖f‖ ^ p.toReal = ∑' i, ‖f i‖ ^ p.toReal

Proof state:
case hx.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
calc
  (0 : ℝ) = (0 : ℝ) ^ p.toReal := by rw [Real.zero_rpow hp.ne']
  _ ≤ _ := by gcongr; apply norm_nonneg

Result:
no goals

Proof state:
case h₁
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 ≤ ‖↑f i‖

Tactic:
apply norm_nonneg

Result:
no goals

Proof state:
case hx.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
intro i

Result:
case hx.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 ^ p.toReal ≤ ‖↑f i‖ ^ p.toReal

Tactic:
gcongr

Result:
case h₁
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 ≤ ‖↑f i‖

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
i : α
⊢ 0 = 0 ^ p.toReal

Tactic:
rw [Real.zero_rpow hp.ne']

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal

case hx
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ 0 ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal

Proof state:
case hx
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ 0 ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
apply tsum_nonneg

Result:
case hx.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
field_simp

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_self_mul_compl_apply (s : Set α) (f : α → M) (a : α) :
    mulIndicator s f a * mulIndicator sᶜ f a = f a :=
  by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∉ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_lt_ofReal_iff {p q : ℝ} (h : 0 < q) :
    ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Proof state:
p q : ℝ
h : 0 < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem regular_of_isMulLeftInvariant {μ : Measure G} [SigmaFinite μ] [IsMulLeftInvariant μ]
    {K : Set G} (hK : IsCompact K) (h2K : (interior K).Nonempty) (hμK : μ K ≠ ∞) : Regular μ

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : μ K ≠ ⊤
⊢ μ.Regular

Tactic:
rw [haarMeasure_unique μ ⟨⟨K, hK⟩, h2K⟩]

Result:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : μ K ≠ ⊤
⊢ (μ ↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K } •
      haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K }).Regular

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : μ K ≠ ⊤
⊢ (μ ↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K } •
      haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K }).Regular

Tactic:
exact Regular.smul hμK

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y

Proof state:
case a
n : Nat
x y : BitVec n
⊢ (x - y).toNat = (x + -y).toNat

Tactic:
simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]

Result:
case a
n : Nat
x y : BitVec n
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n

Proof state:
case a
n : Nat
x y : BitVec n
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n

Tactic:
rw [Nat.add_comm]

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x - y = x + -y

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x y : BitVec n
⊢ (x - y).toNat = (x + -y).toNat
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm'_mono_nnnorm_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
    eLpNorm' f q μ ≤ eLpNorm' g q μ

Proof state:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
x : α
hx : ‖f x‖₊ ≤ ‖g x‖₊
⊢ ‖f x‖ₑ ^ q ≤ ‖g x‖ₑ ^ q

Tactic:
dsimp [enorm]

Result:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
x : α
hx : ‖f x‖₊ ≤ ‖g x‖₊
⊢ ↑‖f x‖₊ ^ q ≤ ↑‖g x‖₊ ^ q

Proof state:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ

Tactic:
refine lintegral_mono_ae (h.mono fun x hx => ?_)

Result:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
x : α
hx : ‖f x‖₊ ≤ ‖g x‖₊
⊢ ‖f x‖ₑ ^ q ≤ ‖g x‖ₑ ^ q

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr ?_ ^ (1/q)

Result:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ

Proof state:
case h₁
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
x : α
hx : ‖f x‖₊ ≤ ‖g x‖₊
⊢ ↑‖f x‖₊ ^ q ≤ ↑‖g x‖₊ ^ q

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNorm' f q μ ≤ eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm]

Result:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Ioi_mul_left (a : α) : (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Tactic:
rw [mul_comm, left_mul_prod_Ioi]

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem linearIndependent_smul_of_linearIndependent {s : Finset F} :
    (LinearIndepOn (FixedPoints.subfield G F) id (s : Set F)) →
      LinearIndepOn F (MulAction.toFun G F) s

Proof state:
case intro.intro
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : (Finsupp.linearCombination F ⇑(toFun G F)) l = (toFun G F) a
⊢ False

Tactic:
rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla

Result:
case intro.intro
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_exp {x : ℂ} (hx₁ : -π < x.im) (hx₂ : x.im ≤ π) : log (exp x) = x

Proof state:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (cexp x) = x

Tactic:
rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
  arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
lemma trace_comp_cycle (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) :
    trace R P (g ∘ₗ f ∘ₗ h) = trace R N (f ∘ₗ h ∘ₗ g)

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R N
inst✝² : Module.Finite R N
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) (g ∘ₗ f ∘ₗ h) = (trace R N) (f ∘ₗ h ∘ₗ g)

Tactic:
rw [trace_comp_comm', comp_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem mem_span_insert_exchange :
    x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y z : V
hz : z ∈ span K s
h : 0 • y + z ∉ span K s
⊢ False

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z

Tactic:
have a0 : a ≠ 0 := by
  rintro rfl
  simp_all

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x y : V
⊢ ∀ (x_1 : K), ∀ x_2 ∈ span K s, x = x_1 • y + x_2 → x ∉ span K s → ∃ a, ∃ z ∈ span K s, y = a • x + z

Tactic:
rintro a z hz rfl h

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ ∃ a_1, ∃ z_1 ∈ span K s, y = a_1 • (a • y + z) + z_1

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z

Tactic:
match_scalars <;> simp [a0]

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x y : V
⊢ x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s)

Tactic:
simp only [mem_span_insert, forall_exists_index, and_imp]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x y : V
⊢ ∀ (x_1 : K), ∀ x_2 ∈ span K s, x = x_1 • y + x_2 → x ∉ span K s → ∃ a, ∃ z ∈ span K s, y = a • x + z

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y z : V
hz : z ∈ span K s
h : 0 • y + z ∉ span K s
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ ∃ a_1, ∃ z_1 ∈ span K s, y = a_1 • (a • y + z) + z_1

Tactic:
refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasDerivAt_ofReal_cpow_const' {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ -1) :
    HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1) / (r + 1)) (x ^ r) x

Proof state:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 • ((r + 1) * ↑(-x) ^ r)

Tactic:
rw [real_smul, ofReal_neg 1, ofReal_one]

Result:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 * ((r + 1) * ↑(-x) ^ r)

Proof state:
case inl.convert_4.convert_6
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ∈ slitPlane

Tactic:
simp [hx]

Result:
no goals

Proof state:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
⊢ r = r + 1 - 1

Tactic:
ring

Result:
no goals

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
have : ∀ᶠ y : ℝ in 𝓝 x,
    (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) := by
  refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
  rw [ofReal_cpow_of_nonpos (le_of_lt hy)]

Result:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Proof state:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)

Tactic:
refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_

Result:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
y : ℝ
hy : y ∈ Set.Iio 0
⊢ ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)

Proof state:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x

Tactic:
convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1

Result:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 • ((r + 1) * ↑(-x) ^ r)
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem IsNilpotent.mapQ (hnp : IsNilpotent f) : IsNilpotent (p.mapQ p f hp)

Proof state:
case intro
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
use k

Result:
case h
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ p.mapQ p f hp ^ k = 0

Proof state:
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
obtain ⟨k, hk⟩ := hnp

Result:
case intro
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ IsNilpotent (p.mapQ p f hp)

Proof state:
case h
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ p.mapQ p f hp ^ k = 0

Tactic:
simp [← p.mapQ_pow, hk]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem support_update_zero [DecidableEq α] : support (f.update a 0) = f.support.erase a

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
inst✝ : DecidableEq α
⊢ (f.update a 0).support = f.support.erase a

Tactic:
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
inst✝ : DecidableEq α
⊢ f.support.erase a = f.support.erase a

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
inst✝ : DecidableEq α
⊢ (f.update a 0).support = f.support.erase a

Tactic:
classical
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
congr!

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
inst✝ : DecidableEq α
⊢ f.support.erase a = f.support.erase a

Tactic:
congr!

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem fill_toList {p : Path α} : (p.fill t).toList = p.withList t.toList

Proof state:
α : Type u_1
t : RBNode α
p : Path α
⊢ (p.fill t).toList = p.withList t.toList

Tactic:
induction p generalizing t <;> simp [*]

Result:
no goals