harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem mem_iff_ultrafilter : s ∈ f ↔ ∀ g : Ultrafilter α, ↑g ≤ f → s ∈ g

Proof state:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
⊢ False

Tactic:
set g : Filter (sᶜ : Set α) := comap (↑) f

Result:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ False

Proof state:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ False

Tactic:
haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf] )

Result:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
this : g.NeBot
⊢ False

Proof state:
α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g

Tactic:
refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩

Result:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
⊢ False

Proof state:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ (range Subtype.val)ᶜ ∉ f

Tactic:
simpa [compl_setOf]

Result:
no goals

Proof state:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
this : g.NeBot
⊢ False

Tactic:
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_eq_self_iff_angle_eq_zero {x : V} (hx : x ≠ 0) (θ : Real.Angle) :
    o.rotation θ x = x ↔ θ = 0

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ) x = x
⊢ θ = 0

Tactic:
rw [eq_comm]

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ) x = x
⊢ 0 = θ

Proof state:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : θ = 0
⊢ (o.rotation θ) x = x

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ) x = x
⊢ 0 = θ

Tactic:
simpa [hx, h] using o.oangle_rotation_right hx hx θ

Result:
no goals

Proof state:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ θ = 0 → (o.rotation θ) x = x

Tactic:
intro h

Result:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : θ = 0
⊢ (o.rotation θ) x = x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ (o.rotation θ) x = x ↔ θ = 0

Tactic:
constructor

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ (o.rotation θ) x = x → θ = 0

case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ θ = 0 → (o.rotation θ) x = x

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ (o.rotation θ) x = x → θ = 0

Tactic:
intro h

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ) x = x
⊢ θ = 0
-- Mathlib/NumberTheory/WellApproximable.lean
theorem mem_addWellApproximable_iff (δ : ℕ → ℝ) (x : UnitAddCircle) :
    x ∈ addWellApproximable UnitAddCircle δ ↔
      {n : ℕ | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑((m : ℝ) / n)‖ < δ n}.Infinite

Proof state:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ x ∈ addWellApproximable UnitAddCircle δ ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

Tactic:
simp only [mem_add_wellApproximable_iff, ← Nat.cofinite_eq_atTop, cofinite.blimsup_set_eq,
  mem_setOf_eq]

Result:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}.Infinite ↔
    {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

Proof state:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}.Infinite ↔
    {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

Tactic:
refine iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)

Result:
case refine_1
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}
⊢ n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}

case refine_2
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
⊢ n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}

Proof state:
case intro.intro.intro
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left✝ : gcd m n = 1
right✝ : ‖x - ↑(↑m / ↑n)‖ < δ n
⊢ 0 < n

Tactic:
exact pos_of_gt hm₁

Result:
no goals

Proof state:
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
⊢ 0 < n

Tactic:
obtain ⟨m, hm₁, _, _⟩ := hn

Result:
case intro.intro.intro
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left✝ : gcd m n = 1
right✝ : ‖x - ↑(↑m / ↑n)‖ < δ n
⊢ 0 < n

Proof state:
case refine_1
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}
⊢ n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}

Tactic:
exact (mem_approxAddOrderOf_iff hn.1).mp hn.2

Result:
no goals

Proof state:
case refine_2
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
h : 0 < n
⊢ n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}

Tactic:
exact ⟨h, (mem_approxAddOrderOf_iff h).mpr hn⟩

Result:
no goals

Proof state:
case refine_2
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
⊢ n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}

Tactic:
have h : 0 < n := by obtain ⟨m, hm₁, _, _⟩ := hn; exact pos_of_gt hm₁

Result:
case refine_2
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
h : 0 < n
⊢ n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_mono' (h : a ≤ b) (ht : b = ∞ → a = ∞) : a.toReal ≤ b.toReal

Proof state:
case inl
b : ℝ≥0∞
h : ⊤ ≤ b
ht : b = ⊤ → ⊤ = ⊤
⊢ ⊤.toReal ≤ b.toReal

Tactic:
exact toReal_nonneg

Result:
no goals

Proof state:
a b : ℝ≥0∞
h : a ≤ b
ht : b = ⊤ → a = ⊤
⊢ a.toReal ≤ b.toReal

Tactic:
rcases eq_or_ne a ∞ with rfl | ha

Result:
case inl
b : ℝ≥0∞
h : ⊤ ≤ b
ht : b = ⊤ → ⊤ = ⊤
⊢ ⊤.toReal ≤ b.toReal

case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ⊤ → a = ⊤
ha : a ≠ ⊤
⊢ a.toReal ≤ b.toReal

Proof state:
case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ⊤ → a = ⊤
ha : a ≠ ⊤
⊢ a.toReal ≤ b.toReal

Tactic:
exact toReal_mono (mt ht ha) h

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem coe_update [DecidableEq α] : (f.update a b : α → M) = Function.update f a b

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
x✝ : α
⊢ { support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ }
      x✝ =
    if h : x✝ = a then ⋯ ▸ b else f x✝

Tactic:
dsimp

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
x✝ : α
⊢ (if h : x✝ = a then ⋯ ▸ b else f x✝) = if h : x✝ = a then ⋯ ▸ b else f x✝

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ ⇑(f.update a b) = Function.update (⇑f) a b

Tactic:
delta update Function.update

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ ⇑{ support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ } =
    fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ ⇑{ support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ } =
    fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
x✝ : α
⊢ { support := if b = 0 then f.support.erase a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then ⋯ ▸ b else f a_1, mem_support_toFun := ⋯ }
      x✝ =
    if h : x✝ = a then ⋯ ▸ b else f x✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
x✝ : α
⊢ (if h : x✝ = a then ⋯ ▸ b else f x✝) = if h : x✝ = a then ⋯ ▸ b else f x✝

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
lemma eq_universallyClosed_inf_isAffineHom :
    @IsIntegralHom = (@UniversallyClosed ⊓ @IsAffineHom : MorphismProperty Scheme)

Proof state:
⊢ @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsIntegralHom x✝ ↔ (@UniversallyClosed ⊓ @IsAffineHom) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsIntegralHom x✝ ↔ (@UniversallyClosed ⊓ @IsAffineHom) x✝

Tactic:
exact iff_universallyClosed_and_isAffineHom

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isLE_of_le (p q : ℤ) (hpq : p ≤ q) [K.IsLE p] :
    K.IsLE q

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
i : ℤ
hi : q < i
⊢ ExactAt K i

Tactic:
apply K.exactAt_of_isLE p

Result:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
i : ℤ
hi : q < i
⊢ p < i

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ K.IsLE q

Tactic:
rw [isLE_iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ ∀ (i : ℤ), q < i → ExactAt K i

Proof state:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
i : ℤ
hi : q < i
⊢ p < i

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ ∀ (i : ℤ), q < i → ExactAt K i

Tactic:
intro i hi

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
i : ℤ
hi : q < i
⊢ ExactAt K i
-- Mathlib/Data/Setoid/Partition.lean
theorem iUnion : ⋃ i, s i = univ

Proof state:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ x ∈ ⋃ i, s i ↔ x ∈ univ

Tactic:
simp [hs.exists_mem x]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ ⋃ i, s i = univ

Tactic:
ext x

Result:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ x ∈ ⋃ i, s i ↔ x ∈ univ
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem gcd_eq_sum : ∃ a b : R, a * x + b * y = gcd x y :=
  Ideal.mem_span_pair.mp (by rw [← span_gcd]; apply Ideal.subset_span; simp)

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}

Tactic:
apply Ideal.subset_span

Result:
case a
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {x, y}

Tactic:
rw [← span_gcd]

Result:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}
-- Mathlib/Analysis/Calculus/Deriv/Prod.lean
theorem derivWithin_pi (h : ∀ i, DifferentiableWithinAt 𝕜 (fun x => φ x i) s x) :
    derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x

Proof state:
case inl
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
inst✝² : Fintype ι
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x

Tactic:
exact (hasDerivWithinAt_pi.2 fun i => (h i).hasDerivWithinAt).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
inst✝² : Fintype ι
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x

Tactic:
simp only [derivWithin_zero_of_isolated hxs, Pi.zero_def]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
inst✝² : Fintype ι
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x
⊢ derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
inst✝² : Fintype ι
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x

case inr
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
inst✝² : Fintype ι
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.toPoly.degree = 2

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.toPoly.degree = 2

Tactic:
rw [of_a_eq_zero ha, degree_quadratic hb]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Floor.lean
theorem FloorSemiring.eventually_mul_pow_lt_factorial_sub (a c : K) (d : ℕ) :
    ∀ᶠ n in atTop, a * c ^ n < (n - d)!

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < ↑(n - d)!

Tactic:
filter_upwards [Nat.eventually_mul_pow_lt_factorial_sub ⌈|a|⌉₊ ⌈|c|⌉₊ d] with n h

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ a * c ^ n < ↑(n - d)!

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ a * c ^ n < ↑(n - d)!

Tactic:
calc a * c ^ n
  _ ≤ |a * c ^ n| := le_abs_self _
  _ ≤ ⌈|a|⌉₊ * (⌈|c|⌉₊ : K) ^ n := ?_
  _ = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) := ?_
  _ < (n - d)! := Nat.cast_lt.mpr h

Result:
case h.calc_1
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a * c ^ n| ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

case h.calc_2
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)

Proof state:
case h.calc_1
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| * |c| ^ n ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

Tactic:
gcongr <;> try first | positivity | apply Nat.le_ceil

Result:
no goals

Proof state:
case h.calc_2
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)

Tactic:
simp_rw [Nat.cast_mul, Nat.cast_pow]

Result:
no goals

Proof state:
case h.calc_1
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a * c ^ n| ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

Tactic:
rw [abs_mul, abs_pow]

Result:
case h.calc_1
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| * |c| ^ n ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

Proof state:
case h.calc_1.h₂.ha
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ 0 ≤ |c|

Tactic:
positivity

Result:
no goals

Proof state:
case h.calc_1.h₂.hab
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |c| ≤ ↑⌈|c|⌉₊

Tactic:
apply Nat.le_ceil

Result:
no goals

Proof state:
case h.calc_1.h₂.hab
K : Type u_1
inst✝¹ : LinearOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |c| ≤ ↑⌈|c|⌉₊

Tactic:
first | positivity | apply Nat.le_ceil

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem divp_mul_divp (x y : α) (ux uy : αˣ) : x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

Proof state:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

Tactic:
rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem subset_insert_diff_singleton (x : α) (s : Set α) : s ⊆ insert x (s \ {x})

Proof state:
α : Type u
x : α
s : Set α
⊢ s ⊆ insert x (s \ {x})

Tactic:
rw [← diff_singleton_subset_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma isRkFinite_iff (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsRkFinite X ↔ ∃ I, M.IsBasis I X ∧ I.Finite

Tactic:
simp_rw [isRkFinite_iff_exists_isBasis', M.isBasis'_iff_isBasis hX]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcdA_zero_left {s : ℕ} : gcdA 0 s = 0

Proof state:
s : ℕ
⊢ gcdA 0 s = 0

Tactic:
unfold gcdA

Result:
s : ℕ
⊢ (xgcd 0 s).1 = 0

Proof state:
s : ℕ
⊢ (xgcd 0 s).1 = 0

Tactic:
rw [xgcd, xgcd_zero_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem map_monotone (f : V ↪ W) : Monotone (SimpleGraph.map f)

Proof state:
case intro.intro.intro.intro
V : Type u_1
W : Type u_2
f : V ↪ W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)

Tactic:
exact ⟨_, _, h ha, rfl, rfl⟩

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ Monotone (SimpleGraph.map f)

Tactic:
rintro G G' h _ _ ⟨u, v, ha, rfl, rfl⟩

Result:
case intro.intro.intro.intro
V : Type u_1
W : Type u_2
f : V ↪ W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is one if the characteristic is zero. -/
lemma char_zero_of_expChar_one (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1] : p = 0

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0

Tactic:
cases hq

Result:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0

case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0

Proof state:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0

Tactic:
exact CharP.eq R hp inferInstance

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0

Tactic:
exact False.elim (CharP.char_ne_one R 1 rfl)

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma IsIntegralCurve.comp_add (hγ : IsIntegralCurve γ v) (dt : ℝ) :
    IsIntegralCurve (γ ∘ (· + dt)) v

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x => x + dt) v

Tactic:
rw [isIntegralCurve_iff_isIntegralCurveOn] at *

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurveOn γ v univ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x + dt) v univ

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsIntegralCurveOn γ v univ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x + dt) v univ

Tactic:
simpa using hγ.comp_add dt

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :
    m * npowRec' k m = npowRec' k m * m

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k + 2 ≠ 0
⊢ m * npowRec' (k + 2) m = npowRec' (k + 2) m * m

Tactic:
simp [npowRec', ← mul_assoc, ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
k0 : k ≠ 0
m : M
⊢ m * npowRec' k m = npowRec' k m * m

Tactic:
induction k using Nat.strongRecOn with
| ind k' ih =>
  match k' with
  | 1 => simp [npowRec', mul_assoc]
  | k + 2 => simp [npowRec', ← mul_assoc, ih]

Result:
no goals

Proof state:
case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k' ≠ 0
⊢ m * npowRec' k' m = npowRec' k' m * m

Tactic:
match k' with
| 1 => simp [npowRec', mul_assoc]
| k + 2 => simp [npowRec', ← mul_assoc, ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : 1 ≠ 0
⊢ m * npowRec' 1 m = npowRec' 1 m * m

Tactic:
simp [npowRec', mul_assoc]

Result:
no goals