harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_mul_X' [DecidableEq σ] (m) (s : σ) (p : MvPolynomial σ R) :
    coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
refine (coeff_mul_monomial' _ _ _ _).trans ?_

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
  mul_one]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma hasFDerivWithinAt_tangentCoordChange {x y z : M}
    (h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source) :
    HasFDerivWithinAt ((extChartAt I y) ∘ (extChartAt I x).symm) (tangentCoordChange I x y z)
      (range I) (extChartAt I x z) :=
  have h' : extChartAt I x z ∈ ((extChartAt I x).symm ≫ (extChartAt I y)).source

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ ↑(extChartAt I x) z ∈ ((extChartAt I x).symm ≫ extChartAt I y).source

Tactic:
rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ ↑(extChartAt I x) z ∈ ↑(extChartAt I x) '' ((extChartAt I x).source ∩ (extChartAt I y).source)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ ↑(extChartAt I x) z ∈ ↑(extChartAt I x) '' ((extChartAt I x).source ∩ (extChartAt I y).source)

Tactic:
exact mem_image_of_mem _ h

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive]
lemma isCyclic_iff_exists_natCard_le_orderOf [Finite α] :
    IsCyclic α ↔ ∃ g : α, Nat.card α ≤ orderOf g

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ (∃ g, orderOf g = Nat.card α) ↔ ∃ g, Nat.card α ≤ orderOf g

Tactic:
apply exists_congr

Result:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ ∀ (a : α), orderOf a = Nat.card α ↔ Nat.card α ≤ orderOf a

Proof state:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g

Tactic:
exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ IsCyclic α ↔ ∃ g, Nat.card α ≤ orderOf g

Tactic:
rw [isCyclic_iff_exists_orderOf_eq_natCard]

Result:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ (∃ g, orderOf g = Nat.card α) ↔ ∃ g, Nat.card α ≤ orderOf g

Proof state:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ ∀ (a : α), orderOf a = Nat.card α ↔ Nat.card α ≤ orderOf a

Tactic:
intro g

Result:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem true_beq  : ∀b, (true  == b) =  b

Proof state:
⊢ ∀ (b : Bool), (true == b) = b

Tactic:
decide

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem start_v (a b : ℕ+) : (start a b).v = ⟨a, b⟩

Proof state:
a b : ℕ+
this✝ : 0 < ↑a
this : 0 < ↑b
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
congr <;> omega

Result:
no goals

Proof state:
a b : ℕ+
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
rw [one_mul, one_mul, zero_mul, zero_mul]

Result:
a b : ℕ+
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Proof state:
a b : ℕ+
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
have := a.pos

Result:
a b : ℕ+
this : 0 < ↑a
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Proof state:
a b : ℕ+
this : 0 < ↑a
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
have := b.pos

Result:
a b : ℕ+
this✝ : 0 < ↑a
this : 0 < ↑b
⊢ (↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)

Proof state:
a b : ℕ+
⊢ (start a b).v = (↑a, ↑b)

Tactic:
dsimp [start, v, XgcdType.a, XgcdType.b, w, z]

Result:
a b : ℕ+
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_one : det (1 : Matrix n n R) = 1

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
⊢ det 1 = 1

Tactic:
rw [← diagonal_one]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
⊢ (diagonal fun x => 1).det = 1

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
⊢ (diagonal fun x => 1).det = 1

Tactic:
simp [-diagonal_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem smul_finsum {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i

Proof state:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Result:
case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → M
⊢ 0 • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), 0 • f i

case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

Proof state:
case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → M
⊢ 0 • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), 0 • f i

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

Tactic:
exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma BoundaryGE.not_mem {j : ι} (hj : e.BoundaryGE j) {i' : ι'} (hi' : c'.Rel i' (e.f j))
    (a : ι) : e.f a ≠ i' := fun ha =>
  hj.2 a (by simpa only [ha] using hi')

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
i' : ι'
hi' : c'.Rel i' (e.f j)
a : ι
ha : e.f a = i'
⊢ c'.Rel (e.f a) (e.f j)

Tactic:
simpa only [ha] using hi'

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem toList_nil : toList (nil : Seq α) ⟨0, terminatedAt_zero_iff.2 rfl⟩ = []

Proof state:
case h.a
α : Type u
i✝ : ℕ
a✝ : α
⊢ a✝ ∈ (nil.toList ⋯)[i✝]? ↔ a✝ ∈ [][i✝]?

Tactic:
simp [nil, toList, const]

Result:
no goals

Proof state:
α : Type u
⊢ nil.toList ⋯ = []

Tactic:
ext

Result:
case h.a
α : Type u
i✝ : ℕ
a✝ : α
⊢ a✝ ∈ (nil.toList ⋯)[i✝]? ↔ a✝ ∈ [][i✝]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_left_eq_self {x y : BitVec w} : x + y = y ↔ x = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x + y = 0#w + y ↔ x = 0#w

Tactic:
exact BitVec.add_left_inj y

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x + y = y ↔ x = 0#w

Tactic:
conv => lhs; rhs; rw [← BitVec.zero_add y]

Result:
w : Nat
x y : BitVec w
⊢ x + y = 0#w + y ↔ x = 0#w
-- Mathlib/Data/Finsupp/Indicator.lean
theorem indicator_apply [DecidableEq ι] : indicator s f i = if hi : i ∈ s then f i hi else 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (indicator s f) i = if hi : i ∈ s then f i hi else 0

Tactic:
simp only [indicator, ne_eq, coe_mk]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_last_apply {i : Fin (n + 2)} :
    predAbove (last n) i = if hi : i = last _ then last _ else i.castPred hi

Proof state:
case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove i = last n

Tactic:
rw [hi, predAbove_right_last]

Result:
no goals

Proof state:
case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
rw [predAbove_last_of_ne_last hi]

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

Tactic:
split_ifs with hi

Result:
case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove i = last n

case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem uniformContinuous_lift' [T0Space β] (f : α → β) : UniformContinuous (lift' f)

Proof state:
case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
rwa [lift', dif_pos hf, uniformContinuous_lift]

Result:
no goals

Proof state:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
rw [lift', dif_neg hf]

Result:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f ⋯.some

Proof state:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f ⋯.some

Tactic:
exact uniformContinuous_of_const fun a _ => rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
⊢ UniformContinuous (lift' f)

Tactic:
by_cases hf : UniformContinuous f

Result:
case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)

case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem adjoin_range_X : Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) = ⊤

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Algebra.adjoin R (range X) = ⊤

Tactic:
set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R))

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
⊢ S = ⊤

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
⊢ p ∈ S

Tactic:
induction p using MvPolynomial.induction_on with
| h_C => exact S.algebraMap_mem _
| h_add p q hp hq => exact S.add_mem hp hq
| h_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

Result:
no goals

Proof state:
case h_X
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
i : σ
hp : p ∈ S
⊢ p * X i ∈ S

Tactic:
exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

Result:
no goals

Proof state:
case h_C
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
a✝ : R
⊢ C a✝ ∈ S

Tactic:
exact S.algebraMap_mem _

Result:
no goals

Proof state:
case h_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p q : MvPolynomial σ R
hp : p ∈ S
hq : q ∈ S
⊢ p + q ∈ S

Tactic:
exact S.add_mem hp hq

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
⊢ S = ⊤

Tactic:
refine top_unique fun p hp => ?_

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
hp : p ∈ ⊤
⊢ p ∈ S

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
hp : p ∈ ⊤
⊢ p ∈ S

Tactic:
clear hp

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
⊢ p ∈ S
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8Len_eq_zero : utf8Len l = 0 ↔ l = []

Proof state:
l : List Char
⊢ utf8Len l = 0 ↔ l = []

Tactic:
cases l <;> simp [Nat.ne_zero_iff_zero_lt.mpr (Char.utf8Size_pos _)]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) :
    Function.HasTemperateGrowth f

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
x : E
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * (1 + ‖x‖) ^ 1

Tactic:
simp [mul_add]

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
this : fderiv ℝ ⇑f = fun x => f
⊢ Function.HasTemperateGrowth (fderiv ℝ ⇑f)

Tactic:
simpa [this] using .const _

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
⊢ fderiv ℝ ⇑f = fun x => f

Tactic:
ext1 v

Result:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
v : E
⊢ fderiv ℝ (⇑f) v = f

Proof state:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
v : E
⊢ fderiv ℝ (⇑f) v = f

Tactic:
simp only [ContinuousLinearMap.fderiv]

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
x : E
⊢ ‖f x‖ ≤ ‖f‖ * (1 + ‖x‖) ^ 1

Tactic:
exact (f.le_opNorm x).trans (by simp [mul_add])

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
⊢ Function.HasTemperateGrowth ⇑f

Tactic:
apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_)

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
⊢ Function.HasTemperateGrowth (fderiv ℝ ⇑f)

E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
x : E
⊢ ‖f x‖ ≤ ‖f‖ * (1 + ‖x‖) ^ 1

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
⊢ Function.HasTemperateGrowth (fderiv ℝ ⇑f)

Tactic:
have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
this : fderiv ℝ ⇑f = fun x => f
⊢ Function.HasTemperateGrowth (fderiv ℝ ⇑f)
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) :
    G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

Tactic:
rw [edgeDensity_def, edgeDensity_def, div_add_div_same, div_eq_one_iff_eq]

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t)) = ↑(#s) * ↑(#t)

α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#s) * ↑(#t) ≠ 0

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#s) * ↑(#t) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t)) = ↑(#s) * ↑(#t)

Tactic:
exact mod_cast card_interedges_add_card_interedges_compl _ h

Result:
no goals
-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem affineIndependent_minCardFinsetOfMemConvexHull :
    AffineIndependent 𝕜 ((↑) : minCardFinsetOfMemConvexHull hx → E)

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ AffineIndependent 𝕜 Subtype.val

Tactic:
let k := #(minCardFinsetOfMemConvexHull hx) - 1

Result:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := #(minCardFinsetOfMemConvexHull hx) - 1
⊢ AffineIndependent 𝕜 Subtype.val
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem ofScientific_true_def : Rat.ofScientific m true e = mkRat m (10 ^ e)

Proof state:
m e : Nat
⊢ (if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)

Tactic:
rw [normalize_eq_mkRat]

Result:
m e : Nat
⊢ (if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)

Proof state:
m e : Nat
⊢ Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)

Tactic:
unfold Rat.ofScientific

Result:
m e : Nat
⊢ (if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)

Proof state:
m e : Nat
⊢ (if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_div_base (b n : ℕ) : log b (n / b) = log b n - 1

Proof state:
b n : ℕ
⊢ log b (n / b) = log b n - 1

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1

case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1

Proof state:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1

Tactic:
rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]

Result:
no goals

Proof state:
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1

Tactic:
rcases lt_or_le n b with h | h

Result:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1

case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]

Result:
no goals

Proof state:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1

Tactic:
rw [div_eq_of_lt h, log_of_lt h, log_zero_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_bot : (⊥ : TwoSidedIdeal R).matricesOver n = ⊥

Proof state:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

case h.mpr
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Proof state:
case h.mp
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0

Tactic:
ext

Result:
case h.mp.a
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i✝ j✝ : n
⊢ M i✝ j✝ = 0 i✝ j✝

Proof state:
case h.mp.a
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i✝ j✝ : n
⊢ M i✝ j✝ = 0 i✝ j✝

Tactic:
apply H

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
intro H

Result:
case h.mpr
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0

Proof state:
case h.mp
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

Tactic:
intro H

Result:
case h.mp
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0

Proof state:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ matricesOver n ⊥ ↔ M ∈ ⊥

Tactic:
simp only [mem_matricesOver, mem_bot]

Result:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
⊢ matricesOver n ⊥ = ⊥

Tactic:
ext M

Result:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ matricesOver n ⊥ ↔ M ∈ ⊥

Proof state:
case h.mpr
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0

Tactic:
simp [H]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_add (f g : α →₁[μ] E) : integral (f + g) = integral f + integral g

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integral (f + g) = integral f + integral g

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f + g) = integralCLM f + integralCLM g

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f + g) = integralCLM f + integralCLM g

Tactic:
exact map_add integralCLM f g

Result:
no goals