harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
theorem generalized_tube_lemma (hs : IsCompact s) {t : Set Y} (ht : IsCompact t)
    {n : Set (X × Y)} (hn : IsOpen n) (hp : s ×ˢ t ⊆ n) :
    ∃ (u : Set X) (v : Set Y), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Proof state:
case intro.mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn✝ : IsOpen n
u : Set X
v : Set Y
hn : (u, v).1 ×ˢ (u, v).2 ⊆ n
huo : IsOpen (u, v).1
hsu : s ⊆ (u, v).1
hvo : IsOpen (u, v).2
htv : t ⊆ (u, v).2
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
exact ⟨u, v, huo, hvo, hsu, htv, hn⟩

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen n
hp : ∃ i, ((IsOpen i.1 ∧ s ⊆ i.1) ∧ IsOpen i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩

Result:
case intro.mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn✝ : IsOpen n
u : Set X
v : Set Y
hn : (u, v).1 ×ˢ (u, v).2 ⊆ n
huo : IsOpen (u, v).1
hsu : s ⊆ (u, v).1
hvo : IsOpen (u, v).2
htv : t ⊆ (u, v).2
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen n
hp : s ×ˢ t ⊆ n
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht,
  ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen n
hp : ∃ i, ((IsOpen i.1 ∧ s ⊆ i.1) ∧ IsOpen i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
-- Mathlib/Order/CompleteLattice.lean
theorem iInf₂_eq_top {f : ∀ i, κ i → α} : ⨅ (i) (j), f i j = ⊤ ↔ ∀ i j, f i j = ⊤

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ ⨅ i, ⨅ j, f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem symm {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : Equivalent s₂ s₁ :=
  ⟨h.choose.symm, fun i => iso_symm (by simpa using h.choose_spec (h.choose.symm i))⟩

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
i : Fin s₂.length
⊢ Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ)
    (s₂.toFun i.castSucc, s₂.toFun i.succ)

Tactic:
simpa using h.choose_spec (h.choose.symm i)

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem inv_zero : (0 : (Cauchy abv))⁻¹ = 0 :=
  congr_arg mk <| by rw [dif_pos] <;> [rfl; exact zero_limZero]

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0

Tactic:
rw [dif_pos] <;> [rfl; exact zero_limZero]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMaxOn.hasFDerivWithinAt_eq_zero (h : IsLocalMaxOn f s a)
    (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a)
    (hy' : -y ∈ posTangentConeAt s a) : f' y = 0 :=
  le_antisymm (h.hasFDerivWithinAt_nonpos hf hy) <| by simpa using h.hasFDerivWithinAt_nonpos hf hy'

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ 0 ≤ f' y

Tactic:
simpa using h.hasFDerivWithinAt_nonpos hf hy'

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
    finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V

Proof state:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank K (V ⧸ ker f) + finrank K ↥(ker f) = finrank K V

Tactic:
exact Submodule.finrank_quotient_add_finrank _

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V

Tactic:
rw [← f.quotKerEquivRange.finrank_eq]

Result:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank K (V ⧸ ker f) + finrank K ↥(ker f) = finrank K V
-- Mathlib/Order/Filter/Map.lean
theorem inf_principal_eq_bot_iff_comap {F : Filter α} {s : Set α} :
    F ⊓ 𝓟 s = ⊥ ↔ comap ((↑) : s → α) F = ⊥

Proof state:
α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ 𝓟 s = ⊥ ↔ comap Subtype.val F = ⊥

Tactic:
rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]

Result:
no goals
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem IsAlgClosed.algebraicClosure_eq_bot_iff [IsAlgClosed E] :
    algebraicClosure F E = ⊥ ↔ IsAlgClosed F

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
⊢ algebraicClosure F E = ⊥ ↔ IsAlgClosed F

Tactic:
refine ⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
  fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩

Result:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
⊢ ∃ x, eval x p = 0

Proof state:
case intro.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ eval x p = 0

Tactic:
simpa [Algebra.ofId_apply] using hx

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne'

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : E
hx : (aeval x) p = 0
⊢ ∃ x, eval x p = 0

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : E
hx : (aeval x) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, rfl⟩ := h ▸ mem_algebraicClosure_iff'.2 (minpoly.ne_zero_iff.1 <|
  ne_zero_of_dvd_ne_zero hmon.ne_zero (minpoly.dvd _ x hx))

Result:
case intro.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_zero (f : R) (U hu) : const R 0 f U hu = 0 :=
  Subtype.eq <| funext fun x => IsLocalization.mk'_eq_iff_eq_mul.2 <| by
    rw [RingHom.map_zero]
    exact (mul_eq_zero_of_left rfl ((algebraMap R (Localizations R x)) _)).symm

Proof state:
R : Type u
inst✝ : CommRing R
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl
x : ↥(unop (op U))
⊢ (algebraMap R (Localizations R ↑x)) 0 = ↑0 x * (algebraMap R (Localizations R ↑x)) ↑⟨f, ⋯⟩

Tactic:
rw [RingHom.map_zero]

Result:
R : Type u
inst✝ : CommRing R
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl
x : ↥(unop (op U))
⊢ 0 = ↑0 x * (algebraMap R (Localizations R ↑x)) ↑⟨f, ⋯⟩

Proof state:
R : Type u
inst✝ : CommRing R
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl
x : ↥(unop (op U))
⊢ 0 = ↑0 x * (algebraMap R (Localizations R ↑x)) ↑⟨f, ⋯⟩

Tactic:
exact (mul_eq_zero_of_left rfl ((algebraMap R (Localizations R x)) _)).symm

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem isSheaf_iff_preservesFiniteProducts_of_projective [Preregular C] [FinitaryExtensive C]
    [∀ (X : C), Projective X] :
    IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F

Tactic:
rw [isSheaf_coherent_iff_regular_and_extensive, and_iff_left (isSheaf_of_projective F),
  isSheaf_iff_preservesFiniteProducts]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp] lemma one_lt_sq_iff_one_lt_abs (a : α) : 1 < a ^ 2 ↔ 1 < |a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ 1 < a ^ 2 ↔ 1 < |a|

Tactic:
simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 a

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_lt_iff (ha : ⊥ < a) : s.sup f < a ↔ ∀ b ∈ s, f b < a :=
  ⟨fun hs _ hb => lt_of_le_of_lt (le_sup hb) hs,
    Finset.cons_induction_on s (fun _ => ha) fun c t hc => by
      simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right⟩

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
⊢ ((∀ b ∈ t, f b < a) → t.sup f < a) → (∀ b ∈ cons c t hc, f b < a) → (cons c t hc).sup f < a

Tactic:
simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.max_zero {f : α → ℝ} (hf : HasFiniteIntegral f μ) :
    HasFiniteIntegral (fun a => max (f a) 0) μ :=
  hf.mono <| Eventually.of_forall fun x => by simp [abs_le, le_abs_self]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖f x ⊔ 0‖ ≤ ‖f x‖

Tactic:
simp [abs_le, le_abs_self]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive sub_one_nsmul_add]
lemma mul_pow_sub_one (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma mem_uIcc : a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
simp [uIcc_eq_union]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_push (a : Vector α n) (x : α) (i : Nat) (h : i < n + 1) :
    (a.push x)[i] = if h : i < n then a[i] else x

Proof state:
α : Type u_1
n : Nat
a : Vector α n
x : α
i : Nat
h : i < n + 1
⊢ (a.push x)[i] = if h : i < n then a[i] else x

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
x : α
i : Nat
a : Array α
h : i < a.size + 1
⊢ ({ toArray := a, size_toArray := ⋯ }.push x)[i] = if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else x

Proof state:
case mk
α : Type u_1
x : α
i : Nat
a : Array α
h : i < a.size + 1
⊢ ({ toArray := a, size_toArray := ⋯ }.push x)[i] = if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else x

Tactic:
simp [Array.getElem_push]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem mem_idealOfSet {s : Set X} {f : C(X, R)} :
    f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0

Tactic:
convert Iff.rfl

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem comp_init {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) :
    g ∘ init q = init (g ∘ q)

Proof state:
case h
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j

Tactic:
simp [init]

Result:
no goals

Proof state:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
⊢ g ∘ init q = init (g ∘ q)

Tactic:
ext j

Result:
case h
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j
-- Mathlib/Data/Nat/Bits.lean
lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n

Proof state:
n : ℕ
h : n ≠ 0
this : n * 1 < n * succ 1
⊢ n < n * succ 1

Tactic:
rwa [Nat.mul_one] at this

Result:
no goals

Proof state:
n : ℕ
h : n ≠ 0
⊢ n.div2 < n

Tactic:
rw [div2_val]

Result:
n : ℕ
h : n ≠ 0
⊢ n / 2 < n

Proof state:
n : ℕ
h : n ≠ 0
⊢ n / 2 < n

Tactic:
apply (div_lt_iff_lt_mul <| succ_pos 1).2

Result:
n : ℕ
h : n ≠ 0
⊢ n < n * succ 1

Proof state:
n : ℕ
h : n ≠ 0
⊢ n < n * succ 1

Tactic:
have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
  (lt_of_le_of_ne n.zero_le h.symm)

Result:
n : ℕ
h : n ≠ 0
this : n * 1 < n * succ 1
⊢ n < n * succ 1
-- Mathlib/FieldTheory/IntermediateField/Algebraic.lean
theorem eq_of_le_of_finrank_le' [FiniteDimensional F L] (h_le : F ≤ E)
    (h_finrank : finrank F L ≤ finrank E L) : F = E

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E

Tactic:
refine le_antisymm h_le (fun l hl ↦ ?_)

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ F

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ F

Tactic:
rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
  ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {p₁ p₂ p₃ p₄ p₅ : P} (hapc : ∠ p₁ p₅ p₃ = π)
    (hbpd : ∠ p₂ p₅ p₄ = π) : ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p₅ : P
hapc : ∠ p₁ p₅ p₃ = π
hbpd : ∠ p₂ p₅ p₄ = π
⊢ ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄

Tactic:
linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
  angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ p₃]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasStrictDerivAt h₂ h₂' y) (hf : HasStrictFDerivAt f f' x) (hy : y = f x) :
    HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' (f x)
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
exact hh.comp_hasStrictFDerivAt x hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' y
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
rw [hy] at hh

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' (f x)
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Mathlib/Analysis/PSeries.lean
theorem tendsto_sum_range_one_div_nat_succ_atTop :
    Tendsto (fun n => ∑ i ∈ Finset.range n, (1 / (i + 1) : ℝ)) atTop atTop

Proof state:
i : ℕ
⊢ 0 ≤ 1 / (↑i + 1)

Tactic:
positivity

Result:
no goals

Proof state:
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) atTop atTop

Tactic:
rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]

Result:
⊢ ¬Summable fun i => 1 / (↑i + 1)


⊢ ∀ (n : ℕ), 0 ≤ 1 / (↑n + 1)

Proof state:
⊢ ¬Summable fun i => 1 / (↑i + 1)

Tactic:
exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 not_summable_one_div_natCast

Result:
no goals

Proof state:
⊢ ∀ (n : ℕ), 0 ≤ 1 / (↑n + 1)

Tactic:
exact fun i => by positivity

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ) :
    (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Proof state:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_closedBall]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c :=
  ⟨exists_mul_of_le, by
    rintro ⟨c, rfl⟩
    exact le_self_mul⟩

Proof state:
α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ (∃ c, b = a * c) → a ≤ b

Tactic:
rintro ⟨c, rfl⟩

Result:
case intro
α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c

Proof state:
case intro
α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c

Tactic:
exact le_self_mul

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem rightUnitor_tensor (X Y : C) :
    (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_nil : rtakeWhile p ([] : List α) = []

Proof state:
α : Type u_1
p : α → Bool
⊢ rtakeWhile p [] = []

Tactic:
simp [rtakeWhile, takeWhile]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem strictMonoOn_projIcc : StrictMonoOn (projIcc a b h) (Icc a b) := fun x hx y hy hxy => by
  simpa only [projIcc_of_mem, hx, hy]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y

Tactic:
simpa only [projIcc_of_mem, hx, hy]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem IicSnd_mono {r r' : ℝ} (h_le : r ≤ r') : ρ.IicSnd r ≤ ρ.IicSnd r'

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r r' : ℝ
h_le : r ≤ r'
⊢ (ρ.restrict (univ ×ˢ Iic r)).fst ≤ (ρ.restrict (univ ×ˢ Iic r')).fst

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r r' : ℝ
h_le : r ≤ r'
⊢ ρ.IicSnd r ≤ ρ.IicSnd r'

Tactic:
unfold IicSnd

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r r' : ℝ
h_le : r ≤ r'
⊢ (ρ.restrict (univ ×ˢ Iic r)).fst ≤ (ρ.restrict (univ ×ˢ Iic r')).fst
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_univ (M : Matroid α) : M.closure univ = M.E

Proof state:
α : Type u_2
M : Matroid α
⊢ M.closure univ = M.E

Tactic:
rw [← closure_inter_ground, univ_inter, closure_ground]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem mem_iff {x : R} : x ∈ selfAdjoint R ↔ star x = x

Proof state:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ selfAdjoint R ↔ star x = x

Tactic:
rw [← AddSubgroup.mem_carrier]

Result:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).carrier ↔ star x = x

Proof state:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).carrier ↔ star x = x

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem spanSingleton_div_self {x : K} (hx : x ≠ 0) :
    spanSingleton R₁⁰ x / spanSingleton R₁⁰ x = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ x / spanSingleton R₁⁰ x = 1

Tactic:
rw [spanSingleton_div_spanSingleton, div_self hx, spanSingleton_one]

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma algebraMap_apply (x) : algebraMap P.Ring S x = aeval (R := R) P.val x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x : P.Ring
⊢ (algebraMap P.Ring S) x = (aeval P.val) x

Tactic:
simp [algebraMap_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essInf_eq_sSup {m : MeasurableSpace α} (μ : Measure α) (f : α → β) :
    essInf f μ = sSup { a | μ { x | f x < a } = 0 }

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sSup {a | ∀ᶠ (n : β) in map f (ae μ), a ≤ n} = sSup {a | μ {x | f x < a} = 0}

Tactic:
simp only [eventually_map, ae_iff, not_le]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essInf f μ = sSup {a | μ {x | f x < a} = 0}

Tactic:
dsimp [essInf, liminf, limsInf]

Result:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sSup {a | ∀ᶠ (n : β) in map f (ae μ), a ≤ n} = sSup {a | μ {x | f x < a} = 0}
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_add_smul_left (x y : V) (r : ℝ) :
    (o.oangle (x + r • y) y).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle (x + r • y) y).sign = (o.oangle x y).sign

Tactic:
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]

Result:
no goals