harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_neg (f : N →ₗ[R] P) : (-f).lTensor M = -f.lTensor M

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ (lTensorHom M) (-f) = -(lTensorHom M) f

Tactic:
exact (lTensorHom (R := R) (N := N) (P := P) M).map_neg f

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ lTensor M (-f) = -lTensor M f

Tactic:
simp only [← coe_lTensorHom]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ (lTensorHom M) (-f) = -(lTensorHom M) f
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuous₂_curry (f : α × β → γ) :
    UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

Proof state:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α × β → γ
⊢ UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

Tactic:
rw [UniformContinuous₂, uncurry_curry]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem dropLast_append_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l ++ [getLast l h] = l
  | [], h => absurd rfl h
  | [_], _ => rfl
  | a :: b :: l, h => by
    rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]
    congr
    exact dropLast_append_getLast (cons_ne_nil b l)

Proof state:
case e_tail
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Tactic:
exact dropLast_append_getLast (cons_ne_nil b l)

Result:
no goals

Proof state:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l

Tactic:
congr

Result:
case e_tail
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Proof state:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]

Result:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem atTop_neBot_iff {α : Type*} [Preorder α] :
    (atTop : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≤ ·)

Proof state:
α : Type u_6
inst✝ : Preorder α
h : atTop.NeBot
x y : α
⊢ ∃ c, x ≤ c ∧ y ≤ c

Tactic:
exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

Result:
no goals

Proof state:
α : Type u_6
inst✝ : Preorder α
⊢ atTop.NeBot ↔ Nonempty α ∧ IsDirected α fun x1 x2 => x1 ≤ x2

Tactic:
refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩

Result:
α : Type u_6
inst✝ : Preorder α
h : atTop.NeBot
x y : α
⊢ ∃ c, x ≤ c ∧ y ≤ c
-- Mathlib/Order/KrullDimension.lean
lemma le_krullDim_iff {n : ℕ} : n ≤ krullDim α ↔ ∃ l : LTSeries α, l.length = n

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
simp [krullDim_eq_bot]

Result:
no goals

Proof state:
case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length

Tactic:
exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

case inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : Nonempty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Proof state:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length ↔ ∃ l, l.length = n

Tactic:
constructor

Result:
case inr.inl.mp
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length → ∃ l, l.length = n

case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : Nonempty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
cases finiteDimensionalOrder_or_infiniteDimensionalOrder α

Result:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Proof state:
case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
simpa [krullDim_eq_top] using Rel.InfiniteDimensional.exists_relSeries_with_length n

Result:
no goals

Proof state:
case inr.inl.mp
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length → ∃ l, l.length = n

Tactic:
exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ.mpr H⟩, rfl⟩

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]

Result:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length ↔ ∃ l, l.length = n
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_nonneg (n : ℕ) (s : ℝ) : 0 ≤ term n s

Proof state:
n : ℕ
s : ℝ
⊢ 0 ≤ term n s

Tactic:
rw [term, intervalIntegral.integral_of_le (by simp)]

Result:
n : ℕ
s : ℝ
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume

Proof state:
n : ℕ
s : ℝ
⊢ ↑n ≤ ↑n + 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
s : ℝ
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume

Tactic:
refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ ?_)

Result:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ (x - ↑n) / x ^ (s + 1)

Proof state:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ (x - ↑n) / x ^ (s + 1)

Tactic:
refine div_nonneg ?_ (rpow_nonneg ?_ _)

Result:
case refine_1
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ x - ↑n

case refine_2
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ x

Proof state:
case refine_1
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ x - ↑n

case refine_2
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ x

Tactic:
all_goals linarith [hx.1]

Result:
no goals

Proof state:
case refine_2
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n) (↑n + 1)
⊢ 0 ≤ x

Tactic:
linarith [hx.1]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dual_finrank_eq : finrank K (Module.Dual K V) = finrank K V

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
by_cases h : FiniteDimensional K V

Result:
case pos
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Proof state:
case pos
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
classical exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm

Result:
no goals

Proof state:
case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)), Basis (↑↑s) K (Dual K V) → False

Tactic:
exact fun _ b ↦ h ((Module.finite_dual_iff K).mp <| Module.Finite.of_basis b)

Result:
no goals

Proof state:
case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset V), Basis (↑↑s) K V → False

Tactic:
exact fun _ b ↦ h (Module.Finite.of_basis b)

Result:
no goals

Proof state:
case pos
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm

Result:
no goals

Proof state:
case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]

Result:
case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset V), Basis (↑↑s) K V → False

case neg
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)), Basis (↑↑s) K (Dual K V) → False
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma isSemisimple_ad_of_mem_isCartanSubalgebra {x : L} (hx : x ∈ H) :
    (ad K L x).IsSemisimple

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆
y z : L
⊢ y ∈ ⨆ α, rootSpace H α

Tactic:
simp [iSup_genWeightSpace_eq_top]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
⊢ ((ad K L) x).IsSemisimple

Tactic:
have aux {α : H → K} {y : L} (hy : y ∈ rootSpace H α) : S y = α x' • y := by
  replace hy : y ∈ (ad K L x).maxGenEigenspace (α x') :=
    (genWeightSpace_le_genWeightSpaceOf L x' α) hy
  rw [maxGenEigenspace_eq] at hy
  set k := maxGenEigenspaceIndex (ad K L x) (α x')
  rw [apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hy hS₀ hS.isFinitelySemisimple hN]

Result:
case intro.intro.intro.intro.intro.intro
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
⊢ ((ad K L) x).IsSemisimple
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem prod_rpow_of_ne_top {ι} {s : Finset ι} {f : ι → ℝ≥0∞} (hf : ∀ i ∈ s, f i ≠ ∞) (r : ℝ) :
    ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ⊤
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
classical
induction s using Finset.induction with
| empty => simp
| @insert i s hi ih =>
  have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
  rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
  apply prod_ne_top h2f

Result:
no goals

Proof state:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ⊤
⊢ ∏ i ∈ insert i s, f i ^ r = (∏ i ∈ insert i s, f i) ^ r

Tactic:
have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi

Result:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ⊤
h2f : ∀ i ∈ s, f i ≠ ⊤
⊢ ∏ i ∈ insert i s, f i ^ r = (∏ i ∈ insert i s, f i) ^ r

Proof state:
case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hf : ∀ i ∈ ∅, f i ≠ ⊤
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
simp

Result:
no goals

Proof state:
case insert.hy
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ⊤
h2f : ∀ i ∈ s, f i ≠ ⊤
⊢ ∏ i ∈ s, f i ≠ ⊤

Tactic:
apply prod_ne_top h2f

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ⊤
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with
| empty => simp
| @insert i s hi ih =>
  have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
  rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
  apply prod_ne_top h2f

Result:
no goals

Proof state:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ⊤
h2f : ∀ i ∈ s, f i ≠ ⊤
⊢ ∏ i ∈ insert i s, f i ^ r = (∏ i ∈ insert i s, f i) ^ r

Tactic:
rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]

Result:
case insert.hy
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ⊤
h2f : ∀ i ∈ s, f i ≠ ⊤
⊢ ∏ i ∈ s, f i ≠ ⊤
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
@[simp] lemma add_left_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] :
    ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

Tactic:
rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem sub_le_integral_of_hasDeriv_right_of_le_Ico (hab : a ≤ b)
    (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x)
    (φint : IntegrableOn φ (Icc a b)) (hφg : ∀ x ∈ Ico a b, g' x ≤ φ x) :
    g b - g a ≤ ∫ y in a..b, φ y

Proof state:
case h
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x => (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal ∂volume < ∫ (x : ℝ) in Icc a b, φ x ∂volume + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
t_lt_u : u ∈ Ioi t
this : (u - t) * slope g t u ≤ (u - t) * y
⊢ g u - g t ≤ (u - t) * y

Tactic:
rwa [← smul_eq_mul, sub_smul_slope] at this

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem ι_basicOpen_preimage (r : Γ(X, ⊤)) :
    IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))

Tactic:
exact hU.basicOpen _

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (⋯.functor.obj ((X.basicOpen r).ι ⁻¹ᵁ U))

Tactic:
rw [Opens.functor_obj_map_obj, Opens.isOpenEmbedding_obj_top, inf_comm,
  ← Scheme.basicOpen_res _ _ (homOfLE le_top).op]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
dsimp [Scheme.Hom.opensFunctor, LocallyRingedSpace.IsOpenImmersion.opensFunctor]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (⋯.functor.obj ((X.basicOpen r).ι ⁻¹ᵁ U))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
-- Mathlib/Logic/Equiv/Functor.lean
theorem mapEquiv_refl : mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Proof state:
case H
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ⇑(Equiv.refl α) <$> x = x

Tactic:
exact LawfulFunctor.id_map x

Result:
no goals

Proof state:
case H
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ (mapEquiv f (Equiv.refl α)) x = (Equiv.refl (f α)) x

Tactic:
simp only [mapEquiv_apply, refl_apply]

Result:
case H
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ⇑(Equiv.refl α) <$> x = x

Proof state:
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext x

Result:
case H
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ (mapEquiv f (Equiv.refl α)) x = (Equiv.refl (f α)) x
-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_reindex {κ' : Type*} (b : Basis κ A B) (f : κ ≃ κ') :
    traceMatrix A (b.reindex f) = reindex f f (traceMatrix A b)

Proof state:
case a
κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
x y : κ'
⊢ traceMatrix A (⇑(b.reindex f)) x y = (reindex f f) (traceMatrix A ⇑b) x y

Tactic:
simp

Result:
no goals

Proof state:
κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
⊢ traceMatrix A ⇑(b.reindex f) = (reindex f f) (traceMatrix A ⇑b)

Tactic:
ext (x y)

Result:
case a
κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
x y : κ'
⊢ traceMatrix A (⇑(b.reindex f)) x y = (reindex f f) (traceMatrix A ⇑b) x y
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem prod_isUnit_iff {α : Type*} [CommMonoid α] {L : List α} :
    IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m

Proof state:
case nil
α : Type u_8
inst✝ : CommMonoid α
h : IsUnit [].prod
⊢ ∀ m ∈ [], IsUnit m

Tactic:
exact fun m' h' => False.elim (not_mem_nil m' h')

Result:
no goals

Proof state:
case cons
α : Type u_8
inst✝ : CommMonoid α
m : α
L : List α
ih : IsUnit L.prod → ∀ m ∈ L, IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ m_1 ∈ m :: L, IsUnit m_1

Tactic:
exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Result:
no goals

Proof state:
α : Type u_8
inst✝ : CommMonoid α
L : List α
⊢ IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m

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

Result:
α : Type u_8
inst✝ : CommMonoid α
L : List α
h : IsUnit L.prod
⊢ ∀ m ∈ L, IsUnit m

Proof state:
α : Type u_8
inst✝ : CommMonoid α
L : List α
h : IsUnit L.prod
⊢ ∀ m ∈ L, IsUnit m

Tactic:
induction L with
| nil => exact fun m' h' => False.elim (not_mem_nil m' h')
| cons m L ih =>
  rw [prod_cons, IsUnit.mul_iff] at h
  exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Result:
no goals

Proof state:
case cons
α : Type u_8
inst✝ : CommMonoid α
m : α
L : List α
ih : IsUnit L.prod → ∀ m ∈ L, IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ m_1 ∈ m :: L, IsUnit m_1

Tactic:
rw [prod_cons, IsUnit.mul_iff] at h

Result:
case cons
α : Type u_8
inst✝ : CommMonoid α
m : α
L : List α
ih : IsUnit L.prod → ∀ m ∈ L, IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ m_1 ∈ m :: L, IsUnit m_1
-- Mathlib/Data/NNReal/Basic.lean
theorem mul_iInf (f : ι → ℝ≥0) (a : ℝ≥0) : a * iInf f = ⨅ i, a * f i

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ a * iInf f = ⨅ i, a * f i

Tactic:
simpa only [mul_comm] using iInf_mul f a

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_inj {s t : Set α} [Fintype s] [Fintype t] : s.toFinset = t.toFinset ↔ s = t :=
  ⟨fun h => by rw [← s.coe_toFinset, h, t.coe_toFinset], fun h => by simp [h]⟩

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ s = t

Tactic:
rw [← s.coe_toFinset, h, t.coe_toFinset]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ s.toFinset = t.toFinset

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem erase_toFinmap (a : α) (s : AList β) : erase a ⟦s⟧ = AList.toFinmap (s.erase a)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ erase a ⟦s⟧ = ⟦AList.erase a s⟧

Tactic:
simp [erase]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem reflTransGen_of_transitive_reflexive {r' : α → α → Prop} (hr : Reflexive r)
    (ht : Transitive r) (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
h' : ReflTransGen r' a b
⊢ r a b

Tactic:
induction h' with
| refl => exact hr _
| tail _ hbc ih => exact ht ih (h _ _ hbc)

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
⊢ r a a

Tactic:
exact hr _

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
b✝ c✝ : α
a✝ : ReflTransGen r' a b✝
hbc : r' b✝ c✝
ih : r a b✝
⊢ r a c✝

Tactic:
exact ht ih (h _ _ hbc)

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem Frequently.exists {p : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x) : ∃ x, p x

Proof state:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False

Tactic:
replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)

Result:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False

Proof state:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ x, p x

Tactic:
by_contra H

Result:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False

Proof state:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False

Tactic:
exact hp H

Result:
no goals