harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem coe_real_preimage_closedBall_inter_eq {x ε : ℝ} (s : Set ℝ)
    (hs : s ⊆ closedBall x (|p| / 2)) :
    (↑) ⁻¹' closedBall (x : AddCircle p) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

Proof state:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
this : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
simp [-zsmul_eq_mul, ← QuotientAddGroup.mk_zero, coe_real_preimage_closedBall_eq_iUnion,
  iUnion_inter, iUnion_ite, this, hε]

Result:
no goals

Proof state:
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅

Tactic:
simp only [Real.closedBall_eq_Icc, zero_sub, zero_add] at hs ⊢

Result:
case inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Proof state:
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε

Tactic:
exact hs.trans (closedBall_subset_closedBall <| by simp [hε])

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False

Tactic:
linarith [abs_eq_self.mpr hp.le]

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ False

Tactic:
have : -p ≤ ↑z * p := by nlinarith

Result:
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem of_length_zero {x : BitVec 0} : x = 0#0

Proof state:
case pred
x : BitVec 0
i✝ : Nat
a✝ : i✝ < 0
⊢ x.getLsbD i✝ = (0#0).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
x : BitVec 0
⊢ x = 0#0

Tactic:
ext

Result:
case pred
x : BitVec 0
i✝ : Nat
a✝ : i✝ < 0
⊢ x.getLsbD i✝ = (0#0).getLsbD i✝
-- Mathlib/Data/Nat/Squarefree.lean
theorem minSqFac_dvd {n d : ℕ} (h : n.minSqFac = some d) : d * d ∣ n

Proof state:
n d : ℕ
h : n.minSqFac = some d
⊢ d * d ∣ n

Tactic:
have := minSqFac_has_prop n

Result:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ d * d ∣ n

Proof state:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n

Tactic:
exact this.2.1

Result:
no goals

Proof state:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ d * d ∣ n

Tactic:
rw [h] at this

Result:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_C_mul (a0 : a ≠ 0) : (C a * p).degree = p.degree

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
rw [degree_mul, degree_C a0, zero_add]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :
    ∃ p : ℕ, a.factorization p < b.factorization p

Proof state:
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
contrapose! hab

Result:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), b.factorization p ≤ a.factorization p
⊢ b ≤ a

Proof state:
a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'

Result:
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, a.factorization p < b.factorization p

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a

Tactic:
exact le_of_dvd ha.bot_lt hab

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), b.factorization p ≤ a.factorization p
⊢ b ≤ a

Tactic:
rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab

Result:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
-- Mathlib/Computability/Reduce.lean
theorem of_eq_of {p : α → Prop} {q : β → Prop} : of p = of q ↔ ManyOneEquiv p q

Proof state:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ { r := ManyOneEquiv, iseqv := proof_1 } (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ of p = of q ↔ ManyOneEquiv p q

Tactic:
rw [of, of, Quotient.eq'']

Result:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ { r := ManyOneEquiv, iseqv := proof_1 } (toNat p) (toNat q) ↔ ManyOneEquiv p q
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem bowtie {j₁ j₂ k₁ k₂ : C} (f₁ : k₁ ⟶ j₁) (g₁ : k₂ ⟶ j₁) (f₂ : k₁ ⟶ j₂) (g₂ : k₂ ⟶ j₂) :
    ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := cospan f₁ g₁

Result:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ (ts ≫ k₁t) ≫ f₂ = (ts ≫ k₂t) ≫ g₂

Tactic:
simp only [Category.assoc, hs]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ (ts ≫ k₁t) ≫ f₁ = (ts ≫ k₂t) ≫ g₁

Tactic:
simp only [Category.assoc, ht]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
exact ⟨s, ts ≫ k₁t, ts ≫ k₂t, by simp only [Category.assoc, ht],
  by simp only [Category.assoc, hs]⟩

Result:
no goals

Proof state:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
obtain ⟨s, ts, hs⟩ := IsCofilteredOrEmpty.cone_maps (k₁t ≫ f₂) (k₂t ≫ g₂)

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem isIso_π_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasLimit F]
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramTerminal I F), by ext; simp, by simp⟩⟩

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.lift F (coneOfDiagramTerminal I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem col_injective [Nonempty ι] : Function.Injective (col ι : (m → α) → Matrix m ι α)

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
⊢ Function.Injective (col ι)

Tactic:
inhabit ι

Result:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (col ι)

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (col ι)

Tactic:
exact fun _x _y h => funext fun i => congr_fun₂ h i default

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
    derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, derivWithin (A i) s x

Tactic:
exact (HasDerivWithinAt.sum fun i hi => (h i hi).hasDerivWithinAt).derivWithin hxs

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Defs.lean
theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M}
    (hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
  | 0 => by
    rw [pow_zero]
    exact OneMemClass.one_mem S
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem (pow_mem hx n) hx

Proof state:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S

Tactic:
exact mul_mem (pow_mem hx n) hx

Result:
no goals

Proof state:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
rw [pow_zero]

Result:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S

Proof state:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S

Tactic:
rw [pow_succ]

Result:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S

Proof state:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S

Tactic:
exact OneMemClass.one_mem S

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.iSup_mem_of_nonempty [Finite ι] [Nonempty ι] (hs : SupClosed s)
    (hf : ∀ i, f i ∈ s) : ⨆ i, f i ∈ s

Proof state:
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
cases nonempty_fintype (PLift ι)

Result:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ ⨆ i, f i ∈ s

Proof state:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i => f i.down) ∈ s

Tactic:
exact hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _

Result:
no goals

Proof state:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ ⨆ i, f i ∈ s

Tactic:
rw [← iSup_plift_down, ← Finset.sup'_univ_eq_ciSup]

Result:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i => f i.down) ∈ s
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_eq_tsub_of_add_eq_add (h : a + d = c + b) : a - b = c - d

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a - b = a + d - d - b

Tactic:
rw [add_tsub_cancel_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a - b = c - d

Tactic:
calc a - b = a + d - d - b := by rw [add_tsub_cancel_right]
         _ = c + b - b - d := by rw [h, tsub_right_comm]
         _ = c - d := by rw [add_tsub_cancel_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a + d - d - b = c + b - b - d

Tactic:
rw [h, tsub_right_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ c + b - b - d = c - d

Tactic:
rw [add_tsub_cancel_right]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem ae_of_mem_of_ae_of_mem_inter_Ioo {μ : Measure ℝ} [NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop}
    (h : ∀ a b, a ∈ s → b ∈ s → a < b → ∀ᵐ x ∂μ, x ∈ s ∩ Ioo a b → p x) :
    ∀ᵐ x ∂μ, x ∈ s → p x

Proof state:
case mk.mk.mk
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

Tactic:
rcases le_or_lt b a with (hba | hab)

Result:
case mk.mk.mk.inl
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x

case mk.mk.mk.inr
μ : Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_lt_of_forall_not_threeGPFree
    (h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ((t : Finset α) : Set α)) :
    mulRothNumber s < n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
⊢ mulRothNumber s < n

Tactic:
obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ mulRothNumber s < n

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
hn : n ≤ #t
⊢ False

Tactic:
obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
u : Finset α
hut : u ⊆ t
h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree ↑t
hn : #u ≤ #t
⊢ False

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ mulRothNumber s < n

Tactic:
rw [← hcard, ← not_le]

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ ¬n ≤ #t

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
u : Finset α
hut : u ⊆ t
h : ∀ t ∈ powersetCard (#u) s, ¬ThreeGPFree ↑t
hn : #u ≤ #t
⊢ False

Tactic:
exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
⊢ ¬n ≤ #t

Tactic:
intro hn

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t
t : Finset α
hts : t ⊆ s
hcard : #t = mulRothNumber s
ht : ThreeGPFree ↑t
hn : n ≤ #t
⊢ False
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem IsAffineOpen.isQuasiSeparated {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) :
    IsQuasiSeparated (U : Set X)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace ↑↑U

case hs
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen ↑U

Tactic:
exacts [@AlgebraicGeometry.quasiSeparatedSpace_of_isAffine _ hU, U.isOpen]

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsQuasiSeparated ↑U

Tactic:
rw [isQuasiSeparated_iff_quasiSeparatedSpace]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace ↑↑U

case hs
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen ↑U
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.bUnion {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} {u : Set ι} (hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ) :
    IndepSets (⋃ n ∈ u, s n) s' κ μ

Proof state:
case intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact hyp n hpn t1 t2 ht1 ht2

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
⊢ IndepSets (⋃ n ∈ u, s n) s' κ μ

Tactic:
intro t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋃ n ∈ u, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋃ n ∈ u, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
simp_rw [Set.mem_iUnion] at ht1

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ i, ∃ (_ : i ∈ u), t1 ∈ s i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ i, ∃ (_ : i ∈ u), t1 ∈ s i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rcases ht1 with ⟨n, hpn, ht1⟩

Result:
case intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2