harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma fderivWithin_pullbackWithin {f : E → F} {V : F → F} {x : E}
    (h'f : (fderivWithin 𝕜 f s x).IsInvertible) :
    fderivWithin 𝕜 f s x (pullbackWithin 𝕜 f V s x) = V (f x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
V : F → F
x : E
h'f : (fderivWithin 𝕜 f s x).IsInvertible
⊢ (fderivWithin 𝕜 f s x) (pullbackWithin 𝕜 f V s x) = V (f x)

Tactic:
rcases h'f with ⟨M, hM⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x) (pullbackWithin 𝕜 f V s x) = V (f x)

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x) (pullbackWithin 𝕜 f V s x) = V (f x)

Tactic:
simp [pullbackWithin_eq_of_fderivWithin_eq hM, ← hM]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma subsingleton [hX : HasProjectiveDimensionLT X n] (i : ℕ) (hi : n ≤ i) (Y : C) :
    Subsingleton (Ext.{w} X Y i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)

Tactic:
have := hX.subsingleton' i hi

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this✝ : HasExt C := HasExt.standard C
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext X Y i)

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this✝ : HasExt C := HasExt.standard C
this : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)

Tactic:
exact Ext.chgUniv.{w, max u v}.symm.subsingleton

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_pos_of_le_one {x : ℝ} (hx : |x| ≤ 1) : 0 < cos x :=
  calc 0 < 1 - x ^ 2 / 2 - |x| ^ 4 * (5 / 96) :=
      sub_pos.2 <|
        lt_sub_iff_add_lt.2
          (calc
            |x| ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2

Proof state:
case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1

Tactic:
rw [sq, ← abs_mul_self, abs_mul]

Result:
case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ |x| * |x| ≤ 1

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ 1 * (5 / 96) + 1 / 2 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ |x| * |x| ≤ 1

Tactic:
exact mul_le_one₀ hx (abs_nonneg _) hx

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2

Tactic:
gcongr

Result:
case h₁.h
x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 ≤ 1

case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1

Proof state:
case h₁.h
x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 ≤ 1

Tactic:
exact pow_le_one₀ (abs_nonneg _) hx

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_range_of_injective [Infinite α] {f : α → β} (hi : Injective f) :
    (range f).Infinite

Proof state:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (range f).Infinite

Tactic:
rw [← image_univ, infinite_image_iff hi.injOn]

Result:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite

Proof state:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite

Tactic:
exact infinite_univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
    x % n = x - n

Proof state:
x n : Nat
h₁ : n ≤ x
h₂ : x < 2 * n
⊢ 0 < n ∧ n ≤ x

Tactic:
omega

Result:
no goals

Proof state:
x n : Nat
h₁ : n ≤ x
h₂ : x < 2 * n
⊢ x % n = x - n

Tactic:
rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
x n : Nat
h₁ : n ≤ x
h₂ : x < 2 * n
⊢ x - n < n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
    ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

Proof state:
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i

Tactic:
rw [prod_eq_zero his]

Result:
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i ∈ s, w i * z i

case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0

Proof state:
case h.e'_4.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ x ∈ s, z x = 0 → w x = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
rw [exp_log hz]

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem nat_card_centralizer_nat_card_stabilizer (g : G) :
    Nat.card (Subgroup.centralizer {g}) =
      Nat.card (MulAction.stabilizer (ConjAct G) g)

Proof state:
G : Type u_3
inst✝ : Group G
g : G
⊢ Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [Subgroup.centralizer_eq_comap_stabilizer]

Result:
G : Type u_3
inst✝ : Group G
g : G
⊢ Nat.card ↥(comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)) =
    Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Proof state:
G : Type u_3
inst✝ : Group G
g : G
⊢ Nat.card ↥(comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)) =
    Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem sum_mul_eq_sub_integral_mul₀' (hc : c 0 = 0) (m : ℕ)
    (hf_diff : ∀ t ∈ Set.Icc (1 : ℝ) m, DifferentiableAt ℝ f t)
    (hf_int : IntegrableOn (deriv f) (Set.Icc (1 : ℝ) m)) :
    ∑ k ∈ Icc 0 m, f k * c k =
      f m * (∑ k ∈ Icc 0 m, c k) -
        ∫ t in Set.Ioc (1 : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Proof state:
case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

Tactic:
all_goals rw [Nat.floor_natCast]

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

Tactic:
rw [Nat.floor_natCast]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert sum_mul_eq_sub_integral_mul₀ c hc m hf_diff hf_int

Result:
case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
private lemma uniformity_eq_aux :
    𝓤 (CStarMatrix m n A) = (𝓤[Pi.uniformSpace _] :
      Filter (CStarMatrix m n A × CStarMatrix m n A))

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : (fun x => (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id
⊢ 𝓤 (Matrix m n A) = 𝓤 (CStarMatrix m n A)

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ (fun x => (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id

Tactic:
ext i <;> rfl

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : (fun x => (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n A)

Tactic:
rw [← uniformInducing_toMatrixAux.comap_uniformity, this, Filter.comap_id]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : (fun x => (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id
⊢ 𝓤 (Matrix m n A) = 𝓤 (CStarMatrix m n A)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n A)

Tactic:
have :
  (fun x : CStarMatrix m n A × CStarMatrix m n A => ⟨ofMatrix.symm x.1, ofMatrix.symm x.2⟩)
    = id := by
  ext i <;> rfl

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : (fun x => (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n A)
-- Mathlib/Order/UpperLower/Basic.lean
theorem IsLowerSet.not_bddBelow (hs : IsLowerSet s) : s.Nonempty → ¬BddBelow s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
c : α
hc : c < b
⊢ False

Tactic:
exact hc.not_le (hb <| hs (hc.le.trans <| hb ha) ha)

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_lt b

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
c : α
hc : c < b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMinOrder α
hs : IsLowerSet s
⊢ s.Nonempty → ¬BddBelow s

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
⊢ False
-- Mathlib/Algebra/Ring/Units.lean
theorem add_eq_mul_one_add_div [Semiring R] {a : Rˣ} {b : R} : ↑a + b = a * (1 + ↑a⁻¹ * b)

Proof state:
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * (1 + ↑a⁻¹ * b)

Tactic:
rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformRight.fst_mul_snd_subset :
    (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2

Tactic:
refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Tactic:
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_const_subset (α) [MeasurableSpace α] (b : β) : (const α b).range ⊆ {b} :=
  Finset.coe_subset.1 <| by simp

Proof state:
β : Type u_2
α : Type u_5
inst✝ : MeasurableSpace α
b : β
⊢ ↑(const α b).range ⊆ ↑{b}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_three : tan (π / 3) = sqrt 3

Proof state:
⊢ √3 / 2 / (1 / 2) = √3

Tactic:
ring

Result:
no goals

Proof state:
⊢ tan (π / 3) = √3

Tactic:
rw [tan_eq_sin_div_cos, sin_pi_div_three, cos_pi_div_three]

Result:
⊢ √3 / 2 / (1 / 2) = √3
-- Mathlib/Order/Filter/Finite.lean
theorem mem_iInf {ι} {s : ι → Filter α} {U : Set α} :
    (U ∈ ⨅ i, s i) ↔
      ∃ I : Set ι, I.Finite ∧ ∃ V : I → Set α, (∀ (i : I), V i ∈ s i) ∧ U = ⋂ i, V i

Proof state:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ t ⊆ ⋃ i, (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rintro ⟨t, tsub, tfin, tinter⟩

Result:
case mp.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ i, (s i).sets
tfin : t.Finite
tinter : ⋂₀ t ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
⊢ V i ∈ s ↑i

Tactic:
have : ⋂₀ σ i ∈ s i := by
  rw [sInter_mem (σfin _)]
  apply σsub

Result:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
this : ⋂₀ σ i ∈ s ↑i
⊢ V i ∈ s ↑i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∀ (i : ↑I), V i ∈ s ↑i

Tactic:
rintro i

Result:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
⊢ V i ∈ s ↑i

Proof state:
case mpr.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i ∈ ⨅ i, s i

Tactic:
exact mem_iInf_of_iInter Ifin V_in Subset.rfl

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = ⋂ i, V i

Tactic:
rwa [hV, ← union_iInter, union_eq_self_of_subset_right]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem not_cliqueFree_of_isTuranMaximal (hn : r ≤ Fintype.card V) (hG : G.IsTuranMaximal r) :
    ¬G.CliqueFree r

Proof state:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
a b : V
hab : a ≠ b
hGab : ¬G.Adj a b
⊢ False

Tactic:
exact hGab <| le_sup_right.trans_eq ((hG.le_iff_eq <| h.sup_edge _ _).1 le_sup_left).symm <|
  (edge_adj ..).2 ⟨Or.inl ⟨rfl, rfl⟩, hab⟩

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬G.Adj a b

Tactic:
simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
  exists_prop, exists_and_right] using h K

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
⊢ False

Tactic:
obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn

Result:
case intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ False

Proof state:
case intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ False

Tactic:
obtain ⟨a, -, b, -, hab, hGab⟩ : ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬ G.Adj a b := by
  simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
    exists_prop, exists_and_right] using h K

Result:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
K : Finset V
left✝ : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
a b : V
hab : a ≠ b
hGab : ¬G.Adj a b
⊢ False

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
⊢ ¬G.CliqueFree r

Tactic:
rintro h

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
⊢ False
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem measure_setOf_frequently_eq_zero {p : ℕ → α → Prop} (hp : ∑' i, μ { x | p i x } ≠ ∞) :
    μ { x | ∃ᶠ n in atTop, p n x } = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
p : ℕ → α → Prop
hp : ∑' (i : ℕ), μ {x | p i x} ≠ ⊤
⊢ μ {x | ∃ᶠ (n : ℕ) in atTop, p n x} = 0

Tactic:
simpa only [limsup_eq_iInf_iSup_of_nat, frequently_atTop, ← bex_def, setOf_forall,
  setOf_exists] using measure_limsup_atTop_eq_zero hp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_rotate' : ∀ (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m)
  | a :: l, 0, m => by simp
  | [], n, m => by simp
  | a :: l, n + 1, m => by
    rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]

Proof state:
α : Type u
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
  Nat.succ_eq_add_one]

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
m : ℕ
⊢ ((a :: l).rotate' 0).rotate' m = (a :: l).rotate' (0 + m)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n m : ℕ
⊢ ([].rotate' n).rotate' m = [].rotate' (n + m)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.isMin (h : IsSuccPrelimit a) : IsMin a := fun b hb => by
  revert h
  refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
  have := hc.isMax.succ_eq
  rw [this] at hc ⊢
  exact H hc

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Tactic:
revert h

Result:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccPrelimit a → a ≤ b

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit (succ c)
this : succ c = c
⊢ succ c ≤ b

Tactic:
rw [this] at hc ⊢

Result:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit c
this : succ c = c
⊢ c ≤ b

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit (succ c)
⊢ succ c ≤ b

Tactic:
have := hc.isMax.succ_eq

Result:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit (succ c)
this : succ c = c
⊢ succ c ≤ b

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccPrelimit a → a ≤ b

Tactic:
refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb

Result:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit (succ c)
⊢ succ c ≤ b

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccPrelimit c → c ≤ b
hc : IsSuccPrelimit c
this : succ c = c
⊢ c ≤ b

Tactic:
exact H hc

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusMap_plusLift {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : Presheaf.IsSheaf J R) :
    J.plusMap η ≫ J.plusLift γ hR = J.plusLift (η ≫ γ) hR

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.plusMap η ≫ J.plusLift γ hR = J.plusLift (η ≫ γ) hR

Tactic:
apply J.plusLift_unique

Result:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.toPlus P ≫ J.plusMap η ≫ J.plusLift γ hR = η ≫ γ

Proof state:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.toPlus P ≫ J.plusMap η ≫ J.plusLift γ hR = η ≫ γ

Tactic:
rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]

Result:
no goals